Abelian categories with enough injectives have injective resolutions

Main results

When the underlying category is abelian:

• CategoryTheory.InjectiveResolution.desc: Given I : InjectiveResolution X and J : InjectiveResolution Y, any morphism X ⟶ Y admits a descent to a chain map J.cocomplex ⟶ I.cocomplex. It is a descent in the sense that I.ι intertwines the descent and the original morphism, see CategoryTheory.InjectiveResolution.desc_commutes.

• CategoryTheory.InjectiveResolution.descHomotopy: Any two such descents are homotopic.

• CategoryTheory.InjectiveResolution.homotopyEquiv: Any two injective resolutions of the same object are homotopy equivalent.

• CategoryTheory.injectiveResolutions: If every object admits an injective resolution, we can construct a functor injectiveResolutions C : C ⥤ HomotopyCategory C.

• CategoryTheory.exact_f_d: f and Injective.d f are exact.

• CategoryTheory.InjectiveResolution.of: Hence, starting from a monomorphism X ⟶ J, where J is injective, we can apply Injective.d repeatedly to obtain an injective resolution of X.

def CategoryTheory.InjectiveResolution.descFZero {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasZeroMorphisms C] {Y : C} {Z : C} (f : Z ⟶ Y) (I : CategoryTheory.InjectiveResolution Y) (J : CategoryTheory.InjectiveResolution Z) : J.cocomplex.X 0 ⟶ I.cocomplex.X 0

Auxiliary construction for desc.

Equations

• CategoryTheory.InjectiveResolution.descFZero f I J = CategoryTheory.Injective.factorThru (CategoryTheory.CategoryStruct.comp f (I.ι.f 0)) (J.ι.f 0)

theorem CategoryTheory.InjectiveResolution.exact₀ {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] {Z : C} (I : CategoryTheory.InjectiveResolution Z) : CategoryTheory.ShortComplex.Exact (CategoryTheory.ShortComplex.mk (I.ι.f 0) (I.cocomplex.d 0 1) (_ : CategoryTheory.CategoryStruct.comp (I.ι.f 0) (I.cocomplex.d 0 1) = 0))

def CategoryTheory.InjectiveResolution.descFOne {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] {Y : C} {Z : C} (f : Z ⟶ Y) (I : CategoryTheory.InjectiveResolution Y) (J : CategoryTheory.InjectiveResolution Z) : J.cocomplex.X 1 ⟶ I.cocomplex.X 1

Auxiliary construction for desc.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem CategoryTheory.InjectiveResolution.descFOne_zero_comm {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] {Y : C} {Z : C} (f : Z ⟶ Y) (I : CategoryTheory.InjectiveResolution Y) (J : CategoryTheory.InjectiveResolution Z) : CategoryTheory.CategoryStruct.comp (J.cocomplex.d 0 1) (CategoryTheory.InjectiveResolution.descFOne f I J) = CategoryTheory.CategoryStruct.comp (CategoryTheory.InjectiveResolution.descFZero f I J) (I.cocomplex.d 0 1)

def CategoryTheory.InjectiveResolution.descFSucc {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] {Y : C} {Z : C} (I : CategoryTheory.InjectiveResolution Y) (J : CategoryTheory.InjectiveResolution Z) (n : ℕ) (g : J.cocomplex.X n ⟶ I.cocomplex.X n) (g' : J.cocomplex.X (n + 1) ⟶ I.cocomplex.X (n + 1)) (w : CategoryTheory.CategoryStruct.comp (J.cocomplex.d n (n + 1)) g' = CategoryTheory.CategoryStruct.comp g (I.cocomplex.d n (n + 1))) : (g'' : J.cocomplex.X (n + 2) ⟶ I.cocomplex.X (n + 2)) ×' CategoryTheory.CategoryStruct.comp (J.cocomplex.d (n + 1) (n + 2)) g'' = CategoryTheory.CategoryStruct.comp g' (I.cocomplex.d (n + 1) (n + 2))

Auxiliary construction for desc.

Equations

• One or more equations did not get rendered due to their size.

