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).

@[reducible, inline]

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

• K.HasTotal c₁₂ = K.toGradedObject.HasMap (c₁.π c₂ c₁₂)

theorem HomologicalComplex₂.hasTotal_of_iso {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₂} (e : K ≅ L) (c₁₂ : ComplexShape I₁₂) [TotalComplexShape c₁ c₂ c₁₂] [K.HasTotal c₁₂] : L.HasTotal 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₁₂] [K.HasTotal c₁₂] (i₁ : I₁) (i₂ : I₂) (i₁₂ : I₁₂) : (K.X i₁).X i₂ ⟶ K.toGradedObject.mapObj (c₁.π c₂ c₁₂) i₁₂

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

Equations

• K.d₁ c₁₂ i₁ i₂ i₁₂ = c₁.ε₁ c₂ c₁₂ (i₁, i₂) • CategoryTheory.CategoryStruct.comp ((K.d i₁ (c₁.next i₁)).f i₂) (K.toGradedObject.ιMapObjOrZero (c₁.π c₂ c₁₂) (c₁.next i₁, i₂) 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₁₂] [K.HasTotal c₁₂] (i₁ : I₁) (i₂ : I₂) (i₁₂ : I₁₂) : (K.X i₁).X i₂ ⟶ K.toGradedObject.mapObj (c₁.π c₂ c₁₂) i₁₂

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

Equations

• K.d₂ c₁₂ i₁ i₂ i₁₂ = c₁.ε₂ c₂ c₁₂ (i₁, i₂) • CategoryTheory.CategoryStruct.comp ((K.X i₁).d i₂ (c₂.next i₂)) (K.toGradedObject.ιMapObjOrZero (c₁.π c₂ c₁₂) (i₁, c₂.next 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₁₂] [K.HasTotal c₁₂] (i₁ : I₁) (i₂ : I₂) (i₁₂ : I₁₂) (h : ¬c₁.Rel i₁ (c₁.next i₁)) : K.d₁ 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₁₂] [K.HasTotal c₁₂] (i₁ : I₁) (i₂ : I₂) (i₁₂ : I₁₂) (h : ¬c₂.Rel i₂ (c₂.next i₂)) : K.d₂ c₁₂ i₁ i₂ i₁₂ = 0

Lemmas in the totalAux namespace should be used only in the internals of the construction of the total complex HomologicalComplex₂.total. Once that definition is done, similar lemmas shall be restated, but with terms like K.toGradedObject.ιMapObj replaced by K.ιTotal. This is done in order to prevent API leakage from definitions involving graded objects.

theorem HomologicalComplex₂.totalAux.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₁₂] [K.HasTotal c₁₂] {i₁ : I₁} {i₁' : I₁} (h : c₁.Rel i₁ i₁') (i₂ : I₂) (i₁₂ : I₁₂) : K.d₁ c₁₂ i₁ i₂ i₁₂ = c₁.ε₁ c₂ c₁₂ (i₁, i₂) • CategoryTheory.CategoryStruct.comp ((K.d i₁ i₁').f i₂) (K.toGradedObject.ιMapObjOrZero (c₁.π c₂ c₁₂) (i₁', i₂) i₁₂)

theorem HomologicalComplex₂.totalAux.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₁₂] [K.HasTotal c₁₂] {i₁ : I₁} {i₁' : I₁} (h : c₁.Rel i₁ i₁') (i₂ : I₂) (i₁₂ : I₁₂) (h' : c₁.π c₂ c₁₂ (i₁', i₂) = i₁₂) : K.d₁ c₁₂ i₁ i₂ i₁₂ = c₁.ε₁ c₂ c₁₂ (i₁, i₂) • CategoryTheory.CategoryStruct.comp ((K.d i₁ i₁').f i₂) (K.toGradedObject.ιMapObj (c₁.π c₂ c₁₂) (i₁', i₂) i₁₂ h')

theorem HomologicalComplex₂.totalAux.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₁₂] [K.HasTotal c₁₂] (i₁ : I₁) {i₂ : I₂} {i₂' : I₂} (h : c₂.Rel i₂ i₂') (i₁₂ : I₁₂) : K.d₂ c₁₂ i₁ i₂ i₁₂ = c₁.ε₂ c₂ c₁₂ (i₁, i₂) • CategoryTheory.CategoryStruct.comp ((K.X i₁).d i₂ i₂') (K.toGradedObject.ιMapObjOrZero (c₁.π c₂ c₁₂) (i₁, i₂') i₁₂)

