Documentation

TauCeti.Algebra.Homology.ShortComplex.Biproduct

Binary biproducts of short complexes #

Two short complexes in a category with zero morphisms have a componentwise binary direct sum, provided the three relevant binary biproducts exist. This file constructs it and records the projection lemmas identifying its objects and maps.

Main definitions #

Implementation notes #

shortComplexBiprod is @[expose]d so that its objects are definitionally the corresponding biproducts outside this file. Without that, the type of (shortComplexBiprod S₁ S₂).f could not be seen to be S₁.X₁ ⊞ S₂.X₁ ⟶ S₁.X₂ ⊞ S₂.X₂, and the projection lemmas for the two maps would have to be stated with a heterogeneous equality.

source
theorem TauCeti.shortComplexBiprod_zero {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] (S₁ S₂ : CategoryTheory.ShortComplex C) [CategoryTheory.Limits.HasBinaryBiproduct S₁.X₁ S₂.X₁] [CategoryTheory.Limits.HasBinaryBiproduct S₁.X₂ S₂.X₂] [CategoryTheory.Limits.HasBinaryBiproduct S₁.X₃ S₂.X₃] :
CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biprod.map S₁.f S₂.f) (CategoryTheory.Limits.biprod.map S₁.g S₂.g) = 0

The two maps in the componentwise biproduct of short complexes have zero composite.

source
noncomputable def TauCeti.shortComplexBiprod {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] (S₁ S₂ : CategoryTheory.ShortComplex C) [CategoryTheory.Limits.HasBinaryBiproduct S₁.X₁ S₂.X₁] [CategoryTheory.Limits.HasBinaryBiproduct S₁.X₂ S₂.X₂] [CategoryTheory.Limits.HasBinaryBiproduct S₁.X₃ S₂.X₃] :
CategoryTheory.ShortComplex C

The componentwise binary direct sum of two short complexes.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    @[simp]
    theorem TauCeti.shortComplexBiprod_X₁ {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] (S₁ S₂ : CategoryTheory.ShortComplex C) [CategoryTheory.Limits.HasBinaryBiproduct S₁.X₁ S₂.X₁] [CategoryTheory.Limits.HasBinaryBiproduct S₁.X₂ S₂.X₂] [CategoryTheory.Limits.HasBinaryBiproduct S₁.X₃ S₂.X₃] :
    (shortComplexBiprod S₁ S₂).X₁ = (S₁.X₁ ⊞ S₂.X₁)

    The left object of the componentwise biproduct of two short complexes.

    source
    @[simp]
    theorem TauCeti.shortComplexBiprod_X₂ {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] (S₁ S₂ : CategoryTheory.ShortComplex C) [CategoryTheory.Limits.HasBinaryBiproduct S₁.X₁ S₂.X₁] [CategoryTheory.Limits.HasBinaryBiproduct S₁.X₂ S₂.X₂] [CategoryTheory.Limits.HasBinaryBiproduct S₁.X₃ S₂.X₃] :
    (shortComplexBiprod S₁ S₂).X₂ = (S₁.X₂ ⊞ S₂.X₂)

    The middle object of the componentwise biproduct of two short complexes.

    source
    @[simp]
    theorem TauCeti.shortComplexBiprod_X₃ {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] (S₁ S₂ : CategoryTheory.ShortComplex C) [CategoryTheory.Limits.HasBinaryBiproduct S₁.X₁ S₂.X₁] [CategoryTheory.Limits.HasBinaryBiproduct S₁.X₂ S₂.X₂] [CategoryTheory.Limits.HasBinaryBiproduct S₁.X₃ S₂.X₃] :
    (shortComplexBiprod S₁ S₂).X₃ = (S₁.X₃ ⊞ S₂.X₃)

    The right object of the componentwise biproduct of two short complexes.

    source
    @[simp]
    theorem TauCeti.shortComplexBiprod_f {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] (S₁ S₂ : CategoryTheory.ShortComplex C) [CategoryTheory.Limits.HasBinaryBiproduct S₁.X₁ S₂.X₁] [CategoryTheory.Limits.HasBinaryBiproduct S₁.X₂ S₂.X₂] [CategoryTheory.Limits.HasBinaryBiproduct S₁.X₃ S₂.X₃] :
    (shortComplexBiprod S₁ S₂).f = CategoryTheory.Limits.biprod.map S₁.f S₂.f

    The first map of the componentwise biproduct of two short complexes.

    source
    @[simp]
    theorem TauCeti.shortComplexBiprod_g {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] (S₁ S₂ : CategoryTheory.ShortComplex C) [CategoryTheory.Limits.HasBinaryBiproduct S₁.X₁ S₂.X₁] [CategoryTheory.Limits.HasBinaryBiproduct S₁.X₂ S₂.X₂] [CategoryTheory.Limits.HasBinaryBiproduct S₁.X₃ S₂.X₃] :
    (shortComplexBiprod S₁ S₂).g = CategoryTheory.Limits.biprod.map S₁.g S₂.g

    The second map of the componentwise biproduct of two short complexes.