def CategoryTheory.InjectiveResolution.desc {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] {Y : C} {Z : C} (f : Z ⟶ Y) (I : CategoryTheory.InjectiveResolution Y) (J : CategoryTheory.InjectiveResolution Z) : J.cocomplex ⟶ I.cocomplex

A morphism in C descends to a chain map between injective resolutions.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem CategoryTheory.InjectiveResolution.desc_commutes_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] {Y : C} {Z : C} (f : Z✝ ⟶ Y) (I : CategoryTheory.InjectiveResolution Y) (J : CategoryTheory.InjectiveResolution Z✝) {Z : CochainComplex C ℕ} (h : I.cocomplex ⟶ Z) : CategoryTheory.CategoryStruct.comp J.ι (CategoryTheory.CategoryStruct.comp (CategoryTheory.InjectiveResolution.desc f I J) h) = CategoryTheory.CategoryStruct.comp ((CochainComplex.single₀ C).toPrefunctor.map f) (CategoryTheory.CategoryStruct.comp I.ι h)

@[simp]

theorem CategoryTheory.InjectiveResolution.desc_commutes {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] {Y : C} {Z : C} (f : Z ⟶ Y) (I : CategoryTheory.InjectiveResolution Y) (J : CategoryTheory.InjectiveResolution Z) : CategoryTheory.CategoryStruct.comp J.ι (CategoryTheory.InjectiveResolution.desc f I J) = CategoryTheory.CategoryStruct.comp ((CochainComplex.single₀ C).toPrefunctor.map f) I.ι

The resolution maps intertwine the descent of a morphism and that morphism.

@[simp]

theorem CategoryTheory.InjectiveResolution.desc_commutes_zero_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] {Y : C} {Z : C} (f : Z✝ ⟶ Y) (I : CategoryTheory.InjectiveResolution Y) (J : CategoryTheory.InjectiveResolution Z✝) {Z : C} (h : I.cocomplex.X 0 ⟶ Z) : CategoryTheory.CategoryStruct.comp (J.ι.f 0) (CategoryTheory.CategoryStruct.comp ((CategoryTheory.InjectiveResolution.desc f I J).f 0) h) = CategoryTheory.CategoryStruct.comp f (CategoryTheory.CategoryStruct.comp (I.ι.f 0) h)

@[simp]

theorem CategoryTheory.InjectiveResolution.desc_commutes_zero {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] {Y : C} {Z : C} (f : Z ⟶ Y) (I : CategoryTheory.InjectiveResolution Y) (J : CategoryTheory.InjectiveResolution Z) : CategoryTheory.CategoryStruct.comp (J.ι.f 0) ((CategoryTheory.InjectiveResolution.desc f I J).f 0) = CategoryTheory.CategoryStruct.comp f (I.ι.f 0)

def CategoryTheory.InjectiveResolution.descHomotopyZeroZero {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] {Y : C} {Z : C} {I : CategoryTheory.InjectiveResolution Y} {J : CategoryTheory.InjectiveResolution Z} (f : I.cocomplex ⟶ J.cocomplex) (comm : CategoryTheory.CategoryStruct.comp I.ι f = 0) : I.cocomplex.X 1 ⟶ J.cocomplex.X 0

An auxiliary definition for descHomotopyZero.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem CategoryTheory.InjectiveResolution.comp_descHomotopyZeroZero_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] {Y : C} {Z : C} {I : CategoryTheory.InjectiveResolution Y} {J : CategoryTheory.InjectiveResolution Z✝} (f : I.cocomplex ⟶ J.cocomplex) (comm : CategoryTheory.CategoryStruct.comp I.ι f = 0) {Z : C} (h : J.cocomplex.X 0 ⟶ Z) : CategoryTheory.CategoryStruct.comp (I.cocomplex.d 0 1) (CategoryTheory.CategoryStruct.comp (CategoryTheory.InjectiveResolution.descHomotopyZeroZero f comm) h) = CategoryTheory.CategoryStruct.comp (f.f 0) h

@[simp]

