Splittings and their canonical biproduct comparisons

For a split short complex X₁ ⟶ X₂ ⟶ X₃ with retraction r and section s, a morphism out of X₂ which vanishes on X₁ factors through the projection g via the section s, and dually a morphism into X₂ which vanishes after g factors through the inclusion f via the retraction r. Both are immediate from the identity r ≫ f + g ≫ s = 𝟙, as is the fact that a natural number e with e • 𝟙 = 0 on both outer terms also kills the middle term. The canonical biproduct comparison sends the inclusion f to biprod.inl, and its composition with biprod.snd recovers the projection g. For a split short complex of homological complexes, the homology of the outer terms is a retract of that of the middle term, so the outer terms are exact wherever the middle term is.

Main results

• CategoryTheory.ShortComplex.Splitting.binaryBicone, CategoryTheory.ShortComplex.Splitting.isBilimitBinaryBicone and CategoryTheory.ShortComplex.Splitting.isLimitBinaryFan: the middle term of a split short complex is a binary biproduct, in particular a binary product, of the outer terms.

• CategoryTheory.ShortComplex.Splitting.f_isoBinaryBiproduct_hom: the inclusion under the canonical biproduct comparison.

• CategoryTheory.ShortComplex.Splitting.isoBinaryBiproduct_hom_snd: the projection under the canonical biproduct comparison.

• CategoryTheory.ShortComplex.Splitting.g_s_comp_eq_of_f_comp_eq_zero: if S.f ≫ k = 0, then S.g ≫ s.s ≫ k = k.

• CategoryTheory.ShortComplex.Splitting.comp_r_f_eq_of_comp_g_eq_zero: if k ≫ S.g = 0, then k ≫ s.r ≫ S.f = k.

• CategoryTheory.ShortComplex.Splitting.nsmul_id_X₂_eq_zero: a natural number killing both outer terms kills the middle term.

• CategoryTheory.ShortComplex.Splitting.comp_s_hom_comp_g_hom_of_comp_f_hom_eq_zero: the first statement for linear maps out of a split short complex of modules into an arbitrary module.

• CategoryTheory.ShortComplex.Splitting.acyclic_X₁ and CategoryTheory.ShortComplex.Splitting.acyclic_X₃: the outer terms of a split short complex of homological complexes are acyclic when the middle term is.

Implementation notes

The module version is stated for linear maps rather than as an instance of the categorical one because its target module may live in any universe, for instance the ring itself when the modules of the short complex live in a different universe.

theorem CategoryTheory.ShortComplex.Splitting.g_s_comp_eq_of_f_comp_eq_zero {C : Type u_1} [Category.{u_2, u_1} C] [Preadditive C] {S : ShortComplex C} (s : S.Splitting) {Y : C} (k : S.X₂ ⟶ Y) (hk : CategoryStruct.comp S.f k = 0) : CategoryStruct.comp S.g (CategoryStruct.comp s.s k) = k

A morphism out of the middle term of a split short complex which vanishes on the first term factors through the projection via the section.

theorem CategoryTheory.ShortComplex.Splitting.comp_r_f_eq_of_comp_g_eq_zero {C : Type u_1} [Category.{u_2, u_1} C] [Preadditive C] {S : ShortComplex C} (s : S.Splitting) {Y : C} (k : Y ⟶ S.X₂) (hk : CategoryStruct.comp k S.g = 0) : CategoryStruct.comp k (CategoryStruct.comp s.r S.f) = k

A morphism into the middle term of a split short complex which vanishes after the projection factors through the inclusion via the retraction.

theorem CategoryTheory.ShortComplex.Splitting.nsmul_id_X₂_eq_zero {C : Type u_1} [Category.{u_2, u_1} C] [Preadditive C] {S : ShortComplex C} (s : S.Splitting) {e : ℕ} (h₁ : e • CategoryStruct.id S.X₁ = 0) (h₃ : e • CategoryStruct.id S.X₃ = 0) : e • CategoryStruct.id S.X₂ = 0