theorem HomologicalComplex₂.totalAux.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₁₂] [K.HasTotal c₁₂] (i₁ : I₁) {i₂ : I₂} {i₂' : I₂} (h : c₂.Rel i₂ i₂') (i₁₂ : I₁₂) (h' : c₁.π c₂ c₁₂ (i₁, i₂') = i₁₂) : K.d₂ c₁₂ i₁ i₂ i₁₂ = c₁.ε₂ c₂ c₁₂ (i₁, i₂) • CategoryTheory.CategoryStruct.comp ((K.X i₁).d i₂ i₂') (K.toGradedObject.ιMapObj (c₁.π c₂ c₁₂) (i₁, i₂') i₁₂ h')

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₁₂] [K.HasTotal c₁₂] {i₁ : I₁} {i₁' : I₁} (h : c₁.Rel i₁ i₁') (i₂ : I₂) (i₁₂ : I₁₂) (h' : c₁.π c₂ c₁₂ (i₁', i₂) ≠ i₁₂) : K.d₁ 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₁₂] [K.HasTotal c₁₂] (i₁ : I₁) {i₂ : I₂} {i₂' : I₂} (h : c₂.Rel i₂ i₂') (i₁₂ : I₁₂) (h' : c₁.π c₂ c₁₂ (i₁, i₂') ≠ i₁₂) : K.d₂ c₁₂ i₁ i₂ i₁₂ = 0

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₁₂] [K.HasTotal c₁₂] (i₁₂ : I₁₂) (i₁₂' : I₁₂) : K.toGradedObject.mapObj (c₁.π c₂ c₁₂) i₁₂ ⟶ K.toGradedObject.mapObj (c₁.π c₂ c₁₂) i₁₂'

The horizontal differential in the total complex.

Equations

• K.D₁ c₁₂ i₁₂ i₁₂' = K.toGradedObject.descMapObj (c₁.π c₂ c₁₂) fun (x : I₁ × I₂) (x_1 : c₁.π c₂ c₁₂ x = i₁₂) => match x, x_1 with | (i₁, i₂), x => K.d₁ c₁₂ i₁ i₂ 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₁₂] [K.HasTotal c₁₂] (i₁₂ : I₁₂) (i₁₂' : I₁₂) : K.toGradedObject.mapObj (c₁.π c₂ c₁₂) i₁₂ ⟶ K.toGradedObject.mapObj (c₁.π c₂ c₁₂) i₁₂'

The vertical differential in the total complex.

Equations

• K.D₂ c₁₂ i₁₂ i₁₂' = K.toGradedObject.descMapObj (c₁.π c₂ c₁₂) fun (x : I₁ × I₂) (x_1 : c₁.π c₂ c₁₂ x = i₁₂) => match x, x_1 with | (i₁, i₂), x => K.d₂ c₁₂ i₁ i₂ i₁₂'

@[simp]

theorem HomologicalComplex₂.totalAux.ιMapObj_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₁₂] [K.HasTotal c₁₂] (i₁₂ : I₁₂) (i₁₂' : I₁₂) (i : I₁ × I₂) (h : c₁.π c₂ c₁₂ i = i₁₂) {Z : C} (h : K.toGradedObject.mapObj (c₁.π c₂ c₁₂) i₁₂' ⟶ Z) : CategoryTheory.CategoryStruct.comp (K.toGradedObject.ιMapObj (c₁.π c₂ c₁₂) i i₁₂ h✝) (CategoryTheory.CategoryStruct.comp (K.D₁ c₁₂ i₁₂ i₁₂') h) = CategoryTheory.CategoryStruct.comp (K.d₁ c₁₂ i.1 i.2 i₁₂') h

@[simp]

theorem HomologicalComplex₂.totalAux.ιMapObj_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₁₂] [K.HasTotal c₁₂] (i₁₂ : I₁₂) (i₁₂' : I₁₂) (i : I₁ × I₂) (h : c₁.π c₂ c₁₂ i = i₁₂) : CategoryTheory.CategoryStruct.comp (K.toGradedObject.ιMapObj (c₁.π c₂ c₁₂) i i₁₂ h) (K.D₁ c₁₂ i₁₂ i₁₂') = K.d₁ c₁₂ i.1 i.2 i₁₂'

@[simp]

