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.

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 AddCommGrp.{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 AddCommGrp.{u} shall be in Type (u + 1), these types are going to be u-small. Then, for C := Sheaf X.etale AddCommGrp.{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.

@[reducible, inline]

abbrev CategoryTheory.HasExt (C : Type u) [Category.{v, u} C] [Abelian C] : Prop

The property that morphisms between single complexes in arbitrary degrees are w-small in the derived category.

theorem CategoryTheory.hasExt_iff (C : Type u) [Category.{v, u} C] [Abelian C] [HasDerivedCategory C] : HasExt C ↔ ∀ (X Y : C) (n : ℤ), 0 ≤ n → Small.{w, w'} ((DerivedCategory.singleFunctor C 0).obj X ⟶ (shiftFunctor (DerivedCategory C) n).obj ((DerivedCategory.singleFunctor C 0).obj Y))

theorem CategoryTheory.hasExt_of_hasDerivedCategory (C : Type u) [Category.{v, u} C] [Abelian C] [HasDerivedCategory C] : HasExt C

theorem CategoryTheory.HasExt.standard (C : Type u) [Category.{v, u} C] [Abelian C] : HasExt C

def CategoryTheory.Abelian.Ext {C : Type u} [Category.{v, u} C] [Abelian C] [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].

noncomputable def CategoryTheory.Abelian.Ext.comp {C : Type u} [Category.{v, u} C] [Abelian C] [HasExt C] {X Y Z : C} {a b : ℕ} (α : Ext X Y a) (β : Ext Y Z b) {c : ℕ} (h : a + b = c) : Ext X Z c

The composition of Ext.

theorem CategoryTheory.Abelian.Ext.comp_assoc {C : Type u} [Category.{v, u} C] [Abelian C] [HasExt C] {X Y Z T : C} {a₁ a₂ a₃ a₁₂ a₂₃ a : ℕ} (α : Ext X Y a₁) (β : Ext Y Z a₂) (γ : 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} [Category.{v, u} C] [Abelian C] [HasExt C] {X Y Z T : C} {a₁ a₃ a₁₃ : ℕ} (α : Ext X Y a₁) (β : Ext Y Z 0) (γ : 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} [Category.{v, u} C] [Abelian C] [HasExt C] {X Y Z T : C} {a₁ a₂ a₁₂ : ℕ} (α : Ext X Y a₁) (β : Ext Y Z a₂) (γ : Ext Z T 0) (h₁₂ : a₁ + a₂ = a₁₂) : (α.comp β h₁₂).comp γ ⋯ = α.comp (β.comp γ ⋯) h₁₂

noncomputable def CategoryTheory.Abelian.Ext.homEquiv {C : Type u} [Category.{v, u} C] [Abelian C] [HasExt C] {X Y : C} [HasDerivedCategory C] {n : ℕ} : Ext X Y n ≃ 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.

@[reducible, inline]

noncomputable abbrev CategoryTheory.Abelian.Ext.hom {C : Type u} [Category.{v, u} C] [Abelian C] [HasExt C] {X Y : C} [HasDerivedCategory C] {a : ℕ} (α : Ext X Y a) : 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.

@[simp]

theorem CategoryTheory.Abelian.Ext.comp_hom {C : Type u} [Category.{v, u} C] [Abelian C] [HasExt C] {X Y Z : C} [HasDerivedCategory C] {a b : ℕ} (α : Ext X Y a) (β : Ext Y Z b) {c : ℕ} (h : a + b = c) : (α.comp β h).hom = α.hom.comp β.hom ⋯

theorem CategoryTheory.Abelian.Ext.ext {C : Type u} [Category.{v, u} C] [Abelian C] [HasExt C] {X Y : C} [HasDerivedCategory C] {n : ℕ} {α β : Ext X Y n} (h : α.hom = β.hom) : α = β

theorem CategoryTheory.Abelian.Ext.ext_iff {C : Type u} [Category.{v, u} C] [Abelian C] [HasExt C] {X Y : C} [HasDerivedCategory C] {n : ℕ} {α β : Ext X Y n} : α = β ↔ α.hom = β.hom

noncomputable def CategoryTheory.Abelian.Ext.mk₀ {C : Type u} [Category.{v, u} C] [Abelian C] [HasExt C] {X Y : C} (f : X ⟶ Y) : Ext X Y 0

The canonical map (X ⟶ Y) → Ext X Y 0.

@[simp]

theorem CategoryTheory.Abelian.Ext.mk₀_hom {C : Type u} [Category.{v, u} C] [Abelian C] [HasExt C] {X Y : C} [HasDerivedCategory C] (f : X ⟶ Y) : (mk₀ f).hom = ShiftedHom.mk₀ ↑0 ⋯ ((DerivedCategory.singleFunctor C 0).map f)

@[simp]

theorem CategoryTheory.Abelian.Ext.mk₀_comp_mk₀ {C : Type u} [Category.{v, u} C] [Abelian C] [HasExt C] {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z) : (mk₀ f).comp (mk₀ g) ⋯ = mk₀ (CategoryStruct.comp f g)

@[simp]

theorem CategoryTheory.Abelian.Ext.mk₀_comp_mk₀_assoc {C : Type u} [Category.{v, u} C] [Abelian C] [HasExt C] {X Y Z T : C} (f : X ⟶ Y) (g : Y ⟶ Z) {n : ℕ} (α : Ext Z T n) : (mk₀ f).comp ((mk₀ g).comp α ⋯) ⋯ = (mk₀ (CategoryStruct.comp f g)).comp α ⋯

theorem CategoryTheory.Abelian.Ext.mk₀_bijective {C : Type u} [Category.{v, u} C] [Abelian C] [HasExt C] (X Y : C) : Function.Bijective mk₀

noncomputable def CategoryTheory.Abelian.Ext.homEquiv₀ {C : Type u} [Category.{v, u} C] [Abelian C] [HasExt C] {X Y : C} : Ext X Y 0 ≃ (X ⟶ Y)

The bijection Ext X Y 0 ≃ (X ⟶ Y).

@[simp]

theorem CategoryTheory.Abelian.Ext.homEquiv₀_symm_apply {C : Type u} [Category.{v, u} C] [Abelian C] [HasExt C] {X Y : C} (a✝ : X ⟶ Y) : homEquiv₀.symm a✝ = mk₀ a✝

@[simp]

theorem CategoryTheory.Abelian.Ext.mk₀_homEquiv₀_apply {C : Type u} [Category.{v, u} C] [Abelian C] [HasExt C] {X Y : C} (f : Ext X Y 0) : mk₀ (homEquiv₀ f) = f

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} [Category.{v, u} C] [Abelian C] [HasExt C] {X Y : C} {n : ℕ} : AddCommGroup (Ext X Y n)

@[reducible, inline]

noncomputable abbrev CategoryTheory.Abelian.Ext.hom' {C : Type u} [Category.{v, u} C] [Abelian C] [HasExt C] {X Y : C} {n : ℕ} (α : Ext X Y n) : 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.

@[simp]

theorem CategoryTheory.Abelian.Ext.add_comp {C : Type u} [Category.{v, u} C] [Abelian C] [HasExt C] {X Y Z : C} {n : ℕ} (α₁ α₂ : Ext X Y n) {m : ℕ} (β : Ext Y Z m) {p : ℕ} (h : n + m = p) : (α₁ + α₂).comp β h = α₁.comp β h + α₂.comp β h

@[simp]

theorem CategoryTheory.Abelian.Ext.comp_add {C : Type u} [Category.{v, u} C] [Abelian C] [HasExt C] {X Y Z : C} {n : ℕ} (α : Ext X Y n) {m : ℕ} (β₁ β₂ : Ext Y Z m) {p : ℕ} (h : n + m = p) : α.comp (β₁ + β₂) h = α.comp β₁ h + α.comp β₂ h

@[simp]

theorem CategoryTheory.Abelian.Ext.neg_comp {C : Type u} [Category.{v, u} C] [Abelian C] [HasExt C] {X Y Z : C} {n : ℕ} (α : Ext X Y n) {m : ℕ} (β : Ext Y Z m) {p : ℕ} (h : n + m = p) : (-α).comp β h = -α.comp β h

@[simp]

theorem CategoryTheory.Abelian.Ext.comp_neg {C : Type u} [Category.{v, u} C] [Abelian C] [HasExt C] {X Y Z : C} {n : ℕ} (α : Ext X Y n) {m : ℕ} (β : Ext Y Z m) {p : ℕ} (h : n + m = p) : α.comp (-β) h = -α.comp β h

@[simp]

theorem CategoryTheory.Abelian.Ext.zero_comp {C : Type u} [Category.{v, u} C] [Abelian C] [HasExt C] (X : C) {Y Z : C} (n : ℕ) {m : ℕ} (β : Ext Y Z m) (p : ℕ) (h : n + m = p) : comp 0 β h = 0

@[simp]

theorem CategoryTheory.Abelian.Ext.comp_zero {C : Type u} [Category.{v, u} C] [Abelian C] [HasExt C] {X Y : C} {n : ℕ} (α : 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} [Category.{v, u} C] [Abelian C] [HasExt C] {X Y : C} {n : ℕ} (α : Ext X Y n) : (mk₀ (CategoryStruct.id X)).comp α ⋯ = α

@[simp]

theorem CategoryTheory.Abelian.Ext.comp_mk₀_id {C : Type u} [Category.{v, u} C] [Abelian C] [HasExt C] {X Y : C} {n : ℕ} (α : Ext X Y n) : α.comp (mk₀ (CategoryStruct.id Y)) ⋯ = α

@[simp]

theorem CategoryTheory.Abelian.Ext.mk₀_zero {C : Type u} [Category.{v, u} C] [Abelian C] [HasExt C] (X Y : C) : mk₀ 0 = 0

theorem CategoryTheory.Abelian.Ext.mk₀_add {C : Type u} [Category.{v, u} C] [Abelian C] [HasExt C] {X Y : C} (f g : X ⟶ Y) : mk₀ (f + g) = mk₀ f + mk₀ g

noncomputable def CategoryTheory.Abelian.Ext.addEquiv₀ {C : Type u} [Category.{v, u} C] [Abelian C] [HasExt C] {X Y : C} : Ext X Y 0 ≃+ (X ⟶ Y)

The additive bijection Ext X Y 0 ≃+ (X ⟶ Y).

@[simp]

theorem CategoryTheory.Abelian.Ext.addEquiv₀_symm_apply {C : Type u} [Category.{v, u} C] [Abelian C] [HasExt C] {X Y : C} (a✝ : X ⟶ Y) : addEquiv₀.symm a✝ = mk₀ a✝

@[simp]

theorem CategoryTheory.Abelian.Ext.mk₀_addEquiv₀_apply {C : Type u} [Category.{v, u} C] [Abelian C] [HasExt C] {X Y : C} (f : Ext X Y 0) : mk₀ (addEquiv₀ f) = f

theorem CategoryTheory.Abelian.Ext.biprod_ext {C : Type u} [Category.{v, u} C] [Abelian C] [HasExt C] {Y : C} {n : ℕ} {X₁ X₂ : C} {α β : Ext (X₁ ⊞ X₂) Y n} (h₁ : (mk₀ Limits.biprod.inl).comp α ⋯ = (mk₀ Limits.biprod.inl).comp β ⋯) (h₂ : (mk₀ Limits.biprod.inr).comp α ⋯ = (mk₀ Limits.biprod.inr).comp β ⋯) : α = β

@[simp]

theorem CategoryTheory.Abelian.Ext.zero_hom {C : Type u} [Category.{v, u} C] [Abelian C] [HasExt C] (X Y : C) (n : ℕ) [HasDerivedCategory C] : hom 0 = 0

@[simp]

theorem CategoryTheory.Abelian.Ext.add_hom {C : Type u} [Category.{v, u} C] [Abelian C] [HasExt C] {X Y : C} {n : ℕ} [HasDerivedCategory C] (α β : Ext X Y n) : (α + β).hom = α.hom + β.hom

theorem CategoryTheory.Abelian.Ext.neg_hom {C : Type u} [Category.{v, u} C] [Abelian C] [HasExt C] {X Y : C} {n : ℕ} [HasDerivedCategory C] (α : Ext X Y n) : (-α).hom = -α.hom

noncomputable def CategoryTheory.Abelian.Ext.homAddEquiv {C : Type u} [Category.{v, u} C] [Abelian C] [HasExt C] {X Y : C} [HasDerivedCategory C] {n : ℕ} : Ext X Y n ≃+ 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.

@[simp]

theorem CategoryTheory.Abelian.Ext.homAddEquiv_apply {C : Type u} [Category.{v, u} C] [Abelian C] [HasExt C] {X Y : C} {n : ℕ} [HasDerivedCategory C] (α : Ext X Y n) : homAddEquiv α = α.hom

noncomputable def CategoryTheory.Abelian.Ext.bilinearComp {C : Type u} [Category.{v, u} C] [Abelian C] [HasExt C] (X Y Z : C) (a b c : ℕ) (h : a + b = c) : Ext X Y a →+ Ext Y Z b →+ Ext X Z c

The composition of Ext, as a bilinear map.

@[simp]

theorem CategoryTheory.Abelian.Ext.bilinearComp_apply_apply {C : Type u} [Category.{v, u} C] [Abelian C] [HasExt C] (X Y Z : C) (a b c : ℕ) (h : a + b = c) (α : Ext X Y a) (β : Ext Y Z b) : ((bilinearComp X Y Z a b c h) α) β = α.comp β h

@[reducible, inline]

noncomputable abbrev CategoryTheory.Abelian.Ext.postcomp {C : Type u} [Category.{v, u} C] [Abelian C] [HasExt C] {Y Z : C} {n : ℕ} (β : Ext Y Z n) (X : C) {a b : ℕ} (h : a + n = b) : Ext X Y a →+ Ext X Z b

The postcomposition Ext X Y a →+ Ext X Z b with β : Ext Y Z n when a + n = b.

@[reducible, inline]

noncomputable abbrev CategoryTheory.Abelian.Ext.precomp {C : Type u} [Category.{v, u} C] [Abelian C] [HasExt C] {X Y : C} {n : ℕ} (α : Ext X Y n) (Z : C) {a b : ℕ} (h : n + a = b) : Ext Y Z a →+ Ext X Z b

The precomposition Ext Y Z a →+ Ext X Z b with α : Ext X Y n when n + a = b.

noncomputable def CategoryTheory.Abelian.extFunctorObj {C : Type u} [Category.{v, u} C] [Abelian C] [HasExt C] (X : C) (n : ℕ) : Functor C AddCommGrp

Auxiliary definition for extFunctor.

@[simp]

theorem CategoryTheory.Abelian.extFunctorObj_map {C : Type u} [Category.{v, u} C] [Abelian C] [HasExt C] (X : C) (n : ℕ) {X✝ Y✝ : C} (f : X✝ ⟶ Y✝) : (extFunctorObj X n).map f = AddCommGrp.ofHom ((Ext.mk₀ f).postcomp X ⋯)

@[simp]

theorem CategoryTheory.Abelian.extFunctorObj_obj_coe {C : Type u} [Category.{v, u} C] [Abelian C] [HasExt C] (X : C) (n : ℕ) (Y : C) : ↑((extFunctorObj X n).obj Y) = Ext X Y n

noncomputable def CategoryTheory.Abelian.extFunctor {C : Type u} [Category.{v, u} C] [Abelian C] [HasExt C] (n : ℕ) : Functor Cᵒᵖ (Functor C AddCommGrp)

The functor Cᵒᵖ ⥤ C ⥤ AddCommGrp which sends X : C and Y : C to Ext X Y n.

@[simp]

theorem CategoryTheory.Abelian.extFunctor_obj {C : Type u} [Category.{v, u} C] [Abelian C] [HasExt C] (n : ℕ) (X : Cᵒᵖ) : (extFunctor n).obj X = extFunctorObj (Opposite.unop X) n

@[simp]

theorem CategoryTheory.Abelian.extFunctor_map_app {C : Type u} [Category.{v, u} C] [Abelian C] [HasExt C] (n : ℕ) {X₁ X₂ : Cᵒᵖ} (f : X₁ ⟶ X₂) (Y : C) : ((extFunctor n).map f).app Y = AddCommGrp.ofHom (AddMonoidHom.mk' (fun (α : Ext (Opposite.unop X₁) Y n) => (Ext.mk₀ f.unop).comp α ⋯) ⋯)

instance CategoryTheory.Abelian.instAdditiveAddCommGrpExtFunctorObj {C : Type u} [Category.{v, u} C] [Abelian C] [HasExt C] (X : C) (n : ℕ) : (extFunctorObj X n).Additive

instance CategoryTheory.Abelian.instAdditiveOppositeFunctorAddCommGrpExtFunctor {C : Type u} [Category.{v, u} C] [Abelian C] [HasExt C] (n : ℕ) : (extFunctor n).Additive

theorem CategoryTheory.Abelian.Ext.comp_sum {C : Type u} [Category.{v, u} C] [Abelian C] [HasExt C] {X Y Z : C} {p : ℕ} (α : Ext X Y p) {ι : Type u_1} [Fintype ι] {q : ℕ} (β : ι → Ext Y Z q) {n : ℕ} (h : p + q = n) : α.comp (∑ i : ι, β i) h = ∑ i : ι, α.comp (β i) h

theorem CategoryTheory.Abelian.Ext.sum_comp {C : Type u} [Category.{v, u} C] [Abelian C] [HasExt C] {X Y Z : C} {p : ℕ} {ι : Type u_1} [Fintype ι] (α : ι → Ext X Y p) {q : ℕ} (β : Ext Y Z q) {n : ℕ} (h : p + q = n) : (∑ i : ι, α i).comp β h = ∑ i : ι, (α i).comp β h

theorem CategoryTheory.Abelian.Ext.mk₀_sum {C : Type u} [Category.{v, u} C] [Abelian C] [HasExt C] {X Y : C} {ι : Type u_1} [Fintype ι] (f : ι → (X ⟶ Y)) : mk₀ (∑ i : ι, f i) = ∑ i : ι, mk₀ (f i)

noncomputable def CategoryTheory.Abelian.Ext.biproductAddEquiv {C : Type u} [Category.{v, u} C] [Abelian C] [HasExt C] {J : Type u_1} [Fintype J] {X : J → C} {c : Limits.Bicone X} (hc : c.IsBilimit) (Y : C) (n : ℕ) : Ext c.pt Y n ≃+ ((i : J) → Ext (X i) Y n)

Ext commutes with biproducts in its first variable.

noncomputable def CategoryTheory.Abelian.Ext.addEquivBiproduct {C : Type u} [Category.{v, u} C] [Abelian C] [HasExt C] (X : C) {J : Type u_1} [Fintype J] {Y : J → C} {c : Limits.Bicone Y} (hc : c.IsBilimit) (n : ℕ) : Ext X c.pt n ≃+ ((i : J) → Ext X (Y i) n)

Ext commutes with biproducts in its second variable.

noncomputable def CategoryTheory.Abelian.Ext.chgUniv {C : Type u} [Category.{v, u} C] [Abelian C] [HasExt C] [HasExt C] {X Y : C} {n : ℕ} : Ext X Y n ≃ Ext X Y n

Up to an equivalence, the type Ext.{w} X Y n does not depend on the universe w.

theorem CategoryTheory.Abelian.Ext.homEquiv_chgUniv {C : Type u} [Category.{v, u} C] [Abelian C] [HasExt C] [HasExt C] {X Y : C} {n : ℕ} [HasDerivedCategory C] (e : Ext X Y n) : homEquiv (chgUniv e) = homEquiv e

theorem CategoryTheory.hasExt_iff_small_ext (C : Type u) [Category.{v, u} C] [Abelian C] [HasExt C] : HasExt C ↔ ∀ (X Y : C) (n : ℕ), Small.{w', w} (Abelian.Ext X Y n)