# mathlib3documentation

category_theory.abelian.injective_resolution

# Main result #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

When the underlying category is abelian:

• category_theory.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 category_theory.InjectiveResolution.desc_commutes.

• category_theory.InjectiveResolution.desc_homotopy: Any two such descents are homotopic.

• category_theory.InjectiveResolution.homotopy_equiv: Any two injective resolutions of the same object are homotopy equivalent.

• category_theory.injective_resolutions: If every object admits an injective resolution, we can construct a functor injective_resolutions C : C ⥤ homotopy_category C.

• category_theory.exact_f_d: f and injective.d f are exact.

• category_theory.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.

noncomputable def category_theory.InjectiveResolution.desc_f_zero {C : Type u} {Y Z : C} (f : Z Y)  :

Auxiliary construction for desc.

Equations
noncomputable def category_theory.InjectiveResolution.desc_f_one {C : Type u} {Y Z : C} (f : Z Y)  :

Auxiliary construction for desc.

Equations
@[simp]
theorem category_theory.InjectiveResolution.desc_f_one_zero_comm {C : Type u} {Y Z : C} (f : Z Y)  :
=
noncomputable def category_theory.InjectiveResolution.desc_f_succ {C : Type u} {Y Z : C} (n : ) (g : J.cocomplex.X n I.cocomplex.X n) (g' : J.cocomplex.X (n + 1) I.cocomplex.X (n + 1)) (w : J.cocomplex.d n (n + 1) g' = g I.cocomplex.d n (n + 1)) :
Σ' (g'' : J.cocomplex.X (n + 2) I.cocomplex.X (n + 2)), J.cocomplex.d (n + 1) (n + 2) g'' = g' I.cocomplex.d (n + 1) (n + 2)

Auxiliary construction for desc.

Equations
@[irreducible]
noncomputable def category_theory.InjectiveResolution.desc {C : Type u} {Y Z : C} (f : Z Y)  :

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

Equations
@[simp]
theorem category_theory.InjectiveResolution.desc_commutes {C : Type u} {Y Z : C} (f : Z Y)  :
= I.ι

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