theorem CategoryTheory.InjectiveResolution.comp_descHomotopyZeroZero {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] {Y : C} {Z : C} {I : CategoryTheory.InjectiveResolution Y} {J : CategoryTheory.InjectiveResolution Z} (f : I.cocomplex ⟶ J.cocomplex) (comm : CategoryTheory.CategoryStruct.comp I.ι f = 0) : CategoryTheory.CategoryStruct.comp (I.cocomplex.d 0 1) (CategoryTheory.InjectiveResolution.descHomotopyZeroZero f comm) = f.f 0

def CategoryTheory.InjectiveResolution.descHomotopyZeroOne {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] {Y : C} {Z : C} {I : CategoryTheory.InjectiveResolution Y} {J : CategoryTheory.InjectiveResolution Z} (f : I.cocomplex ⟶ J.cocomplex) (comm : CategoryTheory.CategoryStruct.comp I.ι f = 0) : I.cocomplex.X 2 ⟶ J.cocomplex.X 1

An auxiliary definition for descHomotopyZero.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem CategoryTheory.InjectiveResolution.comp_descHomotopyZeroOne_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] {Y : C} {Z : C} {I : CategoryTheory.InjectiveResolution Y} {J : CategoryTheory.InjectiveResolution Z✝} (f : I.cocomplex ⟶ J.cocomplex) (comm : CategoryTheory.CategoryStruct.comp I.ι f = 0) {Z : C} (h : J.cocomplex.X 1 ⟶ Z) : CategoryTheory.CategoryStruct.comp (I.cocomplex.d 1 2) (CategoryTheory.CategoryStruct.comp (CategoryTheory.InjectiveResolution.descHomotopyZeroOne f comm) h) = CategoryTheory.CategoryStruct.comp (f.f 1 - CategoryTheory.CategoryStruct.comp (CategoryTheory.InjectiveResolution.descHomotopyZeroZero f comm) (J.cocomplex.d 0 1)) h

@[simp]

theorem CategoryTheory.InjectiveResolution.comp_descHomotopyZeroOne {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] {Y : C} {Z : C} {I : CategoryTheory.InjectiveResolution Y} {J : CategoryTheory.InjectiveResolution Z} (f : I.cocomplex ⟶ J.cocomplex) (comm : CategoryTheory.CategoryStruct.comp I.ι f = 0) : CategoryTheory.CategoryStruct.comp (I.cocomplex.d 1 2) (CategoryTheory.InjectiveResolution.descHomotopyZeroOne f comm) = f.f 1 - CategoryTheory.CategoryStruct.comp (CategoryTheory.InjectiveResolution.descHomotopyZeroZero f comm) (J.cocomplex.d 0 1)

def CategoryTheory.InjectiveResolution.descHomotopyZeroSucc {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] {Y : C} {Z : C} {I : CategoryTheory.InjectiveResolution Y} {J : CategoryTheory.InjectiveResolution Z} (f : I.cocomplex ⟶ J.cocomplex) (n : ℕ) (g : I.cocomplex.X (n + 1) ⟶ J.cocomplex.X n) (g' : I.cocomplex.X (n + 2) ⟶ J.cocomplex.X (n + 1)) (w : f.f (n + 1) = CategoryTheory.CategoryStruct.comp (I.cocomplex.d (n + 1) (n + 2)) g' + CategoryTheory.CategoryStruct.comp g (J.cocomplex.d n (n + 1))) : I.cocomplex.X (n + 3) ⟶ J.cocomplex.X (n + 2)

An auxiliary definition for descHomotopyZero.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem CategoryTheory.InjectiveResolution.comp_descHomotopyZeroSucc_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] {Y : C} {Z : C} {I : CategoryTheory.InjectiveResolution Y} {J : CategoryTheory.InjectiveResolution Z✝} (f : I.cocomplex ⟶ J.cocomplex) (n : ℕ) (g : I.cocomplex.X (n + 1) ⟶ J.cocomplex.X n) (g' : I.cocomplex.X (n + 2) ⟶ J.cocomplex.X (n + 1)) (w : f.f (n + 1) = CategoryTheory.CategoryStruct.comp (I.cocomplex.d (n + 1) (n + 2)) g' + CategoryTheory.CategoryStruct.comp g (J.cocomplex.d n (n + 1))) {Z : C} (h : J.cocomplex.X (n + 2) ⟶ Z) : CategoryTheory.CategoryStruct.comp (I.cocomplex.d (n + 2) (n + 3)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.InjectiveResolution.descHomotopyZeroSucc f n g g' w) h) = CategoryTheory.CategoryStruct.comp (f.f (n + 2) - CategoryTheory.CategoryStruct.comp g' (J.cocomplex.d (n + 1) (n + 2))) h

