Documentation

TauCeti.CategoryTheory.Exact.Biproduct

Binary biproducts of conflations #

Distinguished conflations in an exact category are closed under binary direct sums. The proof uses only Quillen's axioms. First, E2 shows that adjoining an identity summand to an inflation again gives an inflation: the relevant square is a biproduct pushout. E1 then gives the direct sum of two inflations by factoring it as

X₁ ⊞ X₂  --(i₁ ⊞ 1)-->  Y₁ ⊞ X₂  --(1 ⊞ i₂)-->  Y₁ ⊞ Y₂.

The dual argument applies to deflations. Finally, the direct sum of the two underlying kernel--cokernel pairs identifies the cokernel supplied by E1 with the componentwise direct sum, so the componentwise short complex TauCeti.shortComplexBiprod itself is a conflation.

Main declarations #

References #

source
theorem TauCeti.ExactStructure.isInflation_biprod_id {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] (E : ExactStructure C) {X Y : C} {i : X ⟶ Y} (hi : E.IsInflation i) (Z : C) :
E.IsInflation (CategoryTheory.Limits.biprod.map i (CategoryTheory.CategoryStruct.id Z))

Adjoining an identity map as the second summand preserves inflations. This is E2 applied to the biproduct pushout square.

source
theorem TauCeti.ExactStructure.isInflation_id_biprod {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] (E : ExactStructure C) {X Y : C} {i : X ⟶ Y} (hi : E.IsInflation i) (Z : C) :
E.IsInflation (CategoryTheory.Limits.biprod.map (CategoryTheory.CategoryStruct.id Z) i)

Adjoining an identity map as the first summand preserves inflations.

source
theorem TauCeti.ExactStructure.isInflation_biprod {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] (E : ExactStructure C) {X₁ Y₁ X₂ Y₂ : C} {i₁ : X₁ ⟶ Y₁} {i₂ : X₂ ⟶ Y₂} (hi₁ : E.IsInflation i₁) (hi₂ : E.IsInflation i₂) :
E.IsInflation (CategoryTheory.Limits.biprod.map i₁ i₂)

A binary direct sum of inflations is an inflation.

source
theorem TauCeti.ExactStructure.isDeflation_biprod_id {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] (E : ExactStructure C) {Y Z : C} {p : Y ⟶ Z} (hp : E.IsDeflation p) (W : C) :
E.IsDeflation (CategoryTheory.Limits.biprod.map p (CategoryTheory.CategoryStruct.id W))

Adjoining an identity map as the second summand preserves deflations. This is E2op applied to the biproduct pullback square.

source
theorem TauCeti.ExactStructure.isDeflation_id_biprod {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] (E : ExactStructure C) {Y Z : C} {p : Y ⟶ Z} (hp : E.IsDeflation p) (W : C) :
E.IsDeflation (CategoryTheory.Limits.biprod.map (CategoryTheory.CategoryStruct.id W) p)

Adjoining an identity map as the first summand preserves deflations.

source
theorem TauCeti.ExactStructure.isDeflation_biprod {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] (E : ExactStructure C) {Y₁ Z₁ Y₂ Z₂ : C} {p₁ : Y₁ ⟶ Z₁} {p₂ : Y₂ ⟶ Z₂} (hp₁ : E.IsDeflation p₁) (hp₂ : E.IsDeflation p₂) :
E.IsDeflation (CategoryTheory.Limits.biprod.map p₁ p₂)

A binary direct sum of deflations is a deflation.

source
theorem TauCeti.ExactStructure.conflation_biprod {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] (E : ExactStructure C) {S₁ S₂ : CategoryTheory.ShortComplex C} (hS₁ : E.Conflation S₁) (hS₂ : E.Conflation S₂) :
E.Conflation (shortComplexBiprod S₁ S₂)

A binary direct sum of conflations is a conflation.