@[simp]
theorem category_theory.InjectiveResolution.desc_commutes_assoc {C : Type u} {Y Z : C} (f : Z Y) {X' : } (f' : I.cocomplex X') :
J.ι = I.ι f'
noncomputable def category_theory.InjectiveResolution.desc_homotopy_zero_zero {C : Type u} {Y Z : C} (f : I.cocomplex J.cocomplex) (comm : I.ι f = 0) :

An auxiliary definition for desc_homotopy_zero.

Equations
• = (I.ι.f 0) (I.cocomplex.d 0 1) category_theory.InjectiveResolution.desc_homotopy_zero_zero._proof_14 _
noncomputable def category_theory.InjectiveResolution.desc_homotopy_zero_one {C : Type u} {Y Z : C} (f : I.cocomplex J.cocomplex) (comm : I.ι f = 0) :

An auxiliary definition for desc_homotopy_zero.

Equations
• = (I.cocomplex.d 0 1) (I.cocomplex.d 1 2) category_theory.InjectiveResolution.desc_homotopy_zero_one._proof_14 _
noncomputable def category_theory.InjectiveResolution.desc_homotopy_zero_succ {C : Type u} {Y Z : C} (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) = I.cocomplex.d (n + 1) (n + 2) g' + g J.cocomplex.d n (n + 1)) :
I.cocomplex.X (n + 3) J.cocomplex.X (n + 2)

An auxiliary definition for desc_homotopy_zero.

Equations
@[irreducible]
noncomputable def category_theory.InjectiveResolution.desc_homotopy_zero {C : Type u} {Y Z : C} (f : I.cocomplex J.cocomplex) (comm : I.ι f = 0) :
0

Any descent of the zero morphism is homotopic to zero.

Equations
@[irreducible]
noncomputable def category_theory.InjectiveResolution.desc_homotopy {C : Type u} {Y Z : C} (f : Y Z) (g h : I.cocomplex J.cocomplex) (g_comm : I.ι g = J.ι) (h_comm : I.ι h = J.ι) :
h

Two descents of the same morphism are homotopic.

Equations
@[irreducible]
noncomputable def category_theory.InjectiveResolution.desc_id_homotopy {C : Type u} (X : C)  :

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

Equations
@[irreducible]
noncomputable def category_theory.InjectiveResolution.desc_comp_homotopy {C : Type u} {X Y Z : C} (f : X Y) (g : Y Z)  :

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

Equations
noncomputable def category_theory.InjectiveResolution.homotopy_equiv {C : Type u} {X : C}  :

Any two injective resolutions are homotopy equivalent.

Equations
@[simp]
theorem category_theory.InjectiveResolution.homotopy_equiv_hom_ι_assoc {C : Type u} {X : C} {X' : } (f' : J.cocomplex X') :
I.ι (I.homotopy_equiv J).hom f' = J.ι f'
@[simp]
theorem category_theory.InjectiveResolution.homotopy_equiv_inv_ι_assoc {C : Type u} {X : C} {X' : } (f' : I.cocomplex X') :
J.ι (I.homotopy_equiv J).inv f' = I.ι f'
@[reducible]
noncomputable def category_theory.injective_resolution {C : Type u} (Z : C)  :

An arbitrarily chosen injective resolution of an object.

@[reducible]
noncomputable def category_theory.injective_resolution.ι {C : Type u} (Z : C)  :

The cochain map from cochain complex consisting of Z supported in degree 0 back to the arbitrarily chosen injective resolution injective_resolution Z.

@[reducible]
noncomputable def category_theory.injective_resolution.desc {C : Type u} {X Y : C} (f : X Y)  :

The descent of a morphism to a cochain map between the arbitrarily chosen injective resolutions.

noncomputable def category_theory.injective_resolutions (C : Type u)  :

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

Equations
theorem category_theory.exact_f_d {C : Type u} {X Y : C} (f : X Y) :

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.

noncomputable def category_theory.InjectiveResolution.of_cocomplex {C : Type u} (Z : C) :

Auxiliary definition for InjectiveResolution.of.

Equations
• = (λ (_x : Σ (X₀ X₁ : C), X₀ X₁), category_theory.InjectiveResolution.of_cocomplex._match_1 _x)
• category_theory.InjectiveResolution.of_cocomplex._match_1 X, Y, f⟩ =
@[simp]
theorem category_theory.InjectiveResolution.of_cocomplex_d {C : Type u} (Z : C) (i j : ) :
= dite (i + 1 = j) (λ (h : i + 1 = j), (category_theory.InjectiveResolution.of_cocomplex._match_1 .fst (category_theory.InjectiveResolution.of_cocomplex._match_1 .snd.fst _ (λ (t : Σ' (X₀ X₁ X₂ : C) (d₀ : X₀ X₁) (d₁ : X₁ X₂), d₀ d₁ = 0), category_theory.InjectiveResolution.of_cocomplex._match_1 t.snd.fst, t.snd.snd.fst, t.snd.snd.snd.snd.fst⟩) i).d₀ (λ (h : ¬i + 1 = j), 0)
@[simp]
theorem category_theory.InjectiveResolution.of_cocomplex_X {C : Type u} (Z : C) (n : ) :
= (category_theory.InjectiveResolution.of_cocomplex._match_1 .fst (category_theory.InjectiveResolution.of_cocomplex._match_1 .snd.fst _ (λ (t : Σ' (X₀ X₁ X₂ : C) (d₀ : X₀ X₁) (d₁ : X₁ X₂), d₀ d₁ = 0), category_theory.InjectiveResolution.of_cocomplex._match_1 t.snd.fst, t.snd.snd.fst, t.snd.snd.snd.snd.fst⟩) n).X₀
@[irreducible]
noncomputable def category_theory.InjectiveResolution.of {C : Type u} (Z : C) :

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

Equations
@[protected, instance]
@[protected, instance]

If X is a cochain complex of injective objects and we have a quasi-isomorphism f : Y[0] ⟶ X, then X is an injective resolution of Y.

Equations