theorem HomologicalComplex₂.totalAux.ιMapObj_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₁₂] [K.HasTotal c₁₂] (i₁₂ : I₁₂) (i₁₂' : I₁₂) (i : I₁ × I₂) (h : c₁.π c₂ c₁₂ i = i₁₂) {Z : C} (h : K.toGradedObject.mapObj (c₁.π c₂ c₁₂) i₁₂' ⟶ Z) : CategoryTheory.CategoryStruct.comp (K.toGradedObject.ιMapObj (c₁.π c₂ c₁₂) i i₁₂ h✝) (CategoryTheory.CategoryStruct.comp (K.D₂ c₁₂ i₁₂ i₁₂') h) = CategoryTheory.CategoryStruct.comp (K.d₂ c₁₂ i.1 i.2 i₁₂') h

@[simp]

theorem HomologicalComplex₂.totalAux.ιMapObj_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₁₂] [K.HasTotal c₁₂] (i₁₂ : I₁₂) (i₁₂' : I₁₂) (i : I₁ × I₂) (h : c₁.π c₂ c₁₂ i = i₁₂) : CategoryTheory.CategoryStruct.comp (K.toGradedObject.ιMapObj (c₁.π c₂ c₁₂) i i₁₂ h) (K.D₂ c₁₂ i₁₂ i₁₂') = K.d₂ 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₁₂] [K.HasTotal c₁₂] (i₁₂ : I₁₂) (i₁₂' : I₁₂) (h₁₂ : ¬c₁₂.Rel i₁₂ i₁₂') : K.D₁ 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₁₂] [K.HasTotal c₁₂] (i₁₂ : I₁₂) (i₁₂' : I₁₂) (h₁₂ : ¬c₁₂.Rel i₁₂ i₁₂') : K.D₂ 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₁₂] [K.HasTotal c₁₂] (i₁₂ : I₁₂) (i₁₂' : I₁₂) (i₁₂'' : I₁₂) {Z : C} (h : K.toGradedObject.mapObj (c₁.π c₂ c₁₂) i₁₂'' ⟶ Z) : CategoryTheory.CategoryStruct.comp (K.D₁ c₁₂ i₁₂ i₁₂') (CategoryTheory.CategoryStruct.comp (K.D₁ 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₁₂] [K.HasTotal c₁₂] (i₁₂ : I₁₂) (i₁₂' : I₁₂) (i₁₂'' : I₁₂) : CategoryTheory.CategoryStruct.comp (K.D₁ c₁₂ i₁₂ i₁₂') (K.D₁ 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₁₂] [K.HasTotal c₁₂] (i₁₂ : I₁₂) (i₁₂' : I₁₂) (i₁₂'' : I₁₂) {Z : C} (h : K.toGradedObject.mapObj (c₁.π c₂ c₁₂) i₁₂'' ⟶ Z) : CategoryTheory.CategoryStruct.comp (K.D₂ c₁₂ i₁₂ i₁₂') (CategoryTheory.CategoryStruct.comp (K.D₂ 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₁₂] [K.HasTotal c₁₂] (i₁₂ : I₁₂) (i₁₂' : I₁₂) (i₁₂'' : I₁₂) : CategoryTheory.CategoryStruct.comp (K.D₂ c₁₂ i₁₂ i₁₂') (K.D₂ 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₁₂] [K.HasTotal c₁₂] (i₁₂ : I₁₂) (i₁₂' : I₁₂) (i₁₂'' : I₁₂) {Z : C} (h : K.toGradedObject.mapObj (c₁.π c₂ c₁₂) i₁₂'' ⟶ Z) : CategoryTheory.CategoryStruct.comp (K.D₂ c₁₂ i₁₂ i₁₂') (CategoryTheory.CategoryStruct.comp (K.D₁ c₁₂ i₁₂' i₁₂'') h) = CategoryTheory.CategoryStruct.comp (-CategoryTheory.CategoryStruct.comp (K.D₁ c₁₂ i₁₂ i₁₂') (K.D₂ 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₁₂] [K.HasTotal c₁₂] (i₁₂ : I₁₂) (i₁₂' : I₁₂) (i₁₂'' : I₁₂) : CategoryTheory.CategoryStruct.comp (K.D₂ c₁₂ i₁₂ i₁₂') (K.D₁ c₁₂ i₁₂' i₁₂'') = -CategoryTheory.CategoryStruct.comp (K.D₁ c₁₂ i₁₂ i₁₂') (K.D₂ 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₁₂] [K.HasTotal c₁₂] (i₁₂ : I₁₂) (i₁₂' : I₁₂) (i₁₂'' : I₁₂) {Z : C} (h : K.toGradedObject.mapObj (c₁.π c₂ c₁₂) i₁₂'' ⟶ Z) : CategoryTheory.CategoryStruct.comp (K.D₁ c₁₂ i₁₂ i₁₂') (CategoryTheory.CategoryStruct.comp (K.D₂ c₁₂ i₁₂' i₁₂'') h) = CategoryTheory.CategoryStruct.comp (-CategoryTheory.CategoryStruct.comp (K.D₂ c₁₂ i₁₂ i₁₂') (K.D₁ 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₁₂] [K.HasTotal c₁₂] (i₁₂ : I₁₂) (i₁₂' : I₁₂) (i₁₂'' : I₁₂) : CategoryTheory.CategoryStruct.comp (K.D₁ c₁₂ i₁₂ i₁₂') (K.D₂ c₁₂ i₁₂' i₁₂'') = -CategoryTheory.CategoryStruct.comp (K.D₂ c₁₂ i₁₂ i₁₂') (K.D₁ 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₁₂] [K.HasTotal c₁₂] (i₁₂ : I₁₂) (i₁₂' : I₁₂) : (K.total c₁₂).d i₁₂ i₁₂' = K.D₁ c₁₂ i₁₂ i₁₂' + K.D₂ c₁₂ i₁₂ i₁₂'

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₁₂] [K.HasTotal c₁₂] : HomologicalComplex C c₁₂

The total complex of a bicomplex.

Equations

• K.total c₁₂ = { X := K.toGradedObject.mapObj (c₁.π c₂ c₁₂), d := fun (i₁₂ i₁₂' : I₁₂) => K.D₁ c₁₂ i₁₂ i₁₂' + K.D₂ c₁₂ i₁₂ i₁₂', shape := ⋯, d_comp_d' := ⋯ }

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₁₂] [K.HasTotal c₁₂] (i₁ : I₁) (i₂ : I₂) (i₁₂ : I₁₂) (h : c₁.π c₂ c₁₂ (i₁, i₂) = i₁₂) : (K.X i₁).X i₂ ⟶ (K.total c₁₂).X i₁₂

The inclusion of a summand in the total complex.

Equations

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

@[simp]

theorem HomologicalComplex₂.XXIsoOfEq_hom_ιTotal_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₁₂] [K.HasTotal c₁₂] {x₁ : I₁} {y₁ : I₁} (h₁ : x₁ = y₁) {x₂ : I₂} {y₂ : I₂} (h₂ : x₂ = y₂) (i₁₂ : I₁₂) (h : c₁.π c₂ c₁₂ (y₁, y₂) = i₁₂) {Z : C} (h : (K.total c₁₂).X i₁₂ ⟶ Z) : CategoryTheory.CategoryStruct.comp (HomologicalComplex₂.XXIsoOfEq C c₁ c₂ K h₁ h₂).hom (CategoryTheory.CategoryStruct.comp (K.ιTotal c₁₂ y₁ y₂ i₁₂ h✝) h) = CategoryTheory.CategoryStruct.comp (K.ιTotal c₁₂ x₁ x₂ i₁₂ ⋯) h

@[simp]

theorem HomologicalComplex₂.XXIsoOfEq_hom_ι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₁₂] [K.HasTotal c₁₂] {x₁ : I₁} {y₁ : I₁} (h₁ : x₁ = y₁) {x₂ : I₂} {y₂ : I₂} (h₂ : x₂ = y₂) (i₁₂ : I₁₂) (h : c₁.π c₂ c₁₂ (y₁, y₂) = i₁₂) : CategoryTheory.CategoryStruct.comp (HomologicalComplex₂.XXIsoOfEq C c₁ c₂ K h₁ h₂).hom (K.ιTotal c₁₂ y₁ y₂ i₁₂ h) = K.ιTotal c₁₂ x₁ x₂ i₁₂ ⋯

@[simp]

theorem HomologicalComplex₂.XXIsoOfEq_inv_ιTotal_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₁₂] [K.HasTotal c₁₂] {x₁ : I₁} {y₁ : I₁} (h₁ : x₁ = y₁) {x₂ : I₂} {y₂ : I₂} (h₂ : x₂ = y₂) (i₁₂ : I₁₂) (h : c₁.π c₂ c₁₂ (x₁, x₂) = i₁₂) {Z : C} (h : (K.total c₁₂).X i₁₂ ⟶ Z) : CategoryTheory.CategoryStruct.comp (HomologicalComplex₂.XXIsoOfEq C c₁ c₂ K h₁ h₂).inv (CategoryTheory.CategoryStruct.comp (K.ιTotal c₁₂ x₁ x₂ i₁₂ h✝) h) = CategoryTheory.CategoryStruct.comp (K.ιTotal c₁₂ y₁ y₂ i₁₂ ⋯) h

@[simp]

theorem HomologicalComplex₂.XXIsoOfEq_inv_ι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₁₂] [K.HasTotal c₁₂] {x₁ : I₁} {y₁ : I₁} (h₁ : x₁ = y₁) {x₂ : I₂} {y₂ : I₂} (h₂ : x₂ = y₂) (i₁₂ : I₁₂) (h : c₁.π c₂ c₁₂ (x₁, x₂) = i₁₂) : CategoryTheory.CategoryStruct.comp (HomologicalComplex₂.XXIsoOfEq C c₁ c₂ K h₁ h₂).inv (K.ιTotal c₁₂ x₁ x₂ i₁₂ h) = K.ιTotal c₁₂ y₁ y₂ i₁₂ ⋯

