mathlib documentation

category_theory.abelian.injective_resolution

Main result #

When the underlying category is abelian:

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

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

Equations
@[simp]

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

An auxiliary definition for desc_homotopy_zero.

Equations

An auxiliary definition for desc_homotopy_zero.

Equations
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

Any descent of the zero morphism is homotopic to zero.

Equations

An arbitrarily chosen injective resolution of an object.

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

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

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

Equations

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.

Auxiliary definition for InjectiveResolution.of.

Equations
@[simp]