A natural number killing both outer terms of a split short complex kills the middle term.

def CategoryTheory.ShortComplex.Splitting.binaryBicone {C : Type u_1} [Category.{u_2, u_1} C] [Preadditive C] {S : ShortComplex C} (s : S.Splitting) : Limits.BinaryBicone S.X₁ S.X₃

The binary bicone of a split short complex: S.X₂ with the inclusions S.f, s.s and the projections s.r, S.g. It is exposed so that its simps lemmas are definitional.

@[simp]

theorem CategoryTheory.ShortComplex.Splitting.binaryBicone_inl {C : Type u_1} [Category.{u_2, u_1} C] [Preadditive C] {S : ShortComplex C} (s : S.Splitting) : s.binaryBicone.inl = S.f

@[simp]

theorem CategoryTheory.ShortComplex.Splitting.binaryBicone_pt {C : Type u_1} [Category.{u_2, u_1} C] [Preadditive C] {S : ShortComplex C} (s : S.Splitting) : s.binaryBicone.pt = S.X₂

@[simp]

theorem CategoryTheory.ShortComplex.Splitting.binaryBicone_fst {C : Type u_1} [Category.{u_2, u_1} C] [Preadditive C] {S : ShortComplex C} (s : S.Splitting) : s.binaryBicone.fst = s.r

@[simp]

theorem CategoryTheory.ShortComplex.Splitting.binaryBicone_inr {C : Type u_1} [Category.{u_2, u_1} C] [Preadditive C] {S : ShortComplex C} (s : S.Splitting) : s.binaryBicone.inr = s.s

@[simp]

theorem CategoryTheory.ShortComplex.Splitting.binaryBicone_snd {C : Type u_1} [Category.{u_2, u_1} C] [Preadditive C] {S : ShortComplex C} (s : S.Splitting) : s.binaryBicone.snd = S.g

def CategoryTheory.ShortComplex.Splitting.isBilimitBinaryBicone {C : Type u_1} [Category.{u_2, u_1} C] [Preadditive C] {S : ShortComplex C} (s : S.Splitting) : s.binaryBicone.IsBilimit

The bicone of a splitting is a binary bilimit: S.X₂ is a biproduct of S.X₁ and S.X₃ through S.f, s.s, s.r and S.g, because s.r ≫ S.f + S.g ≫ s.s = 𝟙 S.X₂.

def CategoryTheory.ShortComplex.Splitting.isLimitBinaryFan {C : Type u_1} [Category.{u_2, u_1} C] [Preadditive C] {S : ShortComplex C} (s : S.Splitting) : Limits.IsLimit (Limits.BinaryFan.mk s.r S.g)

The middle term of a split short complex, with the projections s.r and S.g, is a binary product of the outer terms.

@[simp]

theorem CategoryTheory.ShortComplex.Splitting.f_isoBinaryBiproduct_hom {C : Type u_1} [Category.{u_2, u_1} C] [Preadditive C] {S : ShortComplex C} [Limits.HasBinaryBiproduct S.X₁ S.X₃] (s : S.Splitting) : CategoryStruct.comp S.f s.isoBinaryBiproduct.hom = Limits.biprod.inl

The inclusion of a split short complex is the first biproduct inclusion under its canonical comparison.

@[simp]

theorem CategoryTheory.ShortComplex.Splitting.f_isoBinaryBiproduct_hom_assoc {C : Type u_1} [Category.{u_2, u_1} C] [Preadditive C] {S : ShortComplex C} [Limits.HasBinaryBiproduct S.X₁ S.X₃] (s : S.Splitting) {Z : C} (h : S.X₁ ⊞ S.X₃ ⟶ Z) : CategoryStruct.comp S.f (CategoryStruct.comp s.isoBinaryBiproduct.hom h) = CategoryStruct.comp Limits.biprod.inl h