noncomputable def 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₁₂] [K.HasTotal c₁₂] (i₁ : I₁) (i₂ : I₂) (i₁₂ : I₁₂) : (K.X i₁).X i₂ ⟶ (K.total c₁₂).X i₁₂

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

Equations

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

theorem HomologicalComplex₂.ιTotalOrZero_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₁₂] [K.HasTotal c₁₂] (i₁ : I₁) (i₂ : I₂) (i₁₂ : I₁₂) (h : c₁.π c₂ c₁₂ (i₁, i₂) = i₁₂) : K.ιTotalOrZero c₁₂ i₁ i₂ i₁₂ = K.ιTotal c₁₂ i₁ i₂ i₁₂ h

theorem HomologicalComplex₂.ιTotalOrZero_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₁₂] [K.HasTotal c₁₂] (i₁ : I₁) (i₂ : I₂) (i₁₂ : I₁₂) (h : c₁.π c₂ c₁₂ (i₁, i₂) ≠ i₁₂) : K.ιTotalOrZero c₁₂ i₁ i₂ i₁₂ = 0

@[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₁₂] [K.HasTotal c₁₂] (i₁₂ : I₁₂) (i₁₂' : I₁₂) (i₁ : I₁) (i₂ : I₂) (h : c₁.π c₂ c₁₂ (i₁, i₂) = i₁₂) {Z : C} (h : K.toGradedObject.mapObj (c₁.π c₂ c₁₂) i₁₂' ⟶ Z) : CategoryTheory.CategoryStruct.comp (K.ιTotal c₁₂ i₁ i₂ i₁₂ h✝) (CategoryTheory.CategoryStruct.comp (K.D₁ c₁₂ i₁₂ i₁₂') h) = CategoryTheory.CategoryStruct.comp (K.d₁ c₁₂ i₁ i₂ 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₁₂] [K.HasTotal c₁₂] (i₁₂ : I₁₂) (i₁₂' : I₁₂) (i₁ : I₁) (i₂ : I₂) (h : c₁.π c₂ c₁₂ (i₁, i₂) = i₁₂) : CategoryTheory.CategoryStruct.comp (K.ιTotal c₁₂ i₁ i₂ i₁₂ h) (K.D₁ c₁₂ i₁₂ i₁₂') = K.d₁ c₁₂ i₁ i₂ i₁₂'

@[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₁₂] [K.HasTotal c₁₂] (i₁₂ : I₁₂) (i₁₂' : I₁₂) (i₁ : I₁) (i₂ : I₂) (h : c₁.π c₂ c₁₂ (i₁, i₂) = i₁₂) {Z : C} (h : K.toGradedObject.mapObj (c₁.π c₂ c₁₂) i₁₂' ⟶ Z) : CategoryTheory.CategoryStruct.comp (K.ιTotal c₁₂ i₁ i₂ i₁₂ h✝) (CategoryTheory.CategoryStruct.comp (K.D₂ c₁₂ i₁₂ i₁₂') h) = CategoryTheory.CategoryStruct.comp (K.d₂ c₁₂ i₁ i₂ 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₁₂] [K.HasTotal c₁₂] (i₁₂ : I₁₂) (i₁₂' : I₁₂) (i₁ : I₁) (i₂ : I₂) (h : c₁.π c₂ c₁₂ (i₁, i₂) = i₁₂) : CategoryTheory.CategoryStruct.comp (K.ιTotal c₁₂ i₁ i₂ i₁₂ h) (K.D₂ c₁₂ i₁₂ i₁₂') = K.d₂ c₁₂ i₁ i₂ i₁₂'

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₁₂] [K.HasTotal c₁₂] {i₁ : I₁} {i₁' : I₁} (h : c₁.Rel i₁ i₁') (i₂ : I₂) (i₁₂ : I₁₂) : K.d₁ c₁₂ i₁ i₂ i₁₂ = c₁.ε₁ c₂ c₁₂ (i₁, i₂) • CategoryTheory.CategoryStruct.comp ((K.d i₁ i₁').f i₂) (K.ιTotalOrZero c₁₂ i₁' i₂ i₁₂)

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₁₂] [K.HasTotal c₁₂] {i₁ : I₁} {i₁' : I₁} (h : c₁.Rel i₁ i₁') (i₂ : I₂) (i₁₂ : I₁₂) (h' : c₁.π c₂ c₁₂ (i₁', i₂) = i₁₂) : K.d₁ c₁₂ i₁ i₂ i₁₂ = c₁.ε₁ c₂ c₁₂ (i₁, i₂) • CategoryTheory.CategoryStruct.comp ((K.d i₁ i₁').f i₂) (K.ιTotal 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₁₂] [K.HasTotal c₁₂] (i₁ : I₁) {i₂ : I₂} {i₂' : I₂} (h : c₂.Rel i₂ i₂') (i₁₂ : I₁₂) : K.d₂ c₁₂ i₁ i₂ i₁₂ = c₁.ε₂ c₂ c₁₂ (i₁, i₂) • CategoryTheory.CategoryStruct.comp ((K.X i₁).d i₂ i₂') (K.ιTotalOrZero c₁₂ i₁ i₂' i₁₂)

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₁₂] [K.HasTotal c₁₂] (i₁ : I₁) {i₂ : I₂} {i₂' : I₂} (h : c₂.Rel i₂ i₂') (i₁₂ : I₁₂) (h' : c₁.π c₂ c₁₂ (i₁, i₂') = i₁₂) : K.d₂ c₁₂ i₁ i₂ i₁₂ = c₁.ε₂ c₂ c₁₂ (i₁, i₂) • CategoryTheory.CategoryStruct.comp ((K.X i₁).d i₂ i₂') (K.ιTotal c₁₂ i₁ i₂' i₁₂ h')

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₁₂] [K.HasTotal c₁₂] {A : C} {i₁₂ : I₁₂} (f : (i₁ : I₁) → (i₂ : I₂) → c₁.π c₂ c₁₂ (i₁, i₂) = i₁₂ → ((K.X i₁).X i₂ ⟶ A)) : (K.total c₁₂).X i₁₂ ⟶ A

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

Equations

• K.totalDesc f = K.toGradedObject.descMapObj (c₁.π c₂ c₁₂) fun (x : I₁ × I₂) (hi : c₁.π c₂ c₁₂ x = i₁₂) => match x, hi with | (i₁, i₂), hi => f i₁ i₂ hi

@[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₁₂] [K.HasTotal c₁₂] {A : C} {i₁₂ : I₁₂} (f : (i₁ : I₁) → (i₂ : I₂) → c₁.π c₂ c₁₂ (i₁, i₂) = i₁₂ → ((K.X i₁).X i₂ ⟶ A)) (i₁ : I₁) (i₂ : I₂) (hi : c₁.π c₂ c₁₂ (i₁, i₂) = i₁₂) {Z : C} (h : A ⟶ Z) : CategoryTheory.CategoryStruct.comp (K.ιTotal c₁₂ i₁ i₂ i₁₂ hi) (CategoryTheory.CategoryStruct.comp (K.totalDesc 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₁₂] [K.HasTotal c₁₂] {A : C} {i₁₂ : I₁₂} (f : (i₁ : I₁) → (i₂ : I₂) → c₁.π c₂ c₁₂ (i₁, i₂) = i₁₂ → ((K.X i₁).X i₂ ⟶ A)) (i₁ : I₁) (i₂ : I₂) (hi : c₁.π c₂ c₁₂ (i₁, i₂) = i₁₂) : CategoryTheory.CategoryStruct.comp (K.ιTotal c₁₂ i₁ i₂ i₁₂ hi) (K.totalDesc 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₁₂] [K.HasTotal c₁₂] {A : C} {i₁₂ : I₁₂} {f : (K.total c₁₂).X i₁₂ ⟶ A} {g : (K.total c₁₂).X i₁₂ ⟶ A} (h : ∀ (i₁ : I₁) (i₂ : I₂) (hi : c₁.π c₂ c₁₂ (i₁, i₂) = i₁₂), CategoryTheory.CategoryStruct.comp (K.ιTotal c₁₂ i₁ i₂ i₁₂ hi) f = CategoryTheory.CategoryStruct.comp (K.ιTotal c₁₂ i₁ i₂ i₁₂ hi) g) : f = g

@[simp]

theorem HomologicalComplex₂.total.mapAux.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₁₂] [K.HasTotal c₁₂] [L.HasTotal c₁₂] (i₁ : I₁) (i₂ : I₂) (i₁₂ : I₁₂) {Z : C} (h : L.toGradedObject.mapObj (c₁.π c₂ c₁₂) i₁₂ ⟶ Z) : CategoryTheory.CategoryStruct.comp (K.d₁ c₁₂ i₁ i₂ i₁₂) (CategoryTheory.CategoryStruct.comp (CategoryTheory.GradedObject.mapMap (HomologicalComplex₂.toGradedObjectMap φ) (c₁.π c₂ c₁₂) i₁₂) h) = CategoryTheory.CategoryStruct.comp ((φ.f i₁).f i₂) (CategoryTheory.CategoryStruct.comp (L.d₁ c₁₂ i₁ i₂ i₁₂) h)

@[simp]

theorem HomologicalComplex₂.total.mapAux.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₁₂] [K.HasTotal c₁₂] [L.HasTotal c₁₂] (i₁ : I₁) (i₂ : I₂) (i₁₂ : I₁₂) : CategoryTheory.CategoryStruct.comp (K.d₁ c₁₂ i₁ i₂ i₁₂) (CategoryTheory.GradedObject.mapMap (HomologicalComplex₂.toGradedObjectMap φ) (c₁.π c₂ c₁₂) i₁₂) = CategoryTheory.CategoryStruct.comp ((φ.f i₁).f i₂) (L.d₁ c₁₂ i₁ i₂ i₁₂)

@[simp]

theorem HomologicalComplex₂.total.mapAux.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₁₂] [K.HasTotal c₁₂] [L.HasTotal c₁₂] (i₁ : I₁) (i₂ : I₂) (i₁₂ : I₁₂) {Z : C} (h : L.toGradedObject.mapObj (c₁.π c₂ c₁₂) i₁₂ ⟶ Z) : CategoryTheory.CategoryStruct.comp (K.d₂ c₁₂ i₁ i₂ i₁₂) (CategoryTheory.CategoryStruct.comp (CategoryTheory.GradedObject.mapMap (HomologicalComplex₂.toGradedObjectMap φ) (c₁.π c₂ c₁₂) i₁₂) h) = CategoryTheory.CategoryStruct.comp ((φ.f i₁).f i₂) (CategoryTheory.CategoryStruct.comp (L.d₂ c₁₂ i₁ i₂ i₁₂) h)