@[simp]

theorem CategoryTheory.InjectiveResolution.comp_descHomotopyZeroSucc {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] {Y : C} {Z : C} {I : CategoryTheory.InjectiveResolution Y} {J : CategoryTheory.InjectiveResolution Z} (f : I.cocomplex ⟶ J.cocomplex) (n : ℕ) (g : I.cocomplex.X (n + 1) ⟶ J.cocomplex.X n) (g' : I.cocomplex.X (n + 2) ⟶ J.cocomplex.X (n + 1)) (w : f.f (n + 1) = CategoryTheory.CategoryStruct.comp (I.cocomplex.d (n + 1) (n + 2)) g' + CategoryTheory.CategoryStruct.comp g (J.cocomplex.d n (n + 1))) : CategoryTheory.CategoryStruct.comp (I.cocomplex.d (n + 2) (n + 3)) (CategoryTheory.InjectiveResolution.descHomotopyZeroSucc f n g g' w) = f.f (n + 2) - CategoryTheory.CategoryStruct.comp g' (J.cocomplex.d (n + 1) (n + 2))

def CategoryTheory.InjectiveResolution.descHomotopyZero {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] {Y : C} {Z : C} {I : CategoryTheory.InjectiveResolution Y} {J : CategoryTheory.InjectiveResolution Z} (f : I.cocomplex ⟶ J.cocomplex) (comm : CategoryTheory.CategoryStruct.comp I.ι f = 0) : Homotopy f 0

Any descent of the zero morphism is homotopic to zero.

Equations

• One or more equations did not get rendered due to their size.

def CategoryTheory.InjectiveResolution.descHomotopy {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] {Y : C} {Z : C} (f : Y ⟶ Z) {I : CategoryTheory.InjectiveResolution Y} {J : CategoryTheory.InjectiveResolution Z} (g : I.cocomplex ⟶ J.cocomplex) (h : I.cocomplex ⟶ J.cocomplex) (g_comm : CategoryTheory.CategoryStruct.comp I.ι g = CategoryTheory.CategoryStruct.comp ((CochainComplex.single₀ C).toPrefunctor.map f) J.ι) (h_comm : CategoryTheory.CategoryStruct.comp I.ι h = CategoryTheory.CategoryStruct.comp ((CochainComplex.single₀ C).toPrefunctor.map f) J.ι) : Homotopy g h

Two descents of the same morphism are homotopic.

Equations

• One or more equations did not get rendered due to their size.

def CategoryTheory.InjectiveResolution.descIdHomotopy {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] (X : C) (I : CategoryTheory.InjectiveResolution X) : Homotopy (CategoryTheory.InjectiveResolution.desc (CategoryTheory.CategoryStruct.id X) I I) (CategoryTheory.CategoryStruct.id I.cocomplex)

The descent of the identity morphism is homotopic to the identity cochain map.

Equations

• One or more equations did not get rendered due to their size.

def CategoryTheory.InjectiveResolution.descCompHomotopy {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] {X : C} {Y : C} {Z : C} (f : X ⟶ Y) (g : Y ⟶ Z) (I : CategoryTheory.InjectiveResolution X) (J : CategoryTheory.InjectiveResolution Y) (K : CategoryTheory.InjectiveResolution Z) : Homotopy (CategoryTheory.InjectiveResolution.desc (CategoryTheory.CategoryStruct.comp f g) K I) (CategoryTheory.CategoryStruct.comp (CategoryTheory.InjectiveResolution.desc f J I) (CategoryTheory.InjectiveResolution.desc g K J))

The descent of a composition is homotopic to the composition of the descents.

Equations

• One or more equations did not get rendered due to their size.

def CategoryTheory.InjectiveResolution.homotopyEquiv {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] {X : C} (I : CategoryTheory.InjectiveResolution X) (J : CategoryTheory.InjectiveResolution X) : HomotopyEquiv I.cocomplex J.cocomplex

Any two injective resolutions are homotopy equivalent.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem CategoryTheory.InjectiveResolution.homotopyEquiv_hom_ι_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] {X : C} (I : CategoryTheory.InjectiveResolution X) (J : CategoryTheory.InjectiveResolution X) {Z : CochainComplex C ℕ} (h : J.cocomplex ⟶ Z) : CategoryTheory.CategoryStruct.comp I.ι (CategoryTheory.CategoryStruct.comp (CategoryTheory.InjectiveResolution.homotopyEquiv I J).hom h) = CategoryTheory.CategoryStruct.comp J.ι h