The inclusion of a split short complex is the first biproduct inclusion under its canonical comparison.

@[simp]

theorem CategoryTheory.ShortComplex.Splitting.isoBinaryBiproduct_hom_snd {C : Type u_1} [Category.{u_2, u_1} C] [Preadditive C] {S : ShortComplex C} [Limits.HasBinaryBiproduct S.X₁ S.X₃] (s : S.Splitting) : CategoryStruct.comp s.isoBinaryBiproduct.hom Limits.biprod.snd = S.g

The projection of a split short complex is the second biproduct projection under its canonical comparison.

@[simp]

theorem CategoryTheory.ShortComplex.Splitting.isoBinaryBiproduct_hom_snd_assoc {C : Type u_1} [Category.{u_2, u_1} C] [Preadditive C] {S : ShortComplex C} [Limits.HasBinaryBiproduct S.X₁ S.X₃] (s : S.Splitting) {Z : C} (h : S.X₃ ⟶ Z) : CategoryStruct.comp s.isoBinaryBiproduct.hom (CategoryStruct.comp Limits.biprod.snd h) = CategoryStruct.comp S.g h

The projection of a split short complex is the second biproduct projection under its canonical comparison.

theorem CategoryTheory.ShortComplex.Splitting.exactAt_X₁ {C : Type u_1} {ι : Type u_2} [Category.{u_3, u_1} C] [Preadditive C] [CategoryWithHomology C] {c : ComplexShape ι} {S : ShortComplex (HomologicalComplex C c)} (s : S.Splitting) {i : ι} (h : S.X₂.ExactAt i) : S.X₁.ExactAt i

In a split short complex of homological complexes, the first term is exact in every degree where the middle term is, since its homology is a retract of that of the middle term.

theorem CategoryTheory.ShortComplex.Splitting.exactAt_X₃ {C : Type u_1} {ι : Type u_2} [Category.{u_3, u_1} C] [Preadditive C] [CategoryWithHomology C] {c : ComplexShape ι} {S : ShortComplex (HomologicalComplex C c)} (s : S.Splitting) {i : ι} (h : S.X₂.ExactAt i) : S.X₃.ExactAt i

In a split short complex of homological complexes, the third term is exact in every degree where the middle term is, since its homology is a retract of that of the middle term.

theorem CategoryTheory.ShortComplex.Splitting.acyclic_X₁ {C : Type u_1} {ι : Type u_2} [Category.{u_3, u_1} C] [Preadditive C] [CategoryWithHomology C] {c : ComplexShape ι} {S : ShortComplex (HomologicalComplex C c)} (s : S.Splitting) (h : S.X₂.Acyclic) : S.X₁.Acyclic

The first term of a split short complex of homological complexes is acyclic when the middle term is.

theorem CategoryTheory.ShortComplex.Splitting.acyclic_X₃ {C : Type u_1} {ι : Type u_2} [Category.{u_3, u_1} C] [Preadditive C] [CategoryWithHomology C] {c : ComplexShape ι} {S : ShortComplex (HomologicalComplex C c)} (s : S.Splitting) (h : S.X₂.Acyclic) : S.X₃.Acyclic

The third term of a split short complex of homological complexes is acyclic when the middle term is.

theorem CategoryTheory.ShortComplex.Splitting.comp_s_hom_comp_g_hom_of_comp_f_hom_eq_zero {R : Type u_1} [Ring R] {S : ShortComplex (ModuleCat R)} {M : Type u_2} [AddCommGroup M] [Module R M] (s : S.Splitting) (ρ : ↑S.X₂ →ₗ[R] M) (hρ : ρ ∘ₗ ModuleCat.Hom.hom S.f = 0) : (ρ ∘ₗ ModuleCat.Hom.hom s.s) ∘ₗ ModuleCat.Hom.hom S.g = ρ

A linear map out of the middle term of a split short complex of modules which vanishes on the first term factors through the projection via the section.