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} [category_theory.category C] [category_theory.limits.has_zero_morphisms C] [category_theory.limits.has_zero_object C] [category_theory.limits.has_equalizers C] [category_theory.limits.has_images C] {Y Z : C} (f : Z ⟶ Y) (I : category_theory.InjectiveResolution Y) (J : category_theory.InjectiveResolution Z) :

J.cocomplex.X 0 ⟶ I.cocomplex.X 0

Auxiliary construction for desc.

Equations

category_theory.InjectiveResolution.desc_f_zero f I J = category_theory.injective.factor_thru (f ≫ I.ι.f 0) (J.ι.f 0)

source

noncomputable def category_theory.InjectiveResolution.desc_f_one {C : Type u} [category_theory.category C] [category_theory.abelian C] {Y Z : C} (f : Z ⟶ Y) (I : category_theory.InjectiveResolution Y) (J : category_theory.InjectiveResolution Z) :

J.cocomplex.X 1 ⟶ I.cocomplex.X 1

Auxiliary construction for desc.

Equations

category_theory.InjectiveResolution.desc_f_one f I J = category_theory.injective.exact.desc (category_theory.InjectiveResolution.desc_f_zero f I J ≫ I.cocomplex.d 0 1) (J.ι.f 0) (J.cocomplex.d 0 1) _ _

source

@[simp]

theorem category_theory.InjectiveResolution.desc_f_one_zero_comm {C : Type u} [category_theory.category C] [category_theory.abelian C] {Y Z : C} (f : Z ⟶ Y) (I : category_theory.InjectiveResolution Y) (J : category_theory.InjectiveResolution Z) :

J.cocomplex.d 0 1 ≫ category_theory.InjectiveResolution.desc_f_one f I J = category_theory.InjectiveResolution.desc_f_zero f I J ≫ I.cocomplex.d 0 1

source

noncomputable def category_theory.InjectiveResolution.desc_f_succ {C : Type u} [category_theory.category C] [category_theory.abelian C] {Y Z : C} (I : category_theory.InjectiveResolution Y) (J : category_theory.InjectiveResolution Z) (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

I.desc_f_succ J n g g' w = ⟨category_theory.injective.exact.desc (g' ≫ I.cocomplex.d (n + 1) (n + 2)) (J.cocomplex.d n (n + 1)) (J.cocomplex.d (n + 1) (n + 2)) _ _, _⟩

source

@[irreducible]

noncomputable def category_theory.InjectiveResolution.desc {C : Type u} [category_theory.category C] [category_theory.abelian C] {Y Z : C} (f : Z ⟶ Y) (I : category_theory.InjectiveResolution Y) (J : category_theory.InjectiveResolution Z) :

J.cocomplex ⟶ I.cocomplex

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

Equations

category_theory.InjectiveResolution.desc f I J = J.cocomplex.mk_hom I.cocomplex (category_theory.InjectiveResolution.desc_f_zero f I J) (category_theory.InjectiveResolution.desc_f_one f I J) _ (λ (n : ℕ) (_x : Σ' (f : J.cocomplex.X n ⟶ I.cocomplex.X n) (f' : J.cocomplex.X (n + 1) ⟶ I.cocomplex.X (n + 1)), f ≫ I.cocomplex.d n (n + 1) = J.cocomplex.d n (n + 1) ≫ f'), category_theory.InjectiveResolution.desc._match_1 I J n _x)
category_theory.InjectiveResolution.desc._match_1 I J n ⟨g, ⟨g', w⟩⟩ = ⟨(I.desc_f_succ J n g g' _).fst, _⟩

source

@[simp]

theorem category_theory.InjectiveResolution.desc_commutes {C : Type u} [category_theory.category C] [category_theory.abelian C] {Y Z : C} (f : Z ⟶ Y) (I : category_theory.InjectiveResolution Y) (J : category_theory.InjectiveResolution Z) :

J.ι ≫ category_theory.InjectiveResolution.desc f I J = (cochain_complex.single₀ C).map f ≫ I.ι

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

source

@[simp]

