Ext groups in abelian categories #
Let C be an abelian category (with C : Type u and Category.{v} C).
In this file, we introduce the assumption HasExt.{w} C which asserts
that morphisms between single complexes in arbitrary degrees in
the derived category of C are w-small. Under this assumption,
we define Ext.{w} X Y n : Type w as shrunk versions of suitable
types of morphisms in the derived category. In particular, when C has
enough projectives or enough injectives, the property HasExt.{v} C
shall hold (TODO).
Note: in certain situations, w := v shall be the preferred
choice of universe (e.g. if C := ModuleCat.{v} R with R : Type v).
However, in the development of the API for Ext-groups, it is important
to keep a larger degree of generality for universes, as w < v
may happen in certain situations. Indeed, if X : Scheme.{u},
then the underlying category of the étale site of X shall be a large
category. However, the category Sheaf X.Etale AddCommGroupCat.{u}
shall have good properties (because there is a small category of affine
schemes with the same category of sheaves), and even though the type of
morphisms in Sheaf X.Etale AddCommGroupCat.{u} shall be
in Type (u + 1), these types are going to be u-small.
Then, for C := Sheaf X.etale AddCommGroupCat.{u}, we will have
Category.{u + 1} C, but HasExt.{u} C will hold
(as C has enough injectives). Then, the Ext groups between étale
sheaves over X shall be in Type u.
TODO #
@[reducible, inline]
abbrev
CategoryTheory.HasExt
(C : Type u)
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Abelian C]
:
The property that morphisms between single complexes in arbitrary degrees are w-small
in the derived category.
Equations
- One or more equations did not get rendered due to their size.
theorem
CategoryTheory.hasExt_iff
(C : Type u)
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Abelian C]
[HasDerivedCategory C]
:
CategoryTheory.HasExt C ↔ ∀ (X Y : C) (n : ℤ),
Small.{w, w'}
((DerivedCategory.singleFunctor C 0).obj X ⟶ (CategoryTheory.shiftFunctor (DerivedCategory C) n).obj ((DerivedCategory.singleFunctor C 0).obj Y))
theorem
CategoryTheory.hasExt_of_hasDerivedCategory
(C : Type u)
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Abelian C]
[HasDerivedCategory C]
:
def
CategoryTheory.Abelian.Ext
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Abelian C]
[CategoryTheory.HasExt C]
(X Y : C)
(n : ℕ)
:
Type w
A Ext-group in an abelian category C, defined as a Type w when [HasExt.{w} C].
Equations
- One or more equations did not get rendered due to their size.
noncomputable def
CategoryTheory.Abelian.Ext.comp
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Abelian C]
[CategoryTheory.HasExt C]
{X Y Z : C}
{a b : ℕ}
(α : CategoryTheory.Abelian.Ext X Y a)
(β : CategoryTheory.Abelian.Ext Y Z b)
{c : ℕ}
(h : a + b = c)
:
The composition of Ext.
Equations
- α.comp β h = CategoryTheory.Localization.SmallShiftedHom.comp α β ⋯
theorem
CategoryTheory.Abelian.Ext.comp_assoc
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Abelian C]
[CategoryTheory.HasExt C]
{X Y Z T : C}
{a₁ a₂ a₃ a₁₂ a₂₃ a : ℕ}
(α : CategoryTheory.Abelian.Ext X Y a₁)
(β : CategoryTheory.Abelian.Ext Y Z a₂)
(γ : CategoryTheory.Abelian.Ext Z T a₃)
(h₁₂ : a₁ + a₂ = a₁₂)
(h₂₃ : a₂ + a₃ = a₂₃)
(h : a₁ + a₂ + a₃ = a)
:
(α.comp β h₁₂).comp γ ⋯ = α.comp (β.comp γ h₂₃) ⋯
@[simp]
theorem
CategoryTheory.Abelian.Ext.comp_assoc_of_second_deg_zero
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Abelian C]
[CategoryTheory.HasExt C]
{X Y Z T : C}
{a₁ a₃ a₁₃ : ℕ}
(α : CategoryTheory.Abelian.Ext X Y a₁)
(β : CategoryTheory.Abelian.Ext Y Z 0)
(γ : CategoryTheory.Abelian.Ext Z T a₃)
(h₁₃ : a₁ + a₃ = a₁₃)
:
(α.comp β ⋯).comp γ h₁₃ = α.comp (β.comp γ ⋯) h₁₃
@[simp]
theorem
CategoryTheory.Abelian.Ext.comp_assoc_of_third_deg_zero
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Abelian C]
[CategoryTheory.HasExt C]
{X Y Z T : C}
{a₁ a₂ a₁₂ : ℕ}
(α : CategoryTheory.Abelian.Ext X Y a₁)
(β : CategoryTheory.Abelian.Ext Y Z a₂)
(γ : CategoryTheory.Abelian.Ext Z T 0)
(h₁₂ : a₁ + a₂ = a₁₂)
:
(α.comp β h₁₂).comp γ ⋯ = α.comp (β.comp γ ⋯) h₁₂
noncomputable def
CategoryTheory.Abelian.Ext.homEquiv
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Abelian C]
[CategoryTheory.HasExt C]
{X Y : C}
[HasDerivedCategory C]
{n : ℕ}
:
CategoryTheory.Abelian.Ext X Y n ≃ CategoryTheory.ShiftedHom ((DerivedCategory.singleFunctor C 0).obj X) ((DerivedCategory.singleFunctor C 0).obj Y) ↑n
When an instance of [HasDerivedCategory.{w'} C] is available, this is the bijection
between Ext.{w} X Y n and a type of morphisms in the derived category.
Equations
- CategoryTheory.Abelian.Ext.homEquiv = CategoryTheory.Localization.SmallShiftedHom.equiv (HomologicalComplex.quasiIso C (ComplexShape.up ℤ)) DerivedCategory.Q
@[reducible, inline]
noncomputable abbrev
CategoryTheory.Abelian.Ext.hom
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Abelian C]
[CategoryTheory.HasExt C]
{X Y : C}
[HasDerivedCategory C]
{a : ℕ}
(α : CategoryTheory.Abelian.Ext X Y a)
:
CategoryTheory.ShiftedHom ((DerivedCategory.singleFunctor C 0).obj X) ((DerivedCategory.singleFunctor C 0).obj Y) ↑a
The morphism in the derived category which corresponds to an element in Ext X Y a.
Equations
- α.hom = CategoryTheory.Abelian.Ext.homEquiv α
@[simp]
theorem
CategoryTheory.Abelian.Ext.comp_hom
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Abelian C]
[CategoryTheory.HasExt C]
{X Y Z : C}
[HasDerivedCategory C]
{a b : ℕ}
(α : CategoryTheory.Abelian.Ext X Y a)
(β : CategoryTheory.Abelian.Ext Y Z b)
{c : ℕ}
(h : a + b = c)
:
(α.comp β h).hom = α.hom.comp β.hom ⋯
theorem
CategoryTheory.Abelian.Ext.ext
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Abelian C]
[CategoryTheory.HasExt C]
{X Y : C}
[HasDerivedCategory C]
{n : ℕ}
{α β : CategoryTheory.Abelian.Ext X Y n}
(h : α.hom = β.hom)
:
α = β
noncomputable def
CategoryTheory.Abelian.Ext.mk₀
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Abelian C]
[CategoryTheory.HasExt C]
{X Y : C}
(f : X ⟶ Y)
:
The canonical map (X ⟶ Y) → Ext X Y 0.
Equations
- One or more equations did not get rendered due to their size.
@[simp]
theorem
CategoryTheory.Abelian.Ext.mk₀_hom
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Abelian C]
[CategoryTheory.HasExt C]
{X Y : C}
[HasDerivedCategory C]
(f : X ⟶ Y)
:
(CategoryTheory.Abelian.Ext.mk₀ f).hom = CategoryTheory.ShiftedHom.mk₀ ↑0 ⋯ ((DerivedCategory.singleFunctor C 0).map f)
@[simp]
theorem
CategoryTheory.Abelian.Ext.mk₀_comp_mk₀
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Abelian C]
[CategoryTheory.HasExt C]
{X Y Z : C}
(f : X ⟶ Y)
(g : Y ⟶ Z)
:
@[simp]
theorem
CategoryTheory.Abelian.Ext.mk₀_comp_mk₀_assoc
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Abelian C]
[CategoryTheory.HasExt C]
{X Y Z T : C}
(f : X ⟶ Y)
(g : Y ⟶ Z)
{n : ℕ}
(α : CategoryTheory.Abelian.Ext Z T n)
:
(CategoryTheory.Abelian.Ext.mk₀ f).comp ((CategoryTheory.Abelian.Ext.mk₀ g).comp α ⋯) ⋯ = (CategoryTheory.Abelian.Ext.mk₀ (CategoryTheory.CategoryStruct.comp f g)).comp α ⋯
The abelian group structure on Ext X Y n is defined by transporting the
abelian group structure on the constructed derived category
(given by HasDerivedCategory.standard). This constructed derived category
is used in order to obtain most of the compatibilities satisfied by
this abelian group structure. It is then shown that the bijection
homEquiv between Ext X Y n and Hom-types in the derived category
can be promoted to an additive equivalence for any [HasDerivedCategory C] instance.
noncomputable instance
CategoryTheory.Abelian.Ext.instAddCommGroup
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Abelian C]
[CategoryTheory.HasExt C]
{X Y : C}
{n : ℕ}
:
Equations
- CategoryTheory.Abelian.Ext.instAddCommGroup = CategoryTheory.Abelian.Ext.homEquiv.addCommGroup
@[reducible, inline]
noncomputable abbrev
CategoryTheory.Abelian.Ext.hom'
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Abelian C]
[CategoryTheory.HasExt C]
{X Y : C}
{n : ℕ}
(α : CategoryTheory.Abelian.Ext X Y n)
:
CategoryTheory.ShiftedHom ((DerivedCategory.singleFunctor C 0).obj X) ((DerivedCategory.singleFunctor C 0).obj Y) ↑n
The map from Ext X Y n to a ShiftedHom type in the constructed derived
category given by HasDerivedCategory.standard: this definition is introduced
only in order to prove properties of the abelian group structure on Ext-groups.
Do not use this definition: use the more general hom instead.
Equations
- α.hom' = α.hom
@[simp]
theorem
CategoryTheory.Abelian.Ext.add_comp
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Abelian C]
[CategoryTheory.HasExt C]
{X Y Z : C}
{n : ℕ}
(α₁ α₂ : CategoryTheory.Abelian.Ext X Y n)
{m : ℕ}
(β : CategoryTheory.Abelian.Ext Y Z m)
{p : ℕ}
(h : n + m = p)
:
@[simp]
theorem
CategoryTheory.Abelian.Ext.comp_add
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Abelian C]
[CategoryTheory.HasExt C]
{X Y Z : C}
{n : ℕ}
(α : CategoryTheory.Abelian.Ext X Y n)
{m : ℕ}
(β₁ β₂ : CategoryTheory.Abelian.Ext Y Z m)
{p : ℕ}
(h : n + m = p)
:
@[simp]
theorem
CategoryTheory.Abelian.Ext.neg_comp
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Abelian C]
[CategoryTheory.HasExt C]
{X Y Z : C}
{n : ℕ}
(α : CategoryTheory.Abelian.Ext X Y n)
{m : ℕ}
(β : CategoryTheory.Abelian.Ext Y Z m)
{p : ℕ}
(h : n + m = p)
:
@[simp]
theorem
CategoryTheory.Abelian.Ext.comp_neg
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Abelian C]
[CategoryTheory.HasExt C]
{X Y Z : C}
{n : ℕ}
(α : CategoryTheory.Abelian.Ext X Y n)
{m : ℕ}
(β : CategoryTheory.Abelian.Ext Y Z m)
{p : ℕ}
(h : n + m = p)
:
@[simp]
theorem
CategoryTheory.Abelian.Ext.zero_comp
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Abelian C]
[CategoryTheory.HasExt C]
(X : C)
{Y Z : C}
(n : ℕ)
{m : ℕ}
(β : CategoryTheory.Abelian.Ext Y Z m)
(p : ℕ)
(h : n + m = p)
:
CategoryTheory.Abelian.Ext.comp 0 β h = 0
@[simp]
theorem
CategoryTheory.Abelian.Ext.comp_zero
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Abelian C]
[CategoryTheory.HasExt C]
{X Y : C}
{n : ℕ}
(α : CategoryTheory.Abelian.Ext X Y n)
(Z : C)
(m p : ℕ)
(h : n + m = p)
:
α.comp 0 h = 0
@[simp]
theorem
CategoryTheory.Abelian.Ext.mk₀_id_comp
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Abelian C]
[CategoryTheory.HasExt C]
{X Y : C}
{n : ℕ}
(α : CategoryTheory.Abelian.Ext X Y n)
:
(CategoryTheory.Abelian.Ext.mk₀ (CategoryTheory.CategoryStruct.id X)).comp α ⋯ = α
@[simp]
theorem
CategoryTheory.Abelian.Ext.comp_mk₀_id
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Abelian C]
[CategoryTheory.HasExt C]
{X Y : C}
{n : ℕ}
(α : CategoryTheory.Abelian.Ext X Y n)
:
α.comp (CategoryTheory.Abelian.Ext.mk₀ (CategoryTheory.CategoryStruct.id Y)) ⋯ = α
@[simp]
theorem
CategoryTheory.Abelian.Ext.mk₀_zero
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Abelian C]
[CategoryTheory.HasExt C]
(X Y : C)
:
theorem
CategoryTheory.Abelian.Ext.biprod_ext
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Abelian C]
[CategoryTheory.HasExt C]
{Y : C}
{n : ℕ}
{X₁ X₂ : C}
{α β : CategoryTheory.Abelian.Ext (X₁ ⊞ X₂) Y n}
(h₁ :
(CategoryTheory.Abelian.Ext.mk₀ CategoryTheory.Limits.biprod.inl).comp α ⋯ = (CategoryTheory.Abelian.Ext.mk₀ CategoryTheory.Limits.biprod.inl).comp β ⋯)
(h₂ :
(CategoryTheory.Abelian.Ext.mk₀ CategoryTheory.Limits.biprod.inr).comp α ⋯ = (CategoryTheory.Abelian.Ext.mk₀ CategoryTheory.Limits.biprod.inr).comp β ⋯)
:
α = β
@[simp]
theorem
CategoryTheory.Abelian.Ext.zero_hom
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Abelian C]
[CategoryTheory.HasExt C]
(X Y : C)
(n : ℕ)
[HasDerivedCategory C]
:
@[simp]
theorem
CategoryTheory.Abelian.Ext.add_hom
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Abelian C]
[CategoryTheory.HasExt C]
{X Y : C}
{n : ℕ}
[HasDerivedCategory C]
(α β : CategoryTheory.Abelian.Ext X Y n)
:
theorem
CategoryTheory.Abelian.Ext.neg_hom
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Abelian C]
[CategoryTheory.HasExt C]
{X Y : C}
{n : ℕ}
[HasDerivedCategory C]
(α : CategoryTheory.Abelian.Ext X Y n)
:
noncomputable def
CategoryTheory.Abelian.Ext.homAddEquiv
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Abelian C]
[CategoryTheory.HasExt C]
{X Y : C}
[HasDerivedCategory C]
{n : ℕ}
:
CategoryTheory.Abelian.Ext X Y n ≃+ CategoryTheory.ShiftedHom ((DerivedCategory.singleFunctor C 0).obj X) ((DerivedCategory.singleFunctor C 0).obj Y) ↑n
When an instance of [HasDerivedCategory.{w'} C] is available, this is the additive
bijection between Ext.{w} X Y n and a type of morphisms in the derived category.
Equations
- CategoryTheory.Abelian.Ext.homAddEquiv = { toEquiv := CategoryTheory.Abelian.Ext.homEquiv, map_add' := ⋯ }
@[simp]
theorem
CategoryTheory.Abelian.Ext.homAddEquiv_apply
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Abelian C]
[CategoryTheory.HasExt C]
{X Y : C}
{n : ℕ}
[HasDerivedCategory C]
(α : CategoryTheory.Abelian.Ext X Y n)
:
CategoryTheory.Abelian.Ext.homAddEquiv α = α.hom
noncomputable def
CategoryTheory.Abelian.Ext.bilinearComp
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Abelian C]
[CategoryTheory.HasExt C]
(X Y Z : C)
(a b c : ℕ)
(h : a + b = c)
:
CategoryTheory.Abelian.Ext X Y a →+ CategoryTheory.Abelian.Ext Y Z b →+ CategoryTheory.Abelian.Ext X Z c
The composition of Ext, as a bilinear map.
Equations
- One or more equations did not get rendered due to their size.
@[simp]
theorem
CategoryTheory.Abelian.Ext.bilinearComp_apply_apply
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Abelian C]
[CategoryTheory.HasExt C]
(X Y Z : C)
(a b c : ℕ)
(h : a + b = c)
(α : CategoryTheory.Abelian.Ext X Y a)
(β : CategoryTheory.Abelian.Ext Y Z b)
:
((CategoryTheory.Abelian.Ext.bilinearComp X Y Z a b c h) α) β = α.comp β h
@[reducible, inline]
noncomputable abbrev
CategoryTheory.Abelian.Ext.postcomp
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Abelian C]
[CategoryTheory.HasExt C]
{Y Z : C}
{n : ℕ}
(β : CategoryTheory.Abelian.Ext Y Z n)
(X : C)
{a b : ℕ}
(h : a + n = b)
:
CategoryTheory.Abelian.Ext X Y a →+ CategoryTheory.Abelian.Ext X Z b
The postcomposition Ext X Y a →+ Ext X Z b with β : Ext Y Z n when a + n = b.
Equations
- β.postcomp X h = (CategoryTheory.Abelian.Ext.bilinearComp X Y Z a n b h).flip β
@[reducible, inline]
noncomputable abbrev
CategoryTheory.Abelian.Ext.precomp
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Abelian C]
[CategoryTheory.HasExt C]
{X Y : C}
{n : ℕ}
(α : CategoryTheory.Abelian.Ext X Y n)
(Z : C)
{a b : ℕ}
(h : n + a = b)
:
CategoryTheory.Abelian.Ext Y Z a →+ CategoryTheory.Abelian.Ext X Z b
The precomposition Ext Y Z a →+ Ext X Z b with α : Ext X Y n when n + a = b.
Equations
- α.precomp Z h = (CategoryTheory.Abelian.Ext.bilinearComp X Y Z n a b h) α
noncomputable def
CategoryTheory.Abelian.extFunctorObj
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Abelian C]
[CategoryTheory.HasExt C]
(X : C)
(n : ℕ)
:
Auxiliary definition for extFunctor.
Equations
- One or more equations did not get rendered due to their size.
@[simp]
theorem
CategoryTheory.Abelian.extFunctorObj_obj
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Abelian C]
[CategoryTheory.HasExt C]
(X : C)
(n : ℕ)
(Y : C)
:
(CategoryTheory.Abelian.extFunctorObj X n).obj Y = AddCommGrp.of (CategoryTheory.Abelian.Ext X Y n)
@[simp]
theorem
CategoryTheory.Abelian.extFunctorObj_map
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Abelian C]
[CategoryTheory.HasExt C]
(X : C)
(n : ℕ)
{X✝ Y✝ : C}
(f : X✝ ⟶ Y✝)
:
(CategoryTheory.Abelian.extFunctorObj X n).map f = AddCommGrp.ofHom ((CategoryTheory.Abelian.Ext.mk₀ f).postcomp X ⋯)
noncomputable def
CategoryTheory.Abelian.extFunctor
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Abelian C]
[CategoryTheory.HasExt C]
(n : ℕ)
:
The functor Cᵒᵖ ⥤ C ⥤ AddCommGrp which sends X : C and Y : C
to Ext X Y n.
Equations
- One or more equations did not get rendered due to their size.
@[simp]
theorem
CategoryTheory.Abelian.extFunctor_map_app
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Abelian C]
[CategoryTheory.HasExt C]
(n : ℕ)
{X₁ X₂ : Cᵒᵖ}
(f : X₁ ⟶ X₂)
(Y : C)
:
((CategoryTheory.Abelian.extFunctor n).map f).app Y = AddCommGrp.ofHom
(AddMonoidHom.mk'
(fun (α : CategoryTheory.Abelian.Ext (Opposite.unop X₁) Y n) => (CategoryTheory.Abelian.Ext.mk₀ f.unop).comp α ⋯)
⋯)
@[simp]
theorem
CategoryTheory.Abelian.extFunctor_obj
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Abelian C]
[CategoryTheory.HasExt C]
(n : ℕ)
(X : Cᵒᵖ)
: