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

• construct the additive structure on Ext
• compute Ext X Y 0
• define the class in Ext S.X₃ S.X₁ 1 of a short exact short complex S
• construct the long exact sequences of Ext.

@[reducible, inline]

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

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] : CategoryTheory.HasExt C

def CategoryTheory.Abelian.Ext {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [CategoryTheory.HasExt C] (X : C) (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 : C} {Y : C} {Z : C} {a : ℕ} {b : ℕ} (α : CategoryTheory.Abelian.Ext X Y a) (β : CategoryTheory.Abelian.Ext Y Z b) {c : ℕ} (h : a + b = c) : CategoryTheory.Abelian.Ext X Z 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 : C} {Y : C} {Z : C} {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₂₃) ⋯

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