theorem category_theory.InjectiveResolution.desc_commutes_assoc {C : Type u} [category_theory.category C] [category_theory.abelian C] {Y Z : C} (f : Z ⟶ Y) (I : category_theory.InjectiveResolution Y) (J : category_theory.InjectiveResolution Z) {X' : cochain_complex C ℕ} (f' : I.cocomplex ⟶ X') :

J.ι ≫ category_theory.InjectiveResolution.desc f I J ≫ f' = (cochain_complex.single₀ C).map f ≫ I.ι ≫ f'

source

noncomputable def category_theory.InjectiveResolution.desc_homotopy_zero_zero {C : Type u} [category_theory.category C] [category_theory.abelian C] {Y Z : C} {I : category_theory.InjectiveResolution Y} {J : category_theory.InjectiveResolution Z} (f : I.cocomplex ⟶ J.cocomplex) (comm : I.ι ≫ f = 0) :

I.cocomplex.X 1 ⟶ J.cocomplex.X 0

An auxiliary definition for desc_homotopy_zero.

Equations

category_theory.InjectiveResolution.desc_homotopy_zero_zero f comm = category_theory.injective.exact.desc (f.f 0) (I.ι.f 0) (I.cocomplex.d 0 1) category_theory.InjectiveResolution.desc_homotopy_zero_zero._proof_14 _

source

noncomputable def category_theory.InjectiveResolution.desc_homotopy_zero_one {C : Type u} [category_theory.category C] [category_theory.abelian C] {Y Z : C} {I : category_theory.InjectiveResolution Y} {J : category_theory.InjectiveResolution Z} (f : I.cocomplex ⟶ J.cocomplex) (comm : I.ι ≫ f = 0) :

I.cocomplex.X 2 ⟶ J.cocomplex.X 1

An auxiliary definition for desc_homotopy_zero.

Equations

category_theory.InjectiveResolution.desc_homotopy_zero_one f comm = category_theory.injective.exact.desc (f.f 1 - category_theory.InjectiveResolution.desc_homotopy_zero_zero f comm ≫ J.cocomplex.d 0 1) (I.cocomplex.d 0 1) (I.cocomplex.d 1 2) category_theory.InjectiveResolution.desc_homotopy_zero_one._proof_14 _

source

noncomputable def category_theory.InjectiveResolution.desc_homotopy_zero_succ {C : Type u} [category_theory.category C] [category_theory.abelian C] {Y Z : C} {I : category_theory.InjectiveResolution Y} {J : category_theory.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) = 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

category_theory.InjectiveResolution.desc_homotopy_zero_succ f n g g' w = category_theory.injective.exact.desc (f.f (n + 2) - g' ≫ J.cocomplex.d (n + 1) (n + 2)) (I.cocomplex.d (n + 1) (n + 2)) (I.cocomplex.d (n + 2) (n + 3)) _ _

source

@[irreducible]

noncomputable def category_theory.InjectiveResolution.desc_homotopy_zero {C : Type u} [category_theory.category C] [category_theory.abelian C] {Y Z : C} {I : category_theory.InjectiveResolution Y} {J : category_theory.InjectiveResolution Z} (f : I.cocomplex ⟶ J.cocomplex) (comm : I.ι ≫ f = 0) :

homotopy f 0

Any descent of the zero morphism is homotopic to zero.

Equations

