Two-term presentation complexes

A short complex S : S.X₁ ⟶ S.X₂ ⟶ S.X₃ determines the chain complex ⋯ ⟶ 0 ⟶ S.X₁ ⟶ S.X₂, augmented to S.X₃. This file constructs the complex, its augmentation, and the chain maps induced by morphisms of short complexes in any category with zero morphisms and a zero object.

For a short exact presentation by projective objects in an abelian category, this is the complex of the projective resolution used to compute left derived functors in TauCeti.CategoryTheory.Abelian.LeftDerived.

References

• C. A. Weibel, An Introduction to Homological Algebra, Section 2.4.

noncomputable def CategoryTheory.ShortComplex.resolutionComplex {C : Type u} [Category.{v, u} C] [Limits.HasZeroMorphisms C] [Limits.HasZeroObject C] (S : ShortComplex C) : ChainComplex C ℕ

The chain complex ⋯ ⟶ 0 ⟶ S.X₁ ⟶ S.X₂ with S.X₂ in degree 0 and S.X₁ in degree 1, whose only nonzero differential is S.f. In an abelian category, when S is short exact and S.X₁, S.X₂ are projective, it underlies the projective resolution of S.X₃.

This model has definitionally specified objects and differential in degrees 0 and 1, so the kernel formulas for derived functors involve F.map S.f directly. Mathlib's double instead uses classical equality tests on degrees. The comparison resolutionComplexIsoDouble identifies the two models, and the maps below use Mathlib's constructor through this comparison.

@[simp]

theorem CategoryTheory.ShortComplex.resolutionComplex_d_one_zero {C : Type u} [Category.{v, u} C] [Limits.HasZeroMorphisms C] [Limits.HasZeroObject C] (S : ShortComplex C) : S.resolutionComplex.d 1 0 = S.f

The differential of S.resolutionComplex from degree 1 to degree 0 is S.f.

@[simp]

theorem CategoryTheory.ShortComplex.resolutionComplex_X_zero {C : Type u} [Category.{v, u} C] [Limits.HasZeroMorphisms C] [Limits.HasZeroObject C] (S : ShortComplex C) : S.resolutionComplex.X 0 = S.X₂

S.resolutionComplex is S.X₂ in degree 0.

@[simp]

theorem CategoryTheory.ShortComplex.resolutionComplex_X_one {C : Type u} [Category.{v, u} C] [Limits.HasZeroMorphisms C] [Limits.HasZeroObject C] (S : ShortComplex C) : S.resolutionComplex.X 1 = S.X₁

S.resolutionComplex is S.X₁ in degree 1.

theorem CategoryTheory.ShortComplex.isZero_resolutionComplex_X_add_two {C : Type u} [Category.{v, u} C] [Limits.HasZeroMorphisms C] [Limits.HasZeroObject C] (S : ShortComplex C) (n : ℕ) : Limits.IsZero (S.resolutionComplex.X (n + 2))

S.resolutionComplex vanishes in degrees at least 2.

noncomputable def CategoryTheory.ShortComplex.resolutionComplexIsoDouble {C : Type u} [Category.{v, u} C] [Limits.HasZeroMorphisms C] [Limits.HasZeroObject C] (S : ShortComplex C) : S.resolutionComplex ≅ HomologicalComplex.double S.f ⋯

The normalized presentation complex is Mathlib's two-term complex on S.f.

@[simp]

theorem CategoryTheory.ShortComplex.resolutionComplexIsoDouble_hom_f_zero {C : Type u} [Category.{v, u} C] [Limits.HasZeroMorphisms C] [Limits.HasZeroObject C] (S : ShortComplex C) : S.resolutionComplexIsoDouble.hom.f 0 = (HomologicalComplex.doubleXIso₁ S.f ⋯ resolutionComplexIsoDouble_hom_f_zero._proof_1).inv

The comparison isomorphism in degree zero is the inverse of Mathlib's degree-zero identification for the two-term complex.

@[simp]

theorem CategoryTheory.ShortComplex.resolutionComplexIsoDouble_hom_f_one {C : Type u} [Category.{v, u} C] [Limits.HasZeroMorphisms C] [Limits.HasZeroObject C] (S : ShortComplex C) : S.resolutionComplexIsoDouble.hom.f 1 = (HomologicalComplex.doubleXIso₀ S.f ⋯).inv

The comparison isomorphism in degree one is the inverse of Mathlib's degree-one identification for the two-term complex.

@[simp]

theorem CategoryTheory.ShortComplex.resolutionComplexIsoDouble_inv_f_zero {C : Type u} [Category.{v, u} C] [Limits.HasZeroMorphisms C] [Limits.HasZeroObject C] (S : ShortComplex C) : S.resolutionComplexIsoDouble.inv.f 0 = (HomologicalComplex.doubleXIso₁ S.f ⋯ resolutionComplexIsoDouble_hom_f_zero._proof_1).hom

