The total complex of a bicomplex

Given a preadditive category C, two complex shapes c₁ : ComplexShape I₁, c₂ : ComplexShape I₂, a bicomplex K : HomologicalComplex₂ C c₁ c₂, and a third complex shape c₁₂ : ComplexShape I₁₂ equipped with [TotalComplexShape c₁ c₂ c₁₂], we construct the total complex K.total c₁₂ : HomologicalComplex C c₁₂.

In particular, if c := ComplexShape.up ℤ and K : HomologicalComplex₂ c c, then for any n : ℤ, (K.total c).X n identifies to the coproduct of the (K.X p).X q such that p + q = n, and the differential on (K.total c).X n is induced by the sum of horizontal differentials (K.X p).X q ⟶ (K.X (p + 1)).X q and (-1) ^ p times the vertical differentials (K.X p).X q ⟶ (K.X p).X (q + 1).

@[inline, reducible]

abbrev HomologicalComplex₂.HasTotal {C : Type u_1} [CategoryTheory.Category.{u_5, u_1} C] [CategoryTheory.Preadditive C] {I₁ : Type u_2} {I₂ : Type u_3} {I₁₂ : Type u_4} {c₁ : ComplexShape I₁} {c₂ : ComplexShape I₂} (K : HomologicalComplex₂ C c₁ c₂) (c₁₂ : ComplexShape I₁₂) [TotalComplexShape c₁ c₂ c₁₂] : Prop

A bicomplex has a total bicomplex if for any i₁₂ : I₁₂, the coproduct of the objects (K.X i₁).X i₂ such that ComplexShape.π c₁ c₂ c₁₂ ⟨i₁, i₂⟩ = i₁₂ exists.

Equations

• HomologicalComplex₂.HasTotal K c₁₂ = CategoryTheory.GradedObject.HasMap (HomologicalComplex₂.toGradedObject K) (ComplexShape.π c₁ c₂ c₁₂)

noncomputable def HomologicalComplex₂.d₁ {C : Type u_1} [CategoryTheory.Category.{u_5, u_1} C] [CategoryTheory.Preadditive C] {I₁ : Type u_2} {I₂ : Type u_3} {I₁₂ : Type u_4} {c₁ : ComplexShape I₁} {c₂ : ComplexShape I₂} (K : HomologicalComplex₂ C c₁ c₂) (c₁₂ : ComplexShape I₁₂) [DecidableEq I₁₂] [TotalComplexShape c₁ c₂ c₁₂] [HomologicalComplex₂.HasTotal K c₁₂] (i₁ : I₁) (i₂ : I₂) (i₁₂ : I₁₂) : (K.X i₁).X i₂ ⟶ CategoryTheory.GradedObject.mapObj (HomologicalComplex₂.toGradedObject K) (ComplexShape.π c₁ c₂ c₁₂) i₁₂

The horizontal differential in the total complex on a given summand.

Equations

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

noncomputable def HomologicalComplex₂.d₂ {C : Type u_1} [CategoryTheory.Category.{u_5, u_1} C] [CategoryTheory.Preadditive C] {I₁ : Type u_2} {I₂ : Type u_3} {I₁₂ : Type u_4} {c₁ : ComplexShape I₁} {c₂ : ComplexShape I₂} (K : HomologicalComplex₂ C c₁ c₂) (c₁₂ : ComplexShape I₁₂) [DecidableEq I₁₂] [TotalComplexShape c₁ c₂ c₁₂] [HomologicalComplex₂.HasTotal K c₁₂] (i₁ : I₁) (i₂ : I₂) (i₁₂ : I₁₂) : (K.X i₁).X i₂ ⟶ CategoryTheory.GradedObject.mapObj (HomologicalComplex₂.toGradedObject K) (ComplexShape.π c₁ c₂ c₁₂) i₁₂

The vertical differential in the total complex on a given summand.

Equations

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

theorem HomologicalComplex₂.d₁_eq_zero {C : Type u_1} [CategoryTheory.Category.{u_5, u_1} C] [CategoryTheory.Preadditive C] {I₁ : Type u_2} {I₂ : Type u_3} {I₁₂ : Type u_4} {c₁ : ComplexShape I₁} {c₂ : ComplexShape I₂} (K : HomologicalComplex₂ C c₁ c₂) (c₁₂ : ComplexShape I₁₂) [DecidableEq I₁₂] [TotalComplexShape c₁ c₂ c₁₂] [HomologicalComplex₂.HasTotal K c₁₂] (i₁ : I₁) (i₂ : I₂) (i₁₂ : I₁₂) (h : ¬c₁.Rel i₁ (ComplexShape.next c₁ i₁)) : HomologicalComplex₂.d₁ K c₁₂ i₁ i₂ i₁₂ = 0

theorem HomologicalComplex₂.d₂_eq_zero {C : Type u_1} [CategoryTheory.Category.{u_5, u_1} C] [CategoryTheory.Preadditive C] {I₁ : Type u_2} {I₂ : Type u_3} {I₁₂ : Type u_4} {c₁ : ComplexShape I₁} {c₂ : ComplexShape I₂} (K : HomologicalComplex₂ C c₁ c₂) (c₁₂ : ComplexShape I₁₂) [DecidableEq I₁₂] [TotalComplexShape c₁ c₂ c₁₂] [HomologicalComplex₂.HasTotal K c₁₂] (i₁ : I₁) (i₂ : I₂) (i₁₂ : I₁₂) (h : ¬c₂.Rel i₂ (ComplexShape.next c₂ i₂)) : HomologicalComplex₂.d₂ K c₁₂ i₁ i₂ i₁₂ = 0

