A square-zero curved duplex

On each parity take A ⊞ A, and in both directions use the map that sends the first summand to the second and kills the second. Sending the second summand back to the first contracts the duplex. The parity shift negates both differentials.

noncomputable def TauCeti.CurvedDuplex.squareZero {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasBinaryBiproducts C] {R : Type w} [Semiring R] [CategoryTheory.Linear R C] (A : C) : CurvedDuplex C 0

The square-zero duplex with both parity pieces A ⊞ A and differential (a,b) ↦ (0,a).

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem TauCeti.CurvedDuplex.squareZero_X₀ {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasBinaryBiproducts C] {R : Type w} [Semiring R] [CategoryTheory.Linear R C] (A : C) : (squareZero A).X₀ = (A ⊞ A)

@[simp]

theorem TauCeti.CurvedDuplex.squareZero_X₁ {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasBinaryBiproducts C] {R : Type w} [Semiring R] [CategoryTheory.Linear R C] (A : C) : (squareZero A).X₁ = (A ⊞ A)

@[simp]

theorem TauCeti.CurvedDuplex.squareZero_d₀ {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasBinaryBiproducts C] {R : Type w} [Semiring R] [CategoryTheory.Linear R C] (A : C) : (squareZero A).d₀ = CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.biprod.fst CategoryTheory.Limits.biprod.inr

@[simp]

theorem TauCeti.CurvedDuplex.squareZero_d₁ {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasBinaryBiproducts C] {R : Type w} [Semiring R] [CategoryTheory.Linear R C] (A : C) : (squareZero A).d₁ = CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.biprod.fst CategoryTheory.Limits.biprod.inr

theorem TauCeti.CurvedDuplex.nullHomotopicMap_squareZero {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasBinaryBiproducts C] {R : Type w} [Semiring R] [CategoryTheory.Linear R C] (A : C) : nullHomotopicMap (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.biprod.snd CategoryTheory.Limits.biprod.inl) (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.biprod.snd CategoryTheory.Limits.biprod.inl) = CategoryTheory.CategoryStruct.id (squareZero A)

Sending the second summand to the first is a contracting homotopy of the square-zero duplex.

theorem TauCeti.CurvedDuplex.isZero_quotientFunctor_obj_squareZero {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasBinaryBiproducts C] {R : Type w} [Semiring R] [CategoryTheory.Linear R C] (A : C) : CategoryTheory.Limits.IsZero ((nullHomotopic C 0).quotientFunctor.obj (squareZero A))

The square-zero duplex is zero in the homotopy category.