The inverse comparison in degree zero is Mathlib's degree-zero identification.

@[simp]

theorem CategoryTheory.ShortComplex.resolutionComplexIsoDouble_inv_f_one {C : Type u} [Category.{v, u} C] [Limits.HasZeroMorphisms C] [Limits.HasZeroObject C] (S : ShortComplex C) : S.resolutionComplexIsoDouble.inv.f 1 = (HomologicalComplex.doubleXIso₀ S.f ⋯).hom

The inverse comparison in degree one is Mathlib's degree-one identification.

noncomputable def CategoryTheory.ShortComplex.resolutionπ {C : Type u} [Category.{v, u} C] [Limits.HasZeroMorphisms C] [Limits.HasZeroObject C] (S : ShortComplex C) : S.resolutionComplex ⟶ (ChainComplex.single₀ C).obj S.X₃

The augmentation S.g : S.X₂ ⟶ S.X₃ of S.resolutionComplex, as a chain map to the single complex on S.X₃.

@[simp]

theorem CategoryTheory.ShortComplex.resolutionπ_f_zero {C : Type u} [Category.{v, u} C] [Limits.HasZeroMorphisms C] [Limits.HasZeroObject C] (S : ShortComplex C) : S.resolutionπ.f 0 = S.g

In degree 0, the augmentation of S.resolutionComplex is S.g.

noncomputable def CategoryTheory.ShortComplex.resolutionComplexMap {C : Type u} [Category.{v, u} C] [Limits.HasZeroMorphisms C] [Limits.HasZeroObject C] {S S' : ShortComplex C} (φ : S ⟶ S') : S.resolutionComplex ⟶ S'.resolutionComplex

A morphism of short complexes induces the chain map of the associated complexes given by its first two components.

@[simp]

theorem CategoryTheory.ShortComplex.resolutionComplexMap_f_zero {C : Type u} [Category.{v, u} C] [Limits.HasZeroMorphisms C] [Limits.HasZeroObject C] {S S' : ShortComplex C} (φ : S ⟶ S') : (resolutionComplexMap φ).f 0 = φ.τ₂

In degree 0, the chain map induced by φ is φ.τ₂.

@[simp]

theorem CategoryTheory.ShortComplex.resolutionComplexMap_f_one {C : Type u} [Category.{v, u} C] [Limits.HasZeroMorphisms C] [Limits.HasZeroObject C] {S S' : ShortComplex C} (φ : S ⟶ S') : (resolutionComplexMap φ).f 1 = φ.τ₁

In degree 1, the chain map induced by φ is φ.τ₁.

@[simp]

theorem CategoryTheory.ShortComplex.resolutionComplexMap_id {C : Type u} [Category.{v, u} C] [Limits.HasZeroMorphisms C] [Limits.HasZeroObject C] (S : ShortComplex C) : resolutionComplexMap (CategoryStruct.id S) = CategoryStruct.id S.resolutionComplex

The induced map of the identity short-complex morphism is the identity chain map.

@[simp]

theorem CategoryTheory.ShortComplex.resolutionComplexMap_comp {C : Type u} [Category.{v, u} C] [Limits.HasZeroMorphisms C] [Limits.HasZeroObject C] {S S' S'' : ShortComplex C} (φ : S ⟶ S') (ψ : S' ⟶ S'') : resolutionComplexMap (CategoryStruct.comp φ ψ) = CategoryStruct.comp (resolutionComplexMap φ) (resolutionComplexMap ψ)

The induced chain maps preserve composition of short-complex morphisms.

@[simp]

theorem CategoryTheory.ShortComplex.resolutionComplexMap_comp_resolutionπ {C : Type u} [Category.{v, u} C] [Limits.HasZeroMorphisms C] [Limits.HasZeroObject C] {S S' : ShortComplex C} (φ : S ⟶ S') : CategoryStruct.comp (resolutionComplexMap φ) S'.resolutionπ = CategoryStruct.comp S.resolutionπ ((ChainComplex.single₀ C).map φ.τ₃)

The chain map induced by φ lies over φ.τ₃.

@[simp]

theorem CategoryTheory.ShortComplex.resolutionComplexMap_comp_resolutionπ_assoc {C : Type u} [Category.{v, u} C] [Limits.HasZeroMorphisms C] [Limits.HasZeroObject C] {S S' : ShortComplex C} (φ : S ⟶ S') {Z : ChainComplex C ℕ} (h : (ChainComplex.single₀ C).obj S'.X₃ ⟶ Z) : CategoryStruct.comp (resolutionComplexMap φ) (CategoryStruct.comp S'.resolutionπ h) = CategoryStruct.comp S.resolutionπ (CategoryStruct.comp ((ChainComplex.single₀ C).map φ.τ₃) h)

The chain map induced by φ lies over φ.τ₃.