theorem HomologicalComplex₂.d₁_eq' {C : Type u_1} [CategoryTheory.Category.{u_5, u_1} C] [CategoryTheory.Preadditive C] {I₁ : Type u_2} {I₂ : Type u_3} {I₁₂ : Type u_4} {c₁ : ComplexShape I₁} {c₂ : ComplexShape I₂} (K : HomologicalComplex₂ C c₁ c₂) (c₁₂ : ComplexShape I₁₂) [DecidableEq I₁₂] [TotalComplexShape c₁ c₂ c₁₂] [HomologicalComplex₂.HasTotal K c₁₂] {i₁ : I₁} {i₁' : I₁} (h : c₁.Rel i₁ i₁') (i₂ : I₂) (i₁₂ : I₁₂) : HomologicalComplex₂.d₁ K c₁₂ i₁ i₂ i₁₂ = ComplexShape.ε₁ c₁ c₂ c₁₂ (i₁, i₂) • CategoryTheory.CategoryStruct.comp ((K.d i₁ i₁').f i₂) (CategoryTheory.GradedObject.ιMapObjOrZero (HomologicalComplex₂.toGradedObject K) (ComplexShape.π c₁ c₂ c₁₂) (i₁', i₂) i₁₂)

theorem HomologicalComplex₂.d₁_eq_zero' {C : Type u_1} [CategoryTheory.Category.{u_5, u_1} C] [CategoryTheory.Preadditive C] {I₁ : Type u_2} {I₂ : Type u_3} {I₁₂ : Type u_4} {c₁ : ComplexShape I₁} {c₂ : ComplexShape I₂} (K : HomologicalComplex₂ C c₁ c₂) (c₁₂ : ComplexShape I₁₂) [DecidableEq I₁₂] [TotalComplexShape c₁ c₂ c₁₂] [HomologicalComplex₂.HasTotal K c₁₂] {i₁ : I₁} {i₁' : I₁} (h : c₁.Rel i₁ i₁') (i₂ : I₂) (i₁₂ : I₁₂) (h' : ComplexShape.π c₁ c₂ c₁₂ (i₁', i₂) ≠ i₁₂) : HomologicalComplex₂.d₁ K c₁₂ i₁ i₂ i₁₂ = 0

theorem HomologicalComplex₂.d₁_eq {C : Type u_1} [CategoryTheory.Category.{u_5, u_1} C] [CategoryTheory.Preadditive C] {I₁ : Type u_2} {I₂ : Type u_3} {I₁₂ : Type u_4} {c₁ : ComplexShape I₁} {c₂ : ComplexShape I₂} (K : HomologicalComplex₂ C c₁ c₂) (c₁₂ : ComplexShape I₁₂) [DecidableEq I₁₂] [TotalComplexShape c₁ c₂ c₁₂] [HomologicalComplex₂.HasTotal K c₁₂] {i₁ : I₁} {i₁' : I₁} (h : c₁.Rel i₁ i₁') (i₂ : I₂) (i₁₂ : I₁₂) (h' : ComplexShape.π c₁ c₂ c₁₂ (i₁', i₂) = i₁₂) : HomologicalComplex₂.d₁ K c₁₂ i₁ i₂ i₁₂ = ComplexShape.ε₁ c₁ c₂ c₁₂ (i₁, i₂) • CategoryTheory.CategoryStruct.comp ((K.d i₁ i₁').f i₂) (CategoryTheory.GradedObject.ιMapObj (HomologicalComplex₂.toGradedObject K) (ComplexShape.π c₁ c₂ c₁₂) (i₁', i₂) i₁₂ h')

theorem HomologicalComplex₂.d₂_eq' {C : Type u_1} [CategoryTheory.Category.{u_5, u_1} C] [CategoryTheory.Preadditive C] {I₁ : Type u_2} {I₂ : Type u_3} {I₁₂ : Type u_4} {c₁ : ComplexShape I₁} {c₂ : ComplexShape I₂} (K : HomologicalComplex₂ C c₁ c₂) (c₁₂ : ComplexShape I₁₂) [DecidableEq I₁₂] [TotalComplexShape c₁ c₂ c₁₂] [HomologicalComplex₂.HasTotal K c₁₂] (i₁ : I₁) {i₂ : I₂} {i₂' : I₂} (h : c₂.Rel i₂ i₂') (i₁₂ : I₁₂) : HomologicalComplex₂.d₂ K c₁₂ i₁ i₂ i₁₂ = ComplexShape.ε₂ c₁ c₂ c₁₂ (i₁, i₂) • CategoryTheory.CategoryStruct.comp ((K.X i₁).d i₂ i₂') (CategoryTheory.GradedObject.ιMapObjOrZero (HomologicalComplex₂.toGradedObject K) (ComplexShape.π c₁ c₂ c₁₂) (i₁, i₂') i₁₂)

theorem HomologicalComplex₂.d₂_eq_zero' {C : Type u_1} [CategoryTheory.Category.{u_5, u_1} C] [CategoryTheory.Preadditive C] {I₁ : Type u_2} {I₂ : Type u_3} {I₁₂ : Type u_4} {c₁ : ComplexShape I₁} {c₂ : ComplexShape I₂} (K : HomologicalComplex₂ C c₁ c₂) (c₁₂ : ComplexShape I₁₂) [DecidableEq I₁₂] [TotalComplexShape c₁ c₂ c₁₂] [HomologicalComplex₂.HasTotal K c₁₂] (i₁ : I₁) {i₂ : I₂} {i₂' : I₂} (h : c₂.Rel i₂ i₂') (i₁₂ : I₁₂) (h' : ComplexShape.π c₁ c₂ c₁₂ (i₁, i₂') ≠ i₁₂) : HomologicalComplex₂.d₂ K c₁₂ i₁ i₂ i₁₂ = 0

theorem HomologicalComplex₂.d₂_eq {C : Type u_1} [CategoryTheory.Category.{u_5, u_1} C] [CategoryTheory.Preadditive C] {I₁ : Type u_2} {I₂ : Type u_3} {I₁₂ : Type u_4} {c₁ : ComplexShape I₁} {c₂ : ComplexShape I₂} (K : HomologicalComplex₂ C c₁ c₂) (c₁₂ : ComplexShape I₁₂) [DecidableEq I₁₂] [TotalComplexShape c₁ c₂ c₁₂] [HomologicalComplex₂.HasTotal K c₁₂] (i₁ : I₁) {i₂ : I₂} {i₂' : I₂} (h : c₂.Rel i₂ i₂') (i₁₂ : I₁₂) (h' : ComplexShape.π c₁ c₂ c₁₂ (i₁, i₂') = i₁₂) : HomologicalComplex₂.d₂ K c₁₂ i₁ i₂ i₁₂ = ComplexShape.ε₂ c₁ c₂ c₁₂ (i₁, i₂) • CategoryTheory.CategoryStruct.comp ((K.X i₁).d i₂ i₂') (CategoryTheory.GradedObject.ιMapObj (HomologicalComplex₂.toGradedObject K) (ComplexShape.π c₁ c₂ c₁₂) (i₁, i₂') i₁₂ h')

noncomputable def HomologicalComplex₂.D₁ {C : Type u_1} [CategoryTheory.Category.{u_5, u_1} C] [CategoryTheory.Preadditive C] {I₁ : Type u_2} {I₂ : Type u_3} {I₁₂ : Type u_4} {c₁ : ComplexShape I₁} {c₂ : ComplexShape I₂} (K : HomologicalComplex₂ C c₁ c₂) (c₁₂ : ComplexShape I₁₂) [DecidableEq I₁₂] [TotalComplexShape c₁ c₂ c₁₂] [HomologicalComplex₂.HasTotal K c₁₂] (i₁₂ : I₁₂) (i₁₂' : I₁₂) : CategoryTheory.GradedObject.mapObj (HomologicalComplex₂.toGradedObject K) (ComplexShape.π c₁ c₂ c₁₂) i₁₂ ⟶ CategoryTheory.GradedObject.mapObj (HomologicalComplex₂.toGradedObject K) (ComplexShape.π c₁ c₂ c₁₂) i₁₂'

The horizontal differential in the total complex.

Equations

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

@[simp]

theorem HomologicalComplex₂.ι_D₁_assoc {C : Type u_1} [CategoryTheory.Category.{u_5, u_1} C] [CategoryTheory.Preadditive C] {I₁ : Type u_2} {I₂ : Type u_3} {I₁₂ : Type u_4} {c₁ : ComplexShape I₁} {c₂ : ComplexShape I₂} (K : HomologicalComplex₂ C c₁ c₂) (c₁₂ : ComplexShape I₁₂) [DecidableEq I₁₂] [TotalComplexShape c₁ c₂ c₁₂] [HomologicalComplex₂.HasTotal K c₁₂] (i₁₂ : I₁₂) (i₁₂' : I₁₂) (i : I₁ × I₂) (h : ComplexShape.π c₁ c₂ c₁₂ i = i₁₂) {Z : C} (h : CategoryTheory.GradedObject.mapObj (HomologicalComplex₂.toGradedObject K) (ComplexShape.π c₁ c₂ c₁₂) i₁₂' ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.GradedObject.ιMapObj (HomologicalComplex₂.toGradedObject K) (ComplexShape.π c₁ c₂ c₁₂) i i₁₂ h✝) (CategoryTheory.CategoryStruct.comp (HomologicalComplex₂.D₁ K c₁₂ i₁₂ i₁₂') h) = CategoryTheory.CategoryStruct.comp (HomologicalComplex₂.d₁ K c₁₂ i.1 i.2 i₁₂') h

@[simp]

theorem HomologicalComplex₂.ι_D₁ {C : Type u_1} [CategoryTheory.Category.{u_5, u_1} C] [CategoryTheory.Preadditive C] {I₁ : Type u_2} {I₂ : Type u_3} {I₁₂ : Type u_4} {c₁ : ComplexShape I₁} {c₂ : ComplexShape I₂} (K : HomologicalComplex₂ C c₁ c₂) (c₁₂ : ComplexShape I₁₂) [DecidableEq I₁₂] [TotalComplexShape c₁ c₂ c₁₂] [HomologicalComplex₂.HasTotal K c₁₂] (i₁₂ : I₁₂) (i₁₂' : I₁₂) (i : I₁ × I₂) (h : ComplexShape.π c₁ c₂ c₁₂ i = i₁₂) : CategoryTheory.CategoryStruct.comp (CategoryTheory.GradedObject.ιMapObj (HomologicalComplex₂.toGradedObject K) (ComplexShape.π c₁ c₂ c₁₂) i i₁₂ h) (HomologicalComplex₂.D₁ K c₁₂ i₁₂ i₁₂') = HomologicalComplex₂.d₁ K c₁₂ i.1 i.2 i₁₂'

noncomputable def HomologicalComplex₂.D₂ {C : Type u_1} [CategoryTheory.Category.{u_5, u_1} C] [CategoryTheory.Preadditive C] {I₁ : Type u_2} {I₂ : Type u_3} {I₁₂ : Type u_4} {c₁ : ComplexShape I₁} {c₂ : ComplexShape I₂} (K : HomologicalComplex₂ C c₁ c₂) (c₁₂ : ComplexShape I₁₂) [DecidableEq I₁₂] [TotalComplexShape c₁ c₂ c₁₂] [HomologicalComplex₂.HasTotal K c₁₂] (i₁₂ : I₁₂) (i₁₂' : I₁₂) : CategoryTheory.GradedObject.mapObj (HomologicalComplex₂.toGradedObject K) (ComplexShape.π c₁ c₂ c₁₂) i₁₂ ⟶ CategoryTheory.GradedObject.mapObj (HomologicalComplex₂.toGradedObject K) (ComplexShape.π c₁ c₂ c₁₂) i₁₂'

The vertical differential in the total complex.

Equations

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

@[simp]

theorem HomologicalComplex₂.ι_D₂_assoc {C : Type u_1} [CategoryTheory.Category.{u_5, u_1} C] [CategoryTheory.Preadditive C] {I₁ : Type u_2} {I₂ : Type u_3} {I₁₂ : Type u_4} {c₁ : ComplexShape I₁} {c₂ : ComplexShape I₂} (K : HomologicalComplex₂ C c₁ c₂) (c₁₂ : ComplexShape I₁₂) [DecidableEq I₁₂] [TotalComplexShape c₁ c₂ c₁₂] [HomologicalComplex₂.HasTotal K c₁₂] (i₁₂ : I₁₂) (i₁₂' : I₁₂) (i : I₁ × I₂) (h : ComplexShape.π c₁ c₂ c₁₂ i = i₁₂) {Z : C} (h : CategoryTheory.GradedObject.mapObj (HomologicalComplex₂.toGradedObject K) (ComplexShape.π c₁ c₂ c₁₂) i₁₂' ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.GradedObject.ιMapObj (HomologicalComplex₂.toGradedObject K) (ComplexShape.π c₁ c₂ c₁₂) i i₁₂ h✝) (CategoryTheory.CategoryStruct.comp (HomologicalComplex₂.D₂ K c₁₂ i₁₂ i₁₂') h) = CategoryTheory.CategoryStruct.comp (HomologicalComplex₂.d₂ K c₁₂ i.1 i.2 i₁₂') h

@[simp]

theorem HomologicalComplex₂.ι_D₂ {C : Type u_1} [CategoryTheory.Category.{u_5, u_1} C] [CategoryTheory.Preadditive C] {I₁ : Type u_2} {I₂ : Type u_3} {I₁₂ : Type u_4} {c₁ : ComplexShape I₁} {c₂ : ComplexShape I₂} (K : HomologicalComplex₂ C c₁ c₂) (c₁₂ : ComplexShape I₁₂) [DecidableEq I₁₂] [TotalComplexShape c₁ c₂ c₁₂] [HomologicalComplex₂.HasTotal K c₁₂] (i₁₂ : I₁₂) (i₁₂' : I₁₂) (i : I₁ × I₂) (h : ComplexShape.π c₁ c₂ c₁₂ i = i₁₂) : CategoryTheory.CategoryStruct.comp (CategoryTheory.GradedObject.ιMapObj (HomologicalComplex₂.toGradedObject K) (ComplexShape.π c₁ c₂ c₁₂) i i₁₂ h) (HomologicalComplex₂.D₂ K c₁₂ i₁₂ i₁₂') = HomologicalComplex₂.d₂ K c₁₂ i.1 i.2 i₁₂'

theorem HomologicalComplex₂.D₁_shape {C : Type u_1} [CategoryTheory.Category.{u_5, u_1} C] [CategoryTheory.Preadditive C] {I₁ : Type u_2} {I₂ : Type u_3} {I₁₂ : Type u_4} {c₁ : ComplexShape I₁} {c₂ : ComplexShape I₂} (K : HomologicalComplex₂ C c₁ c₂) (c₁₂ : ComplexShape I₁₂) [DecidableEq I₁₂] [TotalComplexShape c₁ c₂ c₁₂] [HomologicalComplex₂.HasTotal K c₁₂] (i₁₂ : I₁₂) (i₁₂' : I₁₂) (h₁₂ : ¬c₁₂.Rel i₁₂ i₁₂') : HomologicalComplex₂.D₁ K c₁₂ i₁₂ i₁₂' = 0

theorem HomologicalComplex₂.D₂_shape {C : Type u_1} [CategoryTheory.Category.{u_5, u_1} C] [CategoryTheory.Preadditive C] {I₁ : Type u_2} {I₂ : Type u_3} {I₁₂ : Type u_4} {c₁ : ComplexShape I₁} {c₂ : ComplexShape I₂} (K : HomologicalComplex₂ C c₁ c₂) (c₁₂ : ComplexShape I₁₂) [DecidableEq I₁₂] [TotalComplexShape c₁ c₂ c₁₂] [HomologicalComplex₂.HasTotal K c₁₂] (i₁₂ : I₁₂) (i₁₂' : I₁₂) (h₁₂ : ¬c₁₂.Rel i₁₂ i₁₂') : HomologicalComplex₂.D₂ K c₁₂ i₁₂ i₁₂' = 0

@[simp]

theorem HomologicalComplex₂.D₁_D₁_assoc {C : Type u_1} [CategoryTheory.Category.{u_5, u_1} C] [CategoryTheory.Preadditive C] {I₁ : Type u_2} {I₂ : Type u_3} {I₁₂ : Type u_4} {c₁ : ComplexShape I₁} {c₂ : ComplexShape I₂} (K : HomologicalComplex₂ C c₁ c₂) (c₁₂ : ComplexShape I₁₂) [DecidableEq I₁₂] [TotalComplexShape c₁ c₂ c₁₂] [HomologicalComplex₂.HasTotal K c₁₂] (i₁₂ : I₁₂) (i₁₂' : I₁₂) (i₁₂'' : I₁₂) {Z : C} (h : CategoryTheory.GradedObject.mapObj (HomologicalComplex₂.toGradedObject K) (ComplexShape.π c₁ c₂ c₁₂) i₁₂'' ⟶ Z) : CategoryTheory.CategoryStruct.comp (HomologicalComplex₂.D₁ K c₁₂ i₁₂ i₁₂') (CategoryTheory.CategoryStruct.comp (HomologicalComplex₂.D₁ K c₁₂ i₁₂' i₁₂'') h) = CategoryTheory.CategoryStruct.comp 0 h

@[simp]

theorem HomologicalComplex₂.D₁_D₁ {C : Type u_1} [CategoryTheory.Category.{u_5, u_1} C] [CategoryTheory.Preadditive C] {I₁ : Type u_2} {I₂ : Type u_3} {I₁₂ : Type u_4} {c₁ : ComplexShape I₁} {c₂ : ComplexShape I₂} (K : HomologicalComplex₂ C c₁ c₂) (c₁₂ : ComplexShape I₁₂) [DecidableEq I₁₂] [TotalComplexShape c₁ c₂ c₁₂] [HomologicalComplex₂.HasTotal K c₁₂] (i₁₂ : I₁₂) (i₁₂' : I₁₂) (i₁₂'' : I₁₂) : CategoryTheory.CategoryStruct.comp (HomologicalComplex₂.D₁ K c₁₂ i₁₂ i₁₂') (HomologicalComplex₂.D₁ K c₁₂ i₁₂' i₁₂'') = 0

@[simp]

theorem HomologicalComplex₂.D₂_D₂_assoc {C : Type u_1} [CategoryTheory.Category.{u_5, u_1} C] [CategoryTheory.Preadditive C] {I₁ : Type u_2} {I₂ : Type u_3} {I₁₂ : Type u_4} {c₁ : ComplexShape I₁} {c₂ : ComplexShape I₂} (K : HomologicalComplex₂ C c₁ c₂) (c₁₂ : ComplexShape I₁₂) [DecidableEq I₁₂] [TotalComplexShape c₁ c₂ c₁₂] [HomologicalComplex₂.HasTotal K c₁₂] (i₁₂ : I₁₂) (i₁₂' : I₁₂) (i₁₂'' : I₁₂) {Z : C} (h : CategoryTheory.GradedObject.mapObj (HomologicalComplex₂.toGradedObject K) (ComplexShape.π c₁ c₂ c₁₂) i₁₂'' ⟶ Z) : CategoryTheory.CategoryStruct.comp (HomologicalComplex₂.D₂ K c₁₂ i₁₂ i₁₂') (CategoryTheory.CategoryStruct.comp (HomologicalComplex₂.D₂ K c₁₂ i₁₂' i₁₂'') h) = CategoryTheory.CategoryStruct.comp 0 h

@[simp]

theorem HomologicalComplex₂.D₂_D₂ {C : Type u_1} [CategoryTheory.Category.{u_5, u_1} C] [CategoryTheory.Preadditive C] {I₁ : Type u_2} {I₂ : Type u_3} {I₁₂ : Type u_4} {c₁ : ComplexShape I₁} {c₂ : ComplexShape I₂} (K : HomologicalComplex₂ C c₁ c₂) (c₁₂ : ComplexShape I₁₂) [DecidableEq I₁₂] [TotalComplexShape c₁ c₂ c₁₂] [HomologicalComplex₂.HasTotal K c₁₂] (i₁₂ : I₁₂) (i₁₂' : I₁₂) (i₁₂'' : I₁₂) : CategoryTheory.CategoryStruct.comp (HomologicalComplex₂.D₂ K c₁₂ i₁₂ i₁₂') (HomologicalComplex₂.D₂ K c₁₂ i₁₂' i₁₂'') = 0

@[simp]

theorem HomologicalComplex₂.D₂_D₁_assoc {C : Type u_1} [CategoryTheory.Category.{u_5, u_1} C] [CategoryTheory.Preadditive C] {I₁ : Type u_2} {I₂ : Type u_3} {I₁₂ : Type u_4} {c₁ : ComplexShape I₁} {c₂ : ComplexShape I₂} (K : HomologicalComplex₂ C c₁ c₂) (c₁₂ : ComplexShape I₁₂) [DecidableEq I₁₂] [TotalComplexShape c₁ c₂ c₁₂] [HomologicalComplex₂.HasTotal K c₁₂] (i₁₂ : I₁₂) (i₁₂' : I₁₂) (i₁₂'' : I₁₂) {Z : C} (h : CategoryTheory.GradedObject.mapObj (HomologicalComplex₂.toGradedObject K) (ComplexShape.π c₁ c₂ c₁₂) i₁₂'' ⟶ Z) : CategoryTheory.CategoryStruct.comp (HomologicalComplex₂.D₂ K c₁₂ i₁₂ i₁₂') (CategoryTheory.CategoryStruct.comp (HomologicalComplex₂.D₁ K c₁₂ i₁₂' i₁₂'') h) = CategoryTheory.CategoryStruct.comp (-CategoryTheory.CategoryStruct.comp (HomologicalComplex₂.D₁ K c₁₂ i₁₂ i₁₂') (HomologicalComplex₂.D₂ K c₁₂ i₁₂' i₁₂'')) h

@[simp]

theorem HomologicalComplex₂.D₂_D₁ {C : Type u_1} [CategoryTheory.Category.{u_5, u_1} C] [CategoryTheory.Preadditive C] {I₁ : Type u_2} {I₂ : Type u_3} {I₁₂ : Type u_4} {c₁ : ComplexShape I₁} {c₂ : ComplexShape I₂} (K : HomologicalComplex₂ C c₁ c₂) (c₁₂ : ComplexShape I₁₂) [DecidableEq I₁₂] [TotalComplexShape c₁ c₂ c₁₂] [HomologicalComplex₂.HasTotal K c₁₂] (i₁₂ : I₁₂) (i₁₂' : I₁₂) (i₁₂'' : I₁₂) : CategoryTheory.CategoryStruct.comp (HomologicalComplex₂.D₂ K c₁₂ i₁₂ i₁₂') (HomologicalComplex₂.D₁ K c₁₂ i₁₂' i₁₂'') = -CategoryTheory.CategoryStruct.comp (HomologicalComplex₂.D₁ K c₁₂ i₁₂ i₁₂') (HomologicalComplex₂.D₂ K c₁₂ i₁₂' i₁₂'')

theorem HomologicalComplex₂.D₁_D₂_assoc {C : Type u_1} [CategoryTheory.Category.{u_5, u_1} C] [CategoryTheory.Preadditive C] {I₁ : Type u_2} {I₂ : Type u_3} {I₁₂ : Type u_4} {c₁ : ComplexShape I₁} {c₂ : ComplexShape I₂} (K : HomologicalComplex₂ C c₁ c₂) (c₁₂ : ComplexShape I₁₂) [DecidableEq I₁₂] [TotalComplexShape c₁ c₂ c₁₂] [HomologicalComplex₂.HasTotal K c₁₂] (i₁₂ : I₁₂) (i₁₂' : I₁₂) (i₁₂'' : I₁₂) {Z : C} (h : CategoryTheory.GradedObject.mapObj (HomologicalComplex₂.toGradedObject K) (ComplexShape.π c₁ c₂ c₁₂) i₁₂'' ⟶ Z) : CategoryTheory.CategoryStruct.comp (HomologicalComplex₂.D₁ K c₁₂ i₁₂ i₁₂') (CategoryTheory.CategoryStruct.comp (HomologicalComplex₂.D₂ K c₁₂ i₁₂' i₁₂'') h) = CategoryTheory.CategoryStruct.comp (-CategoryTheory.CategoryStruct.comp (HomologicalComplex₂.D₂ K c₁₂ i₁₂ i₁₂') (HomologicalComplex₂.D₁ K c₁₂ i₁₂' i₁₂'')) h

theorem HomologicalComplex₂.D₁_D₂ {C : Type u_1} [CategoryTheory.Category.{u_5, u_1} C] [CategoryTheory.Preadditive C] {I₁ : Type u_2} {I₂ : Type u_3} {I₁₂ : Type u_4} {c₁ : ComplexShape I₁} {c₂ : ComplexShape I₂} (K : HomologicalComplex₂ C c₁ c₂) (c₁₂ : ComplexShape I₁₂) [DecidableEq I₁₂] [TotalComplexShape c₁ c₂ c₁₂] [HomologicalComplex₂.HasTotal K c₁₂] (i₁₂ : I₁₂) (i₁₂' : I₁₂) (i₁₂'' : I₁₂) : CategoryTheory.CategoryStruct.comp (HomologicalComplex₂.D₁ K c₁₂ i₁₂ i₁₂') (HomologicalComplex₂.D₂ K c₁₂ i₁₂' i₁₂'') = -CategoryTheory.CategoryStruct.comp (HomologicalComplex₂.D₂ K c₁₂ i₁₂ i₁₂') (HomologicalComplex₂.D₁ K c₁₂ i₁₂' i₁₂'')

@[simp]

theorem HomologicalComplex₂.total_d {C : Type u_1} [CategoryTheory.Category.{u_5, u_1} C] [CategoryTheory.Preadditive C] {I₁ : Type u_2} {I₂ : Type u_3} {I₁₂ : Type u_4} {c₁ : ComplexShape I₁} {c₂ : ComplexShape I₂} (K : HomologicalComplex₂ C c₁ c₂) (c₁₂ : ComplexShape I₁₂) [DecidableEq I₁₂] [TotalComplexShape c₁ c₂ c₁₂] [HomologicalComplex₂.HasTotal K c₁₂] (i₁₂ : I₁₂) (i₁₂' : I₁₂) : (HomologicalComplex₂.total K c₁₂).d i₁₂ i₁₂' = HomologicalComplex₂.D₁ K c₁₂ i₁₂ i₁₂' + HomologicalComplex₂.D₂ K c₁₂ i₁₂ i₁₂'

@[simp]

theorem HomologicalComplex₂.total_X {C : Type u_1} [CategoryTheory.Category.{u_5, u_1} C] [CategoryTheory.Preadditive C] {I₁ : Type u_2} {I₂ : Type u_3} {I₁₂ : Type u_4} {c₁ : ComplexShape I₁} {c₂ : ComplexShape I₂} (K : HomologicalComplex₂ C c₁ c₂) (c₁₂ : ComplexShape I₁₂) [DecidableEq I₁₂] [TotalComplexShape c₁ c₂ c₁₂] [HomologicalComplex₂.HasTotal K c₁₂] : (HomologicalComplex₂.total K c₁₂).X = CategoryTheory.GradedObject.mapObj (HomologicalComplex₂.toGradedObject K) (ComplexShape.π c₁ c₂ c₁₂)

noncomputable def HomologicalComplex₂.total {C : Type u_1} [CategoryTheory.Category.{u_5, u_1} C] [CategoryTheory.Preadditive C] {I₁ : Type u_2} {I₂ : Type u_3} {I₁₂ : Type u_4} {c₁ : ComplexShape I₁} {c₂ : ComplexShape I₂} (K : HomologicalComplex₂ C c₁ c₂) (c₁₂ : ComplexShape I₁₂) [DecidableEq I₁₂] [TotalComplexShape c₁ c₂ c₁₂] [HomologicalComplex₂.HasTotal K c₁₂] : HomologicalComplex C c₁₂

The total complex of a bicomplex.

Equations

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

@[inline, reducible]

noncomputable abbrev HomologicalComplex₂.ιTotal {C : Type u_1} [CategoryTheory.Category.{u_5, u_1} C] [CategoryTheory.Preadditive C] {I₁ : Type u_2} {I₂ : Type u_3} {I₁₂ : Type u_4} {c₁ : ComplexShape I₁} {c₂ : ComplexShape I₂} (K : HomologicalComplex₂ C c₁ c₂) (c₁₂ : ComplexShape I₁₂) [DecidableEq I₁₂] [TotalComplexShape c₁ c₂ c₁₂] [HomologicalComplex₂.HasTotal K c₁₂] (i₁ : I₁) (i₂ : I₂) (i₁₂ : I₁₂) (h : ComplexShape.π c₁ c₂ c₁₂ (i₁, i₂) = i₁₂) : (K.X i₁).X i₂ ⟶ (HomologicalComplex₂.total K c₁₂).X i₁₂

The inclusion of a summand in the total complex.

Equations

• HomologicalComplex₂.ιTotal K c₁₂ i₁ i₂ i₁₂ h = CategoryTheory.GradedObject.ιMapObj (HomologicalComplex₂.toGradedObject K) (ComplexShape.π c₁ c₂ c₁₂) (i₁, i₂) i₁₂ h

@[inline, reducible]

noncomputable abbrev HomologicalComplex₂.ιTotalOrZero {C : Type u_1} [CategoryTheory.Category.{u_5, u_1} C] [CategoryTheory.Preadditive C] {I₁ : Type u_2} {I₂ : Type u_3} {I₁₂ : Type u_4} {c₁ : ComplexShape I₁} {c₂ : ComplexShape I₂} (K : HomologicalComplex₂ C c₁ c₂) (c₁₂ : ComplexShape I₁₂) [DecidableEq I₁₂] [TotalComplexShape c₁ c₂ c₁₂] [HomologicalComplex₂.HasTotal K c₁₂] (i₁ : I₁) (i₂ : I₂) (i₁₂ : I₁₂) : (K.X i₁).X i₂ ⟶ (HomologicalComplex₂.total K c₁₂).X i₁₂

The inclusion of a summand in the total complex, or zero if the degrees do not match.

Equations

• HomologicalComplex₂.ιTotalOrZero K c₁₂ i₁ i₂ i₁₂ = CategoryTheory.GradedObject.ιMapObjOrZero (HomologicalComplex₂.toGradedObject K) (ComplexShape.π c₁ c₂ c₁₂) (i₁, i₂) i₁₂

noncomputable def HomologicalComplex₂.totalDesc {C : Type u_1} [CategoryTheory.Category.{u_5, u_1} C] [CategoryTheory.Preadditive C] {I₁ : Type u_2} {I₂ : Type u_3} {I₁₂ : Type u_4} {c₁ : ComplexShape I₁} {c₂ : ComplexShape I₂} (K : HomologicalComplex₂ C c₁ c₂) {c₁₂ : ComplexShape I₁₂} [DecidableEq I₁₂] [TotalComplexShape c₁ c₂ c₁₂] [HomologicalComplex₂.HasTotal K c₁₂] {A : C} {i₁₂ : I₁₂} (f : (i₁ : I₁) → (i₂ : I₂) → ComplexShape.π c₁ c₂ c₁₂ (i₁, i₂) = i₁₂ → ((K.X i₁).X i₂ ⟶ A)) : (HomologicalComplex₂.total K c₁₂).X i₁₂ ⟶ A

Given a bicomplex K, this is a constructor for morphisms from (K.total c₁₂).X i₁₂.

Equations

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

@[simp]

theorem HomologicalComplex₂.ι_totalDesc_assoc {C : Type u_1} [CategoryTheory.Category.{u_5, u_1} C] [CategoryTheory.Preadditive C] {I₁ : Type u_2} {I₂ : Type u_3} {I₁₂ : Type u_4} {c₁ : ComplexShape I₁} {c₂ : ComplexShape I₂} (K : HomologicalComplex₂ C c₁ c₂) {c₁₂ : ComplexShape I₁₂} [DecidableEq I₁₂] [TotalComplexShape c₁ c₂ c₁₂] [HomologicalComplex₂.HasTotal K c₁₂] {A : C} {i₁₂ : I₁₂} (f : (i₁ : I₁) → (i₂ : I₂) → ComplexShape.π c₁ c₂ c₁₂ (i₁, i₂) = i₁₂ → ((K.X i₁).X i₂ ⟶ A)) (i₁ : I₁) (i₂ : I₂) (hi : ComplexShape.π c₁ c₂ c₁₂ (i₁, i₂) = i₁₂) {Z : C} (h : A ⟶ Z) : CategoryTheory.CategoryStruct.comp (HomologicalComplex₂.ιTotal K c₁₂ i₁ i₂ i₁₂ hi) (CategoryTheory.CategoryStruct.comp (HomologicalComplex₂.totalDesc K f) h) = CategoryTheory.CategoryStruct.comp (f i₁ i₂ hi) h

@[simp]

theorem HomologicalComplex₂.ι_totalDesc {C : Type u_1} [CategoryTheory.Category.{u_5, u_1} C] [CategoryTheory.Preadditive C] {I₁ : Type u_2} {I₂ : Type u_3} {I₁₂ : Type u_4} {c₁ : ComplexShape I₁} {c₂ : ComplexShape I₂} (K : HomologicalComplex₂ C c₁ c₂) {c₁₂ : ComplexShape I₁₂} [DecidableEq I₁₂] [TotalComplexShape c₁ c₂ c₁₂] [HomologicalComplex₂.HasTotal K c₁₂] {A : C} {i₁₂ : I₁₂} (f : (i₁ : I₁) → (i₂ : I₂) → ComplexShape.π c₁ c₂ c₁₂ (i₁, i₂) = i₁₂ → ((K.X i₁).X i₂ ⟶ A)) (i₁ : I₁) (i₂ : I₂) (hi : ComplexShape.π c₁ c₂ c₁₂ (i₁, i₂) = i₁₂) : CategoryTheory.CategoryStruct.comp (HomologicalComplex₂.ιTotal K c₁₂ i₁ i₂ i₁₂ hi) (HomologicalComplex₂.totalDesc K f) = f i₁ i₂ hi

theorem HomologicalComplex₂.total.hom_ext {C : Type u_1} [CategoryTheory.Category.{u_5, u_1} C] [CategoryTheory.Preadditive C] {I₁ : Type u_2} {I₂ : Type u_3} {I₁₂ : Type u_4} {c₁ : ComplexShape I₁} {c₂ : ComplexShape I₂} {K : HomologicalComplex₂ C c₁ c₂} (c₁₂ : ComplexShape I₁₂) [DecidableEq I₁₂] [TotalComplexShape c₁ c₂ c₁₂] [HomologicalComplex₂.HasTotal K c₁₂] {A : C} {i₁₂ : I₁₂} {f : (HomologicalComplex₂.total K c₁₂).X i₁₂ ⟶ A} {g : (HomologicalComplex₂.total K c₁₂).X i₁₂ ⟶ A} (h : ∀ (i₁ : I₁) (i₂ : I₂) (hi : ComplexShape.π c₁ c₂ c₁₂ (i₁, i₂) = i₁₂), CategoryTheory.CategoryStruct.comp (HomologicalComplex₂.ιTotal K c₁₂ i₁ i₂ i₁₂ hi) f = CategoryTheory.CategoryStruct.comp (HomologicalComplex₂.ιTotal K c₁₂ i₁ i₂ i₁₂ hi) g) : f = g

@[simp]

theorem HomologicalComplex₂.total.d₁_mapMap_assoc {C : Type u_1} [CategoryTheory.Category.{u_5, u_1} C] [CategoryTheory.Preadditive C] {I₁ : Type u_2} {I₂ : Type u_3} {I₁₂ : Type u_4} {c₁ : ComplexShape I₁} {c₂ : ComplexShape I₂} {K : HomologicalComplex₂ C c₁ c₂} {L : HomologicalComplex₂ C c₁ c₂} (φ : K ⟶ L) (c₁₂ : ComplexShape I₁₂) [DecidableEq I₁₂] [TotalComplexShape c₁ c₂ c₁₂] [HomologicalComplex₂.HasTotal K c₁₂] [HomologicalComplex₂.HasTotal L c₁₂] (i₁ : I₁) (i₂ : I₂) (i₁₂ : I₁₂) {Z : C} (h : CategoryTheory.GradedObject.mapObj (HomologicalComplex₂.toGradedObject L) (ComplexShape.π c₁ c₂ c₁₂) i₁₂ ⟶ Z) : CategoryTheory.CategoryStruct.comp (HomologicalComplex₂.d₁ K c₁₂ i₁ i₂ i₁₂) (CategoryTheory.CategoryStruct.comp (CategoryTheory.GradedObject.mapMap (HomologicalComplex₂.toGradedObjectMap φ) (ComplexShape.π c₁ c₂ c₁₂) i₁₂) h) = CategoryTheory.CategoryStruct.comp ((φ.f i₁).f i₂) (CategoryTheory.CategoryStruct.comp (HomologicalComplex₂.d₁ L c₁₂ i₁ i₂ i₁₂) h)

@[simp]

theorem HomologicalComplex₂.total.d₁_mapMap {C : Type u_1} [CategoryTheory.Category.{u_5, u_1} C] [CategoryTheory.Preadditive C] {I₁ : Type u_2} {I₂ : Type u_3} {I₁₂ : Type u_4} {c₁ : ComplexShape I₁} {c₂ : ComplexShape I₂} {K : HomologicalComplex₂ C c₁ c₂} {L : HomologicalComplex₂ C c₁ c₂} (φ : K ⟶ L) (c₁₂ : ComplexShape I₁₂) [DecidableEq I₁₂] [TotalComplexShape c₁ c₂ c₁₂] [HomologicalComplex₂.HasTotal K c₁₂] [HomologicalComplex₂.HasTotal L c₁₂] (i₁ : I₁) (i₂ : I₂) (i₁₂ : I₁₂) : CategoryTheory.CategoryStruct.comp (HomologicalComplex₂.d₁ K c₁₂ i₁ i₂ i₁₂) (CategoryTheory.GradedObject.mapMap (HomologicalComplex₂.toGradedObjectMap φ) (ComplexShape.π c₁ c₂ c₁₂) i₁₂) = CategoryTheory.CategoryStruct.comp ((φ.f i₁).f i₂) (HomologicalComplex₂.d₁ L c₁₂ i₁ i₂ i₁₂)

@[simp]

theorem HomologicalComplex₂.total.d₂_mapMap_assoc {C : Type u_1} [CategoryTheory.Category.{u_5, u_1} C] [CategoryTheory.Preadditive C] {I₁ : Type u_2} {I₂ : Type u_3} {I₁₂ : Type u_4} {c₁ : ComplexShape I₁} {c₂ : ComplexShape I₂} {K : HomologicalComplex₂ C c₁ c₂} {L : HomologicalComplex₂ C c₁ c₂} (φ : K ⟶ L) (c₁₂ : ComplexShape I₁₂) [DecidableEq I₁₂] [TotalComplexShape c₁ c₂ c₁₂] [HomologicalComplex₂.HasTotal K c₁₂] [HomologicalComplex₂.HasTotal L c₁₂] (i₁ : I₁) (i₂ : I₂) (i₁₂ : I₁₂) {Z : C} (h : CategoryTheory.GradedObject.mapObj (HomologicalComplex₂.toGradedObject L) (ComplexShape.π c₁ c₂ c₁₂) i₁₂ ⟶ Z) : CategoryTheory.CategoryStruct.comp (HomologicalComplex₂.d₂ K c₁₂ i₁ i₂ i₁₂) (CategoryTheory.CategoryStruct.comp (CategoryTheory.GradedObject.mapMap (HomologicalComplex₂.toGradedObjectMap φ) (ComplexShape.π c₁ c₂ c₁₂) i₁₂) h) = CategoryTheory.CategoryStruct.comp ((φ.f i₁).f i₂) (CategoryTheory.CategoryStruct.comp (HomologicalComplex₂.d₂ L c₁₂ i₁ i₂ i₁₂) h)

@[simp]

theorem HomologicalComplex₂.total.d₂_mapMap {C : Type u_1} [CategoryTheory.Category.{u_5, u_1} C] [CategoryTheory.Preadditive C] {I₁ : Type u_2} {I₂ : Type u_3} {I₁₂ : Type u_4} {c₁ : ComplexShape I₁} {c₂ : ComplexShape I₂} {K : HomologicalComplex₂ C c₁ c₂} {L : HomologicalComplex₂ C c₁ c₂} (φ : K ⟶ L) (c₁₂ : ComplexShape I₁₂) [DecidableEq I₁₂] [TotalComplexShape c₁ c₂ c₁₂] [HomologicalComplex₂.HasTotal K c₁₂] [HomologicalComplex₂.HasTotal L c₁₂] (i₁ : I₁) (i₂ : I₂) (i₁₂ : I₁₂) : CategoryTheory.CategoryStruct.comp (HomologicalComplex₂.d₂ K c₁₂ i₁ i₂ i₁₂) (CategoryTheory.GradedObject.mapMap (HomologicalComplex₂.toGradedObjectMap φ) (ComplexShape.π c₁ c₂ c₁₂) i₁₂) = CategoryTheory.CategoryStruct.comp ((φ.f i₁).f i₂) (HomologicalComplex₂.d₂ L c₁₂ i₁ i₂ i₁₂)

theorem HomologicalComplex₂.total.mapMap_D₁_assoc {C : Type u_1} [CategoryTheory.Category.{u_5, u_1} C] [CategoryTheory.Preadditive C] {I₁ : Type u_2} {I₂ : Type u_3} {I₁₂ : Type u_4} {c₁ : ComplexShape I₁} {c₂ : ComplexShape I₂} {K : HomologicalComplex₂ C c₁ c₂} {L : HomologicalComplex₂ C c₁ c₂} (φ : K ⟶ L) (c₁₂ : ComplexShape I₁₂) [DecidableEq I₁₂] [TotalComplexShape c₁ c₂ c₁₂] [HomologicalComplex₂.HasTotal K c₁₂] [HomologicalComplex₂.HasTotal L c₁₂] (i₁₂ : I₁₂) (i₁₂' : I₁₂) {Z : C} (h : CategoryTheory.GradedObject.mapObj (HomologicalComplex₂.toGradedObject L) (ComplexShape.π c₁ c₂ c₁₂) i₁₂' ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.GradedObject.mapMap (HomologicalComplex₂.toGradedObjectMap φ) (ComplexShape.π c₁ c₂ c₁₂) i₁₂) (CategoryTheory.CategoryStruct.comp (HomologicalComplex₂.D₁ L c₁₂ i₁₂ i₁₂') h) = CategoryTheory.CategoryStruct.comp (HomologicalComplex₂.D₁ K c₁₂ i₁₂ i₁₂') (CategoryTheory.CategoryStruct.comp (CategoryTheory.GradedObject.mapMap (HomologicalComplex₂.toGradedObjectMap φ) (ComplexShape.π c₁ c₂ c₁₂) i₁₂') h)

theorem HomologicalComplex₂.total.mapMap_D₁ {C : Type u_1} [CategoryTheory.Category.{u_5, u_1} C] [CategoryTheory.Preadditive C] {I₁ : Type u_2} {I₂ : Type u_3} {I₁₂ : Type u_4} {c₁ : ComplexShape I₁} {c₂ : ComplexShape I₂} {K : HomologicalComplex₂ C c₁ c₂} {L : HomologicalComplex₂ C c₁ c₂} (φ : K ⟶ L) (c₁₂ : ComplexShape I₁₂) [DecidableEq I₁₂] [TotalComplexShape c₁ c₂ c₁₂] [HomologicalComplex₂.HasTotal K c₁₂] [HomologicalComplex₂.HasTotal L c₁₂] (i₁₂ : I₁₂) (i₁₂' : I₁₂) : CategoryTheory.CategoryStruct.comp (CategoryTheory.GradedObject.mapMap (HomologicalComplex₂.toGradedObjectMap φ) (ComplexShape.π c₁ c₂ c₁₂) i₁₂) (HomologicalComplex₂.D₁ L c₁₂ i₁₂ i₁₂') = CategoryTheory.CategoryStruct.comp (HomologicalComplex₂.D₁ K c₁₂ i₁₂ i₁₂') (CategoryTheory.GradedObject.mapMap (HomologicalComplex₂.toGradedObjectMap φ) (ComplexShape.π c₁ c₂ c₁₂) i₁₂')

theorem HomologicalComplex₂.total.mapMap_D₂_assoc {C : Type u_1} [CategoryTheory.Category.{u_5, u_1} C] [CategoryTheory.Preadditive C] {I₁ : Type u_2} {I₂ : Type u_3} {I₁₂ : Type u_4} {c₁ : ComplexShape I₁} {c₂ : ComplexShape I₂} {K : HomologicalComplex₂ C c₁ c₂} {L : HomologicalComplex₂ C c₁ c₂} (φ : K ⟶ L) (c₁₂ : ComplexShape I₁₂) [DecidableEq I₁₂] [TotalComplexShape c₁ c₂ c₁₂] [HomologicalComplex₂.HasTotal K c₁₂] [HomologicalComplex₂.HasTotal L c₁₂] (i₁₂ : I₁₂) (i₁₂' : I₁₂) {Z : C} (h : CategoryTheory.GradedObject.mapObj (HomologicalComplex₂.toGradedObject L) (ComplexShape.π c₁ c₂ c₁₂) i₁₂' ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.GradedObject.mapMap (HomologicalComplex₂.toGradedObjectMap φ) (ComplexShape.π c₁ c₂ c₁₂) i₁₂) (CategoryTheory.CategoryStruct.comp (HomologicalComplex₂.D₂ L c₁₂ i₁₂ i₁₂') h) = CategoryTheory.CategoryStruct.comp (HomologicalComplex₂.D₂ K c₁₂ i₁₂ i₁₂') (CategoryTheory.CategoryStruct.comp (CategoryTheory.GradedObject.mapMap (HomologicalComplex₂.toGradedObjectMap φ) (ComplexShape.π c₁ c₂ c₁₂) i₁₂') h)

theorem HomologicalComplex₂.total.mapMap_D₂ {C : Type u_1} [CategoryTheory.Category.{u_5, u_1} C] [CategoryTheory.Preadditive C] {I₁ : Type u_2} {I₂ : Type u_3} {I₁₂ : Type u_4} {c₁ : ComplexShape I₁} {c₂ : ComplexShape I₂} {K : HomologicalComplex₂ C c₁ c₂} {L : HomologicalComplex₂ C c₁ c₂} (φ : K ⟶ L) (c₁₂ : ComplexShape I₁₂) [DecidableEq I₁₂] [TotalComplexShape c₁ c₂ c₁₂] [HomologicalComplex₂.HasTotal K c₁₂] [HomologicalComplex₂.HasTotal L c₁₂] (i₁₂ : I₁₂) (i₁₂' : I₁₂) : CategoryTheory.CategoryStruct.comp (CategoryTheory.GradedObject.mapMap (HomologicalComplex₂.toGradedObjectMap φ) (ComplexShape.π c₁ c₂ c₁₂) i₁₂) (HomologicalComplex₂.D₂ L c₁₂ i₁₂ i₁₂') = CategoryTheory.CategoryStruct.comp (HomologicalComplex₂.D₂ K c₁₂ i₁₂ i₁₂') (CategoryTheory.GradedObject.mapMap (HomologicalComplex₂.toGradedObjectMap φ) (ComplexShape.π c₁ c₂ c₁₂) i₁₂')

noncomputable def HomologicalComplex₂.total.map {C : Type u_1} [CategoryTheory.Category.{u_5, u_1} C] [CategoryTheory.Preadditive C] {I₁ : Type u_2} {I₂ : Type u_3} {I₁₂ : Type u_4} {c₁ : ComplexShape I₁} {c₂ : ComplexShape I₂} {K : HomologicalComplex₂ C c₁ c₂} {L : HomologicalComplex₂ C c₁ c₂} (φ : K ⟶ L) (c₁₂ : ComplexShape I₁₂) [DecidableEq I₁₂] [TotalComplexShape c₁ c₂ c₁₂] [HomologicalComplex₂.HasTotal K c₁₂] [HomologicalComplex₂.HasTotal L c₁₂] : HomologicalComplex₂.total K c₁₂ ⟶ HomologicalComplex₂.total L c₁₂

The morphism K.total c₁₂ ⟶ L.total c₁₂ of homological complexes induced by a morphism of bicomplexes K ⟶ L.

Equations

• HomologicalComplex₂.total.map φ c₁₂ = { f := CategoryTheory.GradedObject.mapMap (HomologicalComplex₂.toGradedObjectMap φ) (ComplexShape.π c₁ c₂ c₁₂), comm' := ⋯ }

@[simp]

theorem HomologicalComplex₂.total.forget_map {C : Type u_1} [CategoryTheory.Category.{u_5, u_1} C] [CategoryTheory.Preadditive C] {I₁ : Type u_2} {I₂ : Type u_3} {I₁₂ : Type u_4} {c₁ : ComplexShape I₁} {c₂ : ComplexShape I₂} {K : HomologicalComplex₂ C c₁ c₂} {L : HomologicalComplex₂ C c₁ c₂} (φ : K ⟶ L) (c₁₂ : ComplexShape I₁₂) [DecidableEq I₁₂] [TotalComplexShape c₁ c₂ c₁₂] [HomologicalComplex₂.HasTotal K c₁₂] [HomologicalComplex₂.HasTotal L c₁₂] : (HomologicalComplex.forget C c₁₂).map (HomologicalComplex₂.total.map φ c₁₂) = CategoryTheory.GradedObject.mapMap (HomologicalComplex₂.toGradedObjectMap φ) (ComplexShape.π c₁ c₂ c₁₂)

@[simp]

theorem HomologicalComplex₂.total.map_id {C : Type u_1} [CategoryTheory.Category.{u_5, u_1} C] [CategoryTheory.Preadditive C] {I₁ : Type u_2} {I₂ : Type u_3} {I₁₂ : Type u_4} {c₁ : ComplexShape I₁} {c₂ : ComplexShape I₂} (K : HomologicalComplex₂ C c₁ c₂) (c₁₂ : ComplexShape I₁₂) [DecidableEq I₁₂] [TotalComplexShape c₁ c₂ c₁₂] [HomologicalComplex₂.HasTotal K c₁₂] : HomologicalComplex₂.total.map (CategoryTheory.CategoryStruct.id K) c₁₂ = CategoryTheory.CategoryStruct.id (HomologicalComplex₂.total K c₁₂)

theorem HomologicalComplex₂.total.map_comp_assoc {C : Type u_1} [CategoryTheory.Category.{u_5, u_1} C] [CategoryTheory.Preadditive C] {I₁ : Type u_2} {I₂ : Type u_3} {I₁₂ : Type u_4} {c₁ : ComplexShape I₁} {c₂ : ComplexShape I₂} {K : HomologicalComplex₂ C c₁ c₂} {L : HomologicalComplex₂ C c₁ c₂} {M : HomologicalComplex₂ C c₁ c₂} (φ : K ⟶ L) (ψ : L ⟶ M) (c₁₂ : ComplexShape I₁₂) [DecidableEq I₁₂] [TotalComplexShape c₁ c₂ c₁₂] [HomologicalComplex₂.HasTotal K c₁₂] [HomologicalComplex₂.HasTotal L c₁₂] [HomologicalComplex₂.HasTotal M c₁₂] {Z : HomologicalComplex C c₁₂} (h : HomologicalComplex₂.total M c₁₂ ⟶ Z) : CategoryTheory.CategoryStruct.comp (HomologicalComplex₂.total.map (CategoryTheory.CategoryStruct.comp φ ψ) c₁₂) h = CategoryTheory.CategoryStruct.comp (HomologicalComplex₂.total.map φ c₁₂) (CategoryTheory.CategoryStruct.comp (HomologicalComplex₂.total.map ψ c₁₂) h)

@[simp]

theorem HomologicalComplex₂.total.map_comp {C : Type u_1} [CategoryTheory.Category.{u_5, u_1} C] [CategoryTheory.Preadditive C] {I₁ : Type u_2} {I₂ : Type u_3} {I₁₂ : Type u_4} {c₁ : ComplexShape I₁} {c₂ : ComplexShape I₂} {K : HomologicalComplex₂ C c₁ c₂} {L : HomologicalComplex₂ C c₁ c₂} {M : HomologicalComplex₂ C c₁ c₂} (φ : K ⟶ L) (ψ : L ⟶ M) (c₁₂ : ComplexShape I₁₂) [DecidableEq I₁₂] [TotalComplexShape c₁ c₂ c₁₂] [HomologicalComplex₂.HasTotal K c₁₂] [HomologicalComplex₂.HasTotal L c₁₂] [HomologicalComplex₂.HasTotal M c₁₂] : HomologicalComplex₂.total.map (CategoryTheory.CategoryStruct.comp φ ψ) c₁₂ = CategoryTheory.CategoryStruct.comp (HomologicalComplex₂.total.map φ c₁₂) (HomologicalComplex₂.total.map ψ c₁₂)

@[simp]

theorem HomologicalComplex₂.ιTotal_map_assoc {C : Type u_1} [CategoryTheory.Category.{u_5, u_1} C] [CategoryTheory.Preadditive C] {I₁ : Type u_2} {I₂ : Type u_3} {I₁₂ : Type u_4} {c₁ : ComplexShape I₁} {c₂ : ComplexShape I₂} (K : HomologicalComplex₂ C c₁ c₂) (L : HomologicalComplex₂ C c₁ c₂) (φ : K ⟶ L) (c₁₂ : ComplexShape I₁₂) [DecidableEq I₁₂] [TotalComplexShape c₁ c₂ c₁₂] [HomologicalComplex₂.HasTotal K c₁₂] [HomologicalComplex₂.HasTotal L c₁₂] (i₁ : I₁) (i₂ : I₂) (i₁₂ : I₁₂) (h : ComplexShape.π c₁ c₂ c₁₂ (i₁, i₂) = i₁₂) {Z : C} (h : (HomologicalComplex₂.total L c₁₂).X i₁₂ ⟶ Z) : CategoryTheory.CategoryStruct.comp (HomologicalComplex₂.ιTotal K c₁₂ i₁ i₂ i₁₂ h✝) (CategoryTheory.CategoryStruct.comp ((HomologicalComplex₂.total.map φ c₁₂).f i₁₂) h) = CategoryTheory.CategoryStruct.comp ((φ.f i₁).f i₂) (CategoryTheory.CategoryStruct.comp (HomologicalComplex₂.ιTotal L c₁₂ i₁ i₂ i₁₂ h✝) h)

@[simp]

theorem HomologicalComplex₂.ιTotal_map {C : Type u_1} [CategoryTheory.Category.{u_5, u_1} C] [CategoryTheory.Preadditive C] {I₁ : Type u_2} {I₂ : Type u_3} {I₁₂ : Type u_4} {c₁ : ComplexShape I₁} {c₂ : ComplexShape I₂} (K : HomologicalComplex₂ C c₁ c₂) (L : HomologicalComplex₂ C c₁ c₂) (φ : K ⟶ L) (c₁₂ : ComplexShape I₁₂) [DecidableEq I₁₂] [TotalComplexShape c₁ c₂ c₁₂] [HomologicalComplex₂.HasTotal K c₁₂] [HomologicalComplex₂.HasTotal L c₁₂] (i₁ : I₁) (i₂ : I₂) (i₁₂ : I₁₂) (h : ComplexShape.π c₁ c₂ c₁₂ (i₁, i₂) = i₁₂) : CategoryTheory.CategoryStruct.comp (HomologicalComplex₂.ιTotal K c₁₂ i₁ i₂ i₁₂ h) ((HomologicalComplex₂.total.map φ c₁₂).f i₁₂) = CategoryTheory.CategoryStruct.comp ((φ.f i₁).f i₂) (HomologicalComplex₂.ιTotal L c₁₂ i₁ i₂ i₁₂ h)

@[simp]

theorem HomologicalComplex₂.ιTotalOrZero_map_assoc {C : Type u_1} [CategoryTheory.Category.{u_5, u_1} C] [CategoryTheory.Preadditive C] {I₁ : Type u_2} {I₂ : Type u_3} {I₁₂ : Type u_4} {c₁ : ComplexShape I₁} {c₂ : ComplexShape I₂} (K : HomologicalComplex₂ C c₁ c₂) (L : HomologicalComplex₂ C c₁ c₂) (φ : K ⟶ L) (c₁₂ : ComplexShape I₁₂) [DecidableEq I₁₂] [TotalComplexShape c₁ c₂ c₁₂] [HomologicalComplex₂.HasTotal K c₁₂] [HomologicalComplex₂.HasTotal L c₁₂] (i₁ : I₁) (i₂ : I₂) (i₁₂ : I₁₂) {Z : C} (h : (HomologicalComplex₂.total L c₁₂).X i₁₂ ⟶ Z) : CategoryTheory.CategoryStruct.comp (HomologicalComplex₂.ιTotalOrZero K c₁₂ i₁ i₂ i₁₂) (CategoryTheory.CategoryStruct.comp ((HomologicalComplex₂.total.map φ c₁₂).f i₁₂) h) = CategoryTheory.CategoryStruct.comp ((φ.f i₁).f i₂) (CategoryTheory.CategoryStruct.comp (HomologicalComplex₂.ιTotalOrZero L c₁₂ i₁ i₂ i₁₂) h)

@[simp]

theorem HomologicalComplex₂.ιTotalOrZero_map {C : Type u_1} [CategoryTheory.Category.{u_5, u_1} C] [CategoryTheory.Preadditive C] {I₁ : Type u_2} {I₂ : Type u_3} {I₁₂ : Type u_4} {c₁ : ComplexShape I₁} {c₂ : ComplexShape I₂} (K : HomologicalComplex₂ C c₁ c₂) (L : HomologicalComplex₂ C c₁ c₂) (φ : K ⟶ L) (c₁₂ : ComplexShape I₁₂) [DecidableEq I₁₂] [TotalComplexShape c₁ c₂ c₁₂] [HomologicalComplex₂.HasTotal K c₁₂] [HomologicalComplex₂.HasTotal L c₁₂] (i₁ : I₁) (i₂ : I₂) (i₁₂ : I₁₂) : CategoryTheory.CategoryStruct.comp (HomologicalComplex₂.ιTotalOrZero K c₁₂ i₁ i₂ i₁₂) ((HomologicalComplex₂.total.map φ c₁₂).f i₁₂) = CategoryTheory.CategoryStruct.comp ((φ.f i₁).f i₂) (HomologicalComplex₂.ιTotalOrZero L c₁₂ i₁ i₂ i₁₂)

@[simp]

theorem HomologicalComplex₂.totalFunctor_map (C : Type u_1) [CategoryTheory.Category.{u_5, u_1} C] [CategoryTheory.Preadditive C] {I₁ : Type u_2} {I₂ : Type u_3} {I₁₂ : Type u_4} (c₁ : ComplexShape I₁) (c₂ : ComplexShape I₂) (c₁₂ : ComplexShape I₁₂) [DecidableEq I₁₂] [TotalComplexShape c₁ c₂ c₁₂] [∀ (K : HomologicalComplex₂ C c₁ c₂), HomologicalComplex₂.HasTotal K c₁₂] : ∀ {X Y : HomologicalComplex₂ C c₁ c₂} (φ : X ⟶ Y), (HomologicalComplex₂.totalFunctor C c₁ c₂ c₁₂).map φ = HomologicalComplex₂.total.map φ c₁₂

@[simp]

theorem HomologicalComplex₂.totalFunctor_obj (C : Type u_1) [CategoryTheory.Category.{u_5, u_1} C] [CategoryTheory.Preadditive C] {I₁ : Type u_2} {I₂ : Type u_3} {I₁₂ : Type u_4} (c₁ : ComplexShape I₁) (c₂ : ComplexShape I₂) (c₁₂ : ComplexShape I₁₂) [DecidableEq I₁₂] [TotalComplexShape c₁ c₂ c₁₂] [∀ (K : HomologicalComplex₂ C c₁ c₂), HomologicalComplex₂.HasTotal K c₁₂] (K : HomologicalComplex₂ C c₁ c₂) : (HomologicalComplex₂.totalFunctor C c₁ c₂ c₁₂).obj K = HomologicalComplex₂.total K c₁₂

noncomputable def HomologicalComplex₂.totalFunctor (C : Type u_1) [CategoryTheory.Category.{u_5, u_1} C] [CategoryTheory.Preadditive C] {I₁ : Type u_2} {I₂ : Type u_3} {I₁₂ : Type u_4} (c₁ : ComplexShape I₁) (c₂ : ComplexShape I₂) (c₁₂ : ComplexShape I₁₂) [DecidableEq I₁₂] [TotalComplexShape c₁ c₂ c₁₂] [∀ (K : HomologicalComplex₂ C c₁ c₂), HomologicalComplex₂.HasTotal K c₁₂] : CategoryTheory.Functor (HomologicalComplex₂ C c₁ c₂) (HomologicalComplex C c₁₂)

The functor which sends a bicomplex to its total complex.

Equations

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