category_theory.InjectiveResolution.desc_homotopy_zero f comm = homotopy.mk_coinductive f (category_theory.InjectiveResolution.desc_homotopy_zero_zero f comm) _ (category_theory.InjectiveResolution.desc_homotopy_zero_one f comm) _ (λ (n : ℕ) (_x : Σ' (f_1 : I.cocomplex.X (n + 1) ⟶ J.cocomplex.X n) (f' : I.cocomplex.X (n + 2) ⟶ J.cocomplex.X (n + 1)), f.f (n + 1) = f_1 ≫ J.cocomplex.d n (n + 1) + I.cocomplex.d (n + 1) (n + 2) ≫ f'), category_theory.InjectiveResolution.desc_homotopy_zero._match_1 f n _x)
category_theory.InjectiveResolution.desc_homotopy_zero._match_1 f n ⟨g, ⟨g', w⟩⟩ = ⟨category_theory.InjectiveResolution.desc_homotopy_zero_succ f n g g' _, _⟩

source

@[irreducible]

noncomputable def category_theory.InjectiveResolution.desc_homotopy {C : Type u} [category_theory.category C] [category_theory.abelian C] {Y Z : C} (f : Y ⟶ Z) {I : category_theory.InjectiveResolution Y} {J : category_theory.InjectiveResolution Z} (g h : I.cocomplex ⟶ J.cocomplex) (g_comm : I.ι ≫ g = (cochain_complex.single₀ C).map f ≫ J.ι) (h_comm : I.ι ≫ h = (cochain_complex.single₀ C).map f ≫ J.ι) :

homotopy g h

Two descents of the same morphism are homotopic.

Equations

category_theory.InjectiveResolution.desc_homotopy f g h g_comm h_comm = homotopy.equiv_sub_zero.inv_fun (category_theory.InjectiveResolution.desc_homotopy_zero (g - h) _)

source

@[irreducible]

noncomputable def category_theory.InjectiveResolution.desc_id_homotopy {C : Type u} [category_theory.category C] [category_theory.abelian C] (X : C) (I : category_theory.InjectiveResolution X) :

homotopy (category_theory.InjectiveResolution.desc (𝟙 X) I I) (𝟙 I.cocomplex)

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

Equations

category_theory.InjectiveResolution.desc_id_homotopy X I = category_theory.InjectiveResolution.desc_homotopy (𝟙 X) (category_theory.InjectiveResolution.desc (𝟙 X) I I) (𝟙 I.cocomplex) _ _

source

@[irreducible]

noncomputable def category_theory.InjectiveResolution.desc_comp_homotopy {C : Type u} [category_theory.category C] [category_theory.abelian C] {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z) (I : category_theory.InjectiveResolution X) (J : category_theory.InjectiveResolution Y) (K : category_theory.InjectiveResolution Z) :

homotopy (category_theory.InjectiveResolution.desc (f ≫ g) K I) (category_theory.InjectiveResolution.desc f J I ≫ category_theory.InjectiveResolution.desc g K J)

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

Equations

category_theory.InjectiveResolution.desc_comp_homotopy f g I J K = category_theory.InjectiveResolution.desc_homotopy (f ≫ g) (category_theory.InjectiveResolution.desc (f ≫ g) K I) (category_theory.InjectiveResolution.desc f J I ≫ category_theory.InjectiveResolution.desc g K J) _ _

source

noncomputable def category_theory.InjectiveResolution.homotopy_equiv {C : Type u} [category_theory.category C] [category_theory.abelian C] {X : C} (I : category_theory.InjectiveResolution X) (J : category_theory.InjectiveResolution X) :

homotopy_equiv I.cocomplex J.cocomplex

Any two injective resolutions are homotopy equivalent.

Equations

I.homotopy_equiv J = {hom := category_theory.InjectiveResolution.desc (𝟙 X) J I, inv := category_theory.InjectiveResolution.desc (𝟙 X) I J, homotopy_hom_inv_id := (category_theory.InjectiveResolution.desc_comp_homotopy (𝟙 X) (𝟙 X) I J I).symm.trans (_.mpr (_.mp (category_theory.InjectiveResolution.desc_id_homotopy X I))), homotopy_inv_hom_id := (category_theory.InjectiveResolution.desc_comp_homotopy (𝟙 X) (𝟙 X) J I J).symm.trans (_.mpr (_.mp (category_theory.InjectiveResolution.desc_id_homotopy X J)))}

source

@[simp]

theorem category_theory.InjectiveResolution.homotopy_equiv_hom_ι {C : Type u} [category_theory.category C] [category_theory.abelian C] {X : C} (I J : category_theory.InjectiveResolution X) :

I.ι ≫ (I.homotopy_equiv J).hom = J.ι

source

@[simp]

theorem category_theory.InjectiveResolution.homotopy_equiv_hom_ι_assoc {C : Type u} [category_theory.category C] [category_theory.abelian C] {X : C} (I J : category_theory.InjectiveResolution X) {X' : cochain_complex C ℕ} (f' : J.cocomplex ⟶ X') :

I.ι ≫ (I.homotopy_equiv J).hom ≫ f' = J.ι ≫ f'

source

@[simp]

theorem category_theory.InjectiveResolution.homotopy_equiv_inv_ι {C : Type u} [category_theory.category C] [category_theory.abelian C] {X : C} (I J : category_theory.InjectiveResolution X) :

J.ι ≫ (I.homotopy_equiv J).inv = I.ι

source

@[simp]

theorem category_theory.InjectiveResolution.homotopy_equiv_inv_ι_assoc {C : Type u} [category_theory.category C] [category_theory.abelian C] {X : C} (I J : category_theory.InjectiveResolution X) {X' : cochain_complex C ℕ} (f' : I.cocomplex ⟶ X') :

J.ι ≫ (I.homotopy_equiv J).inv ≫ f' = I.ι ≫ f'

source

@[reducible]

noncomputable def category_theory.injective_resolution {C : Type u} [category_theory.category C] [category_theory.abelian C] (Z : C) [category_theory.has_injective_resolution Z] :

cochain_complex C ℕ

An arbitrarily chosen injective resolution of an object.

source

@[reducible]

noncomputable def category_theory.injective_resolution.ι {C : Type u} [category_theory.category C] [category_theory.abelian C] (Z : C) [category_theory.has_injective_resolution Z] :

(cochain_complex.single₀ C).obj Z ⟶ category_theory.injective_resolution Z

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

source

@[reducible]

noncomputable def category_theory.injective_resolution.desc {C : Type u} [category_theory.category C] [category_theory.abelian C] {X Y : C} (f : X ⟶ Y) [category_theory.has_injective_resolution X] [category_theory.has_injective_resolution Y] :

category_theory.injective_resolution X ⟶ category_theory.injective_resolution Y

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

source

noncomputable def category_theory.injective_resolutions (C : Type u) [category_theory.category C] [category_theory.abelian C] [category_theory.has_injective_resolutions C] :

C ⥤ homotopy_category C (complex_shape.up ℕ)

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

Equations

category_theory.injective_resolutions C = {obj := λ (X : C), (homotopy_category.quotient C (complex_shape.up ℕ)).obj (category_theory.injective_resolution X), map := λ (X Y : C) (f : X ⟶ Y), (homotopy_category.quotient C (complex_shape.up ℕ)).map (category_theory.injective_resolution.desc f), map_id' := _, map_comp' := _}

source

theorem category_theory.exact_f_d {C : Type u} [category_theory.category C] [category_theory.abelian C] [category_theory.enough_injectives C] {X Y : C} (f : X ⟶ Y) :

category_theory.exact f (category_theory.injective.d f)

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.

source