@[simp]

theorem HomologicalComplex₂.total.mapAux.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₁₂] [K.HasTotal c₁₂] [L.HasTotal c₁₂] (i₁ : I₁) (i₂ : I₂) (i₁₂ : I₁₂) : CategoryTheory.CategoryStruct.comp (K.d₂ c₁₂ i₁ i₂ i₁₂) (CategoryTheory.GradedObject.mapMap (HomologicalComplex₂.toGradedObjectMap φ) (c₁.π c₂ c₁₂) i₁₂) = CategoryTheory.CategoryStruct.comp ((φ.f i₁).f i₂) (L.d₂ c₁₂ i₁ i₂ i₁₂)

theorem HomologicalComplex₂.total.mapAux.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₁₂] [K.HasTotal c₁₂] [L.HasTotal c₁₂] (i₁₂ : I₁₂) (i₁₂' : I₁₂) {Z : C} (h : L.toGradedObject.mapObj (c₁.π c₂ c₁₂) i₁₂' ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.GradedObject.mapMap (HomologicalComplex₂.toGradedObjectMap φ) (c₁.π c₂ c₁₂) i₁₂) (CategoryTheory.CategoryStruct.comp (L.D₁ c₁₂ i₁₂ i₁₂') h) = CategoryTheory.CategoryStruct.comp (K.D₁ c₁₂ i₁₂ i₁₂') (CategoryTheory.CategoryStruct.comp (CategoryTheory.GradedObject.mapMap (HomologicalComplex₂.toGradedObjectMap φ) (c₁.π c₂ c₁₂) i₁₂') h)

theorem HomologicalComplex₂.total.mapAux.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₁₂] [K.HasTotal c₁₂] [L.HasTotal c₁₂] (i₁₂ : I₁₂) (i₁₂' : I₁₂) : CategoryTheory.CategoryStruct.comp (CategoryTheory.GradedObject.mapMap (HomologicalComplex₂.toGradedObjectMap φ) (c₁.π c₂ c₁₂) i₁₂) (L.D₁ c₁₂ i₁₂ i₁₂') = CategoryTheory.CategoryStruct.comp (K.D₁ c₁₂ i₁₂ i₁₂') (CategoryTheory.GradedObject.mapMap (HomologicalComplex₂.toGradedObjectMap φ) (c₁.π c₂ c₁₂) i₁₂')

theorem HomologicalComplex₂.total.mapAux.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₁₂] [K.HasTotal c₁₂] [L.HasTotal c₁₂] (i₁₂ : I₁₂) (i₁₂' : I₁₂) {Z : C} (h : L.toGradedObject.mapObj (c₁.π c₂ c₁₂) i₁₂' ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.GradedObject.mapMap (HomologicalComplex₂.toGradedObjectMap φ) (c₁.π c₂ c₁₂) i₁₂) (CategoryTheory.CategoryStruct.comp (L.D₂ c₁₂ i₁₂ i₁₂') h) = CategoryTheory.CategoryStruct.comp (K.D₂ c₁₂ i₁₂ i₁₂') (CategoryTheory.CategoryStruct.comp (CategoryTheory.GradedObject.mapMap (HomologicalComplex₂.toGradedObjectMap φ) (c₁.π c₂ c₁₂) i₁₂') h)

theorem HomologicalComplex₂.total.mapAux.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₁₂] [K.HasTotal c₁₂] [L.HasTotal c₁₂] (i₁₂ : I₁₂) (i₁₂' : I₁₂) : CategoryTheory.CategoryStruct.comp (CategoryTheory.GradedObject.mapMap (HomologicalComplex₂.toGradedObjectMap φ) (c₁.π c₂ c₁₂) i₁₂) (L.D₂ c₁₂ i₁₂ i₁₂') = CategoryTheory.CategoryStruct.comp (K.D₂ c₁₂ i₁₂ i₁₂') (CategoryTheory.GradedObject.mapMap (HomologicalComplex₂.toGradedObjectMap φ) (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₁₂] [K.HasTotal c₁₂] [L.HasTotal c₁₂] : K.total c₁₂ ⟶ L.total 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 φ) (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₁₂] [K.HasTotal c₁₂] [L.HasTotal c₁₂] : (HomologicalComplex.forget C c₁₂).map (HomologicalComplex₂.total.map φ c₁₂) = CategoryTheory.GradedObject.mapMap (HomologicalComplex₂.toGradedObjectMap φ) (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₁₂] [K.HasTotal c₁₂] : HomologicalComplex₂.total.map (CategoryTheory.CategoryStruct.id K) c₁₂ = CategoryTheory.CategoryStruct.id (K.total 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₁₂] [K.HasTotal c₁₂] [L.HasTotal c₁₂] [M.HasTotal c₁₂] {Z : HomologicalComplex C c₁₂} (h : M.total 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₁₂] [K.HasTotal c₁₂] [L.HasTotal c₁₂] [M.HasTotal c₁₂] : HomologicalComplex₂.total.map (CategoryTheory.CategoryStruct.comp φ ψ) c₁₂ = CategoryTheory.CategoryStruct.comp (HomologicalComplex₂.total.map φ c₁₂) (HomologicalComplex₂.total.map ψ c₁₂)

@[simp]

theorem HomologicalComplex₂.total.mapIso_inv {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₂} (e : K ≅ L) (c₁₂ : ComplexShape I₁₂) [DecidableEq I₁₂] [TotalComplexShape c₁ c₂ c₁₂] [K.HasTotal c₁₂] [L.HasTotal c₁₂] : (HomologicalComplex₂.total.mapIso e c₁₂).inv = HomologicalComplex₂.total.map e.inv c₁₂

@[simp]

theorem HomologicalComplex₂.total.mapIso_hom {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₂} (e : K ≅ L) (c₁₂ : ComplexShape I₁₂) [DecidableEq I₁₂] [TotalComplexShape c₁ c₂ c₁₂] [K.HasTotal c₁₂] [L.HasTotal c₁₂] : (HomologicalComplex₂.total.mapIso e c₁₂).hom = HomologicalComplex₂.total.map e.hom c₁₂

noncomputable def HomologicalComplex₂.total.mapIso {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₂} (e : K ≅ L) (c₁₂ : ComplexShape I₁₂) [DecidableEq I₁₂] [TotalComplexShape c₁ c₂ c₁₂] [K.HasTotal c₁₂] [L.HasTotal c₁₂] : K.total c₁₂ ≅ L.total c₁₂

The isomorphism K.total c₁₂ ≅ L.total c₁₂ of homological complexes induced by an isomorphism of bicomplexes K ≅ L.

Equations

• HomologicalComplex₂.total.mapIso e c₁₂ = { hom := HomologicalComplex₂.total.map e.hom c₁₂, inv := HomologicalComplex₂.total.map e.inv c₁₂, hom_inv_id := ⋯, inv_hom_id := ⋯ }

@[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₁₂] [K.HasTotal c₁₂] [L.HasTotal c₁₂] (i₁ : I₁) (i₂ : I₂) (i₁₂ : I₁₂) (h : c₁.π c₂ c₁₂ (i₁, i₂) = i₁₂) {Z : C} (h : (L.total c₁₂).X i₁₂ ⟶ Z) : CategoryTheory.CategoryStruct.comp (K.ιTotal 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 (L.ιTotal 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₁₂] [K.HasTotal c₁₂] [L.HasTotal c₁₂] (i₁ : I₁) (i₂ : I₂) (i₁₂ : I₁₂) (h : c₁.π c₂ c₁₂ (i₁, i₂) = i₁₂) : CategoryTheory.CategoryStruct.comp (K.ιTotal c₁₂ i₁ i₂ i₁₂ h) ((HomologicalComplex₂.total.map φ c₁₂).f i₁₂) = CategoryTheory.CategoryStruct.comp ((φ.f i₁).f i₂) (L.ιTotal 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₁₂] [K.HasTotal c₁₂] [L.HasTotal c₁₂] (i₁ : I₁) (i₂ : I₂) (i₁₂ : I₁₂) {Z : C} (h : (L.total c₁₂).X i₁₂ ⟶ Z) : CategoryTheory.CategoryStruct.comp (K.ιTotalOrZero c₁₂ i₁ i₂ i₁₂) (CategoryTheory.CategoryStruct.comp ((HomologicalComplex₂.total.map φ c₁₂).f i₁₂) h) = CategoryTheory.CategoryStruct.comp ((φ.f i₁).f i₂) (CategoryTheory.CategoryStruct.comp (L.ιTotalOrZero 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₁₂] [K.HasTotal c₁₂] [L.HasTotal c₁₂] (i₁ : I₁) (i₂ : I₂) (i₁₂ : I₁₂) : CategoryTheory.CategoryStruct.comp (K.ιTotalOrZero c₁₂ i₁ i₂ i₁₂) ((HomologicalComplex₂.total.map φ c₁₂).f i₁₂) = CategoryTheory.CategoryStruct.comp ((φ.f i₁).f i₂) (L.ιTotalOrZero 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₂), K.HasTotal 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₂), K.HasTotal c₁₂] (K : HomologicalComplex₂ C c₁ c₂) : (HomologicalComplex₂.totalFunctor C c₁ c₂ c₁₂).obj K = K.total 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₂), K.HasTotal 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.