@[simp]

theorem CategoryTheory.InjectiveResolution.homotopyEquiv_hom_ι {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] {X : C} (I : CategoryTheory.InjectiveResolution X) (J : CategoryTheory.InjectiveResolution X) : CategoryTheory.CategoryStruct.comp I.ι (CategoryTheory.InjectiveResolution.homotopyEquiv I J).hom = J.ι

@[simp]

theorem CategoryTheory.InjectiveResolution.homotopyEquiv_inv_ι_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] {X : C} (I : CategoryTheory.InjectiveResolution X) (J : CategoryTheory.InjectiveResolution X) {Z : CochainComplex C ℕ} (h : I.cocomplex ⟶ Z) : CategoryTheory.CategoryStruct.comp J.ι (CategoryTheory.CategoryStruct.comp (CategoryTheory.InjectiveResolution.homotopyEquiv I J).inv h) = CategoryTheory.CategoryStruct.comp I.ι h

@[simp]

theorem CategoryTheory.InjectiveResolution.homotopyEquiv_inv_ι {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] {X : C} (I : CategoryTheory.InjectiveResolution X) (J : CategoryTheory.InjectiveResolution X) : CategoryTheory.CategoryStruct.comp J.ι (CategoryTheory.InjectiveResolution.homotopyEquiv I J).inv = I.ι

@[inline, reducible]

abbrev CategoryTheory.injectiveResolution {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] (Z : C) [CategoryTheory.HasInjectiveResolution Z] : CategoryTheory.InjectiveResolution Z

An arbitrarily chosen injective resolution of an object.

Equations

• CategoryTheory.injectiveResolution Z = Nonempty.some (_ : Nonempty (CategoryTheory.InjectiveResolution Z))

def CategoryTheory.injectiveResolutions (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [CategoryTheory.HasInjectiveResolutions C] : CategoryTheory.Functor C (HomotopyCategory C (ComplexShape.up ℕ))

Taking injective resolutions is functorial, if considered with target the homotopy category (ℕ-indexed cochain complexes and chain maps up to homotopy).

Equations

• One or more equations did not get rendered due to their size.

def CategoryTheory.InjectiveResolution.iso {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [CategoryTheory.HasInjectiveResolutions C] {X : C} (I : CategoryTheory.InjectiveResolution X) : (CategoryTheory.injectiveResolutions C).toPrefunctor.obj X ≅ (HomotopyCategory.quotient C (ComplexShape.up ℕ)).toPrefunctor.obj I.cocomplex

If I : InjectiveResolution X, then the chosen (injectiveResolutions C).obj X is isomorphic (in the homotopy category) to I.cocomplex.

Equations

• CategoryTheory.InjectiveResolution.iso I = HomotopyCategory.isoOfHomotopyEquiv (CategoryTheory.InjectiveResolution.homotopyEquiv (CategoryTheory.injectiveResolution X) I)

theorem CategoryTheory.InjectiveResolution.iso_hom_naturality_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [CategoryTheory.HasInjectiveResolutions C] {X : C} {Y : C} (f : X ⟶ Y) (I : CategoryTheory.InjectiveResolution X) (J : CategoryTheory.InjectiveResolution Y) (φ : I.cocomplex ⟶ J.cocomplex) (comm : CategoryTheory.CategoryStruct.comp (I.ι.f 0) (φ.f 0) = CategoryTheory.CategoryStruct.comp f (J.ι.f 0)) {Z : HomotopyCategory C (ComplexShape.up ℕ)} (h : (HomotopyCategory.quotient C (ComplexShape.up ℕ)).toPrefunctor.obj J.cocomplex ⟶ Z) : CategoryTheory.CategoryStruct.comp ((CategoryTheory.injectiveResolutions C).toPrefunctor.map f) (CategoryTheory.CategoryStruct.comp (CategoryTheory.InjectiveResolution.iso J).hom h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.InjectiveResolution.iso I).hom (CategoryTheory.CategoryStruct.comp ((HomotopyCategory.quotient C (ComplexShape.up ℕ)).toPrefunctor.map φ) h)

theorem CategoryTheory.InjectiveResolution.iso_hom_naturality {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [CategoryTheory.HasInjectiveResolutions C] {X : C} {Y : C} (f : X ⟶ Y) (I : CategoryTheory.InjectiveResolution X) (J : CategoryTheory.InjectiveResolution Y) (φ : I.cocomplex ⟶ J.cocomplex) (comm : CategoryTheory.CategoryStruct.comp (I.ι.f 0) (φ.f 0) = CategoryTheory.CategoryStruct.comp f (J.ι.f 0)) : CategoryTheory.CategoryStruct.comp ((CategoryTheory.injectiveResolutions C).toPrefunctor.map f) (CategoryTheory.InjectiveResolution.iso J).hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.InjectiveResolution.iso I).hom ((HomotopyCategory.quotient C (ComplexShape.up ℕ)).toPrefunctor.map φ)

theorem CategoryTheory.InjectiveResolution.iso_inv_naturality_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [CategoryTheory.HasInjectiveResolutions C] {X : C} {Y : C} (f : X ⟶ Y) (I : CategoryTheory.InjectiveResolution X) (J : CategoryTheory.InjectiveResolution Y) (φ : I.cocomplex ⟶ J.cocomplex) (comm : CategoryTheory.CategoryStruct.comp (I.ι.f 0) (φ.f 0) = CategoryTheory.CategoryStruct.comp f (J.ι.f 0)) {Z : HomotopyCategory C (ComplexShape.up ℕ)} (h : (CategoryTheory.injectiveResolutions C).toPrefunctor.obj Y ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.InjectiveResolution.iso I).inv (CategoryTheory.CategoryStruct.comp ((CategoryTheory.injectiveResolutions C).toPrefunctor.map f) h) = CategoryTheory.CategoryStruct.comp ((HomotopyCategory.quotient C (ComplexShape.up ℕ)).toPrefunctor.map φ) (CategoryTheory.CategoryStruct.comp (CategoryTheory.InjectiveResolution.iso J).inv h)

theorem CategoryTheory.InjectiveResolution.iso_inv_naturality {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [CategoryTheory.HasInjectiveResolutions C] {X : C} {Y : C} (f : X ⟶ Y) (I : CategoryTheory.InjectiveResolution X) (J : CategoryTheory.InjectiveResolution Y) (φ : I.cocomplex ⟶ J.cocomplex) (comm : CategoryTheory.CategoryStruct.comp (I.ι.f 0) (φ.f 0) = CategoryTheory.CategoryStruct.comp f (J.ι.f 0)) : CategoryTheory.CategoryStruct.comp (CategoryTheory.InjectiveResolution.iso I).inv ((CategoryTheory.injectiveResolutions C).toPrefunctor.map f) = CategoryTheory.CategoryStruct.comp ((HomotopyCategory.quotient C (ComplexShape.up ℕ)).toPrefunctor.map φ) (CategoryTheory.InjectiveResolution.iso J).inv

theorem CategoryTheory.exact_f_d {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [CategoryTheory.EnoughInjectives C] {X : C} {Y : C} (f : X ⟶ Y) : CategoryTheory.ShortComplex.Exact (CategoryTheory.ShortComplex.mk f (CategoryTheory.Injective.d f) (_ : CategoryTheory.CategoryStruct.comp f (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.cokernel.π f) (CategoryTheory.Injective.ι (CategoryTheory.Limits.cokernel f))) = 0))

Our goal is to define InjectiveResolution.of Z : InjectiveResolution Z. The 0-th object in this resolution will just be Injective.under Z, i.e. an arbitrarily chosen injective object with a map from Z. After that, we build the n+1-st object as Injective.syzygies applied to the previously constructed morphism, and the map from the n-th object as Injective.d.

def CategoryTheory.InjectiveResolution.ofCocomplex {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [CategoryTheory.EnoughInjectives C] (Z : C) : CochainComplex C ℕ

Auxiliary definition for InjectiveResolution.of.

Equations

• One or more equations did not get rendered due to their size.

theorem CategoryTheory.InjectiveResolution.ofCocomplex_d_0_1 {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [CategoryTheory.EnoughInjectives C] (Z : C) : (CategoryTheory.InjectiveResolution.ofCocomplex Z).d 0 1 = CategoryTheory.Injective.d (CategoryTheory.Injective.ι Z)

theorem CategoryTheory.InjectiveResolution.ofCocomplex_exactAt_succ {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [CategoryTheory.EnoughInjectives C] (Z : C) (n : ℕ) : HomologicalComplex.ExactAt (CategoryTheory.InjectiveResolution.ofCocomplex Z) (n + 1)

instance CategoryTheory.InjectiveResolution.instInjectiveXNatPreadditiveHasZeroMorphismsToPreadditiveUpToAddRightCancelSemigroupToAddRightCancelMonoidToAddCancelMonoidToCancelAddCommMonoidToOrderedCancelAddCommMonoidStrictOrderedSemiringToOneCanonicallyOrderedCommSemiringOfCocomplex {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [CategoryTheory.EnoughInjectives C] (Z : C) (n : ℕ) : CategoryTheory.Injective ((CategoryTheory.InjectiveResolution.ofCocomplex Z).X n)

Equations

• (_ : CategoryTheory.Injective ((CategoryTheory.InjectiveResolution.ofCocomplex Z).X n)) = (_ : CategoryTheory.Injective ((CategoryTheory.InjectiveResolution.ofCocomplex Z).X n))

@[irreducible]

def CategoryTheory.InjectiveResolution.of {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Abelian C] [CategoryTheory.EnoughInjectives C] (Z : C) : CategoryTheory.InjectiveResolution Z

In any abelian category with enough injectives, InjectiveResolution.of Z constructs an injective resolution of the object Z.

Equations

• @CategoryTheory.InjectiveResolution.of = CategoryTheory.InjectiveResolution.wrapped✝.1

theorem CategoryTheory.InjectiveResolution.of_def {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Abelian C] [CategoryTheory.EnoughInjectives C] (Z : C) : CategoryTheory.InjectiveResolution.of Z = CategoryTheory.InjectiveResolution.mk (CategoryTheory.InjectiveResolution.ofCocomplex Z) ((CochainComplex.fromSingle₀Equiv (CategoryTheory.InjectiveResolution.ofCocomplex Z) Z).symm { val := CategoryTheory.Injective.ι Z, property := (_ : CategoryTheory.CategoryStruct.comp (CategoryTheory.Injective.ι Z) ((CategoryTheory.InjectiveResolution.ofCocomplex Z).d 0 1) = 0) })

instance CategoryTheory.InjectiveResolution.instHasInjectiveResolutionHasZeroObjectPreadditiveHasZeroMorphismsToPreadditive {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [CategoryTheory.EnoughInjectives C] (Z : C) : CategoryTheory.HasInjectiveResolution Z

Equations

• (_ : CategoryTheory.HasInjectiveResolution Z) = (_ : CategoryTheory.HasInjectiveResolution Z)

instance CategoryTheory.InjectiveResolution.instHasInjectiveResolutionsHasZeroObjectPreadditiveHasZeroMorphismsToPreadditive {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [CategoryTheory.EnoughInjectives C] : CategoryTheory.HasInjectiveResolutions C

Equations

• (_ : CategoryTheory.HasInjectiveResolutions C) = (_ : CategoryTheory.HasInjectiveResolutions C)