Behaviour of the total complex with respect to shifts

There are two ways to shift objects in HomologicalComplex₂ C (up ℤ) (up ℤ):

• by shifting the first indices (and changing signs of horizontal differentials), which corresponds to the shift by ℤ on CochainComplex (CochainComplex C ℤ) ℤ.
• by shifting the second indices (and changing signs of vertical differentials).

These two sorts of shift functors shall be abbreviated as HomologicalComplex₂.shiftFunctor₁ C x and HomologicalComplex₂.shiftFunctor₂ C y.

In this file, for any K : HomologicalComplex₂ C (up ℤ) (up ℤ), we define an isomorphism K.totalShift₁Iso x : ((shiftFunctor₁ C x).obj K).total (up ℤ) ≅ (K.total (up ℤ))⟦x⟧ for any x : ℤ (which does not involve signs) and an isomorphism K.totalShift₂Iso y : ((shiftFunctor₂ C y).obj K).total (up ℤ) ≅ (K.total (up ℤ))⟦y⟧ for any y : ℤ (which is given by the multiplication by (p * y).negOnePow on the summand in bidegree (p, q) of K).

Depending on the order of the "composition" of the two isomorphisms totalShift₁Iso and totalShift₂Iso, we get two ways to identify ((shiftFunctor₁ C x).obj ((shiftFunctor₂ C y).obj K)).total (up ℤ) and (K.total (up ℤ))⟦x + y⟧. The lemma totalShift₁Iso_trans_totalShift₂Iso shows that these two compositions of isomorphisms differ by the sign (x * y).negOnePow.

@[reducible, inline]

abbrev HomologicalComplex₂.shiftFunctor₁ (C : Type u_1) [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] (x : ℤ) : CategoryTheory.Functor (HomologicalComplex₂ C (ComplexShape.up ℤ) (ComplexShape.up ℤ)) (HomologicalComplex₂ C (ComplexShape.up ℤ) (ComplexShape.up ℤ))

The shift on bicomplexes obtained by shifting the first indices (and changing the sign of differentials).

@[reducible, inline]

abbrev HomologicalComplex₂.shiftFunctor₂ (C : Type u_1) [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] (y : ℤ) : CategoryTheory.Functor (HomologicalComplex₂ C (ComplexShape.up ℤ) (ComplexShape.up ℤ)) (HomologicalComplex₂ C (ComplexShape.up ℤ) (ComplexShape.up ℤ))

The shift on bicomplexes obtained by shifting the second indices (and changing the sign of differentials).

def HomologicalComplex₂.shiftFunctor₁XXIso {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] (K : HomologicalComplex₂ C (ComplexShape.up ℤ) (ComplexShape.up ℤ)) (a x a' : ℤ) (h : a' = a + x) (b : ℤ) : (((shiftFunctor₁ C x).obj K).X a).X b ≅ (K.X a').X b

The isomorphism (((shiftFunctor₁ C x).obj K).X a).X b ≅ (K.X a').X b when a' = a + x.

def HomologicalComplex₂.shiftFunctor₂XXIso {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] (K : HomologicalComplex₂ C (ComplexShape.up ℤ) (ComplexShape.up ℤ)) (a b y b' : ℤ) (h : b' = b + y) : (((shiftFunctor₂ C y).obj K).X a).X b ≅ (K.X a).X b'

The isomorphism (((shiftFunctor₂ C y).obj K).X a).X b ≅ (K.X a).X b' when b' = b + y.

@[simp]

theorem HomologicalComplex₂.shiftFunctor₁XXIso_refl {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] (K : HomologicalComplex₂ C (ComplexShape.up ℤ) (ComplexShape.up ℤ)) (a b x : ℤ) : K.shiftFunctor₁XXIso a x (a + x) ⋯ b = CategoryTheory.Iso.refl ((((shiftFunctor₁ C x).obj K).X a).X b)

@[simp]

theorem HomologicalComplex₂.shiftFunctor₂XXIso_refl {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] (K : HomologicalComplex₂ C (ComplexShape.up ℤ) (ComplexShape.up ℤ)) (a b y : ℤ) : K.shiftFunctor₂XXIso a b y (b + y) ⋯ = CategoryTheory.Iso.refl ((((shiftFunctor₂ C y).obj K).X a).X b)

instance HomologicalComplex₂.instHasTotalIntObjUpShiftFunctor₁ {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] (K : HomologicalComplex₂ C (ComplexShape.up ℤ) (ComplexShape.up ℤ)) (x : ℤ) [K.HasTotal (ComplexShape.up ℤ)] : ((shiftFunctor₁ C x).obj K).HasTotal (ComplexShape.up ℤ)

instance HomologicalComplex₂.instHasTotalIntObjUpShiftFunctor₂ {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] (K : HomologicalComplex₂ C (ComplexShape.up ℤ) (ComplexShape.up ℤ)) (y : ℤ) [K.HasTotal (ComplexShape.up ℤ)] : ((shiftFunctor₂ C y).obj K).HasTotal (ComplexShape.up ℤ)

instance HomologicalComplex₂.instHasTotalIntObjUpCompShiftFunctor₂ShiftFunctor₁ {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] (K : HomologicalComplex₂ C (ComplexShape.up ℤ) (ComplexShape.up ℤ)) (x y : ℤ) [K.HasTotal (ComplexShape.up ℤ)] : (((shiftFunctor₂ C y).comp (shiftFunctor₁ C x)).obj K).HasTotal (ComplexShape.up ℤ)

instance HomologicalComplex₂.instHasTotalIntObjUpCompShiftFunctor₁ShiftFunctor₂ {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] (K : HomologicalComplex₂ C (ComplexShape.up ℤ) (ComplexShape.up ℤ)) (x y : ℤ) [K.HasTotal (ComplexShape.up ℤ)] : (((shiftFunctor₁ C x).comp (shiftFunctor₂ C y)).obj K).HasTotal (ComplexShape.up ℤ)

noncomputable def HomologicalComplex₂.totalShift₁XIso {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] (K : HomologicalComplex₂ C (ComplexShape.up ℤ) (ComplexShape.up ℤ)) (x : ℤ) [K.HasTotal (ComplexShape.up ℤ)] (n n' : ℤ) (h : n + x = n') : (((shiftFunctor₁ C x).obj K).total (ComplexShape.up ℤ)).X n ≅ (K.total (ComplexShape.up ℤ)).X n'

Auxiliary definition for totalShift₁Iso.

theorem HomologicalComplex₂.D₁_totalShift₁XIso_hom {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] (K : HomologicalComplex₂ C (ComplexShape.up ℤ) (ComplexShape.up ℤ)) (x : ℤ) [K.HasTotal (ComplexShape.up ℤ)] (n₀ n₁ n₀' n₁' : ℤ) (h₀ : n₀ + x = n₀') (h₁ : n₁ + x = n₁') : CategoryTheory.CategoryStruct.comp (((shiftFunctor₁ C x).obj K).D₁ (ComplexShape.up ℤ) n₀ n₁) (K.totalShift₁XIso x n₁ n₁' h₁).hom = x.negOnePow • CategoryTheory.CategoryStruct.comp (K.totalShift₁XIso x n₀ n₀' h₀).hom (K.D₁ (ComplexShape.up ℤ) n₀' n₁')

theorem HomologicalComplex₂.D₁_totalShift₁XIso_hom_assoc {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] (K : HomologicalComplex₂ C (ComplexShape.up ℤ) (ComplexShape.up ℤ)) (x : ℤ) [K.HasTotal (ComplexShape.up ℤ)] (n₀ n₁ n₀' n₁' : ℤ) (h₀ : n₀ + x = n₀') (h₁ : n₁ + x = n₁') {Z : C} (h : (K.total (ComplexShape.up ℤ)).X n₁' ⟶ Z) : CategoryTheory.CategoryStruct.comp (((shiftFunctor₁ C x).obj K).D₁ (ComplexShape.up ℤ) n₀ n₁) (CategoryTheory.CategoryStruct.comp (K.totalShift₁XIso x n₁ n₁' h₁).hom h) = CategoryTheory.CategoryStruct.comp (x.negOnePow • CategoryTheory.CategoryStruct.comp (K.totalShift₁XIso x n₀ n₀' h₀).hom (K.D₁ (ComplexShape.up ℤ) n₀' n₁')) h

theorem HomologicalComplex₂.D₂_totalShift₁XIso_hom {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] (K : HomologicalComplex₂ C (ComplexShape.up ℤ) (ComplexShape.up ℤ)) (x : ℤ) [K.HasTotal (ComplexShape.up ℤ)] (n₀ n₁ n₀' n₁' : ℤ) (h₀ : n₀ + x = n₀') (h₁ : n₁ + x = n₁') : CategoryTheory.CategoryStruct.comp (((shiftFunctor₁ C x).obj K).D₂ (ComplexShape.up ℤ) n₀ n₁) (K.totalShift₁XIso x n₁ n₁' h₁).hom = x.negOnePow • CategoryTheory.CategoryStruct.comp (K.totalShift₁XIso x n₀ n₀' h₀).hom (K.D₂ (ComplexShape.up ℤ) n₀' n₁')

theorem HomologicalComplex₂.D₂_totalShift₁XIso_hom_assoc {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] (K : HomologicalComplex₂ C (ComplexShape.up ℤ) (ComplexShape.up ℤ)) (x : ℤ) [K.HasTotal (ComplexShape.up ℤ)] (n₀ n₁ n₀' n₁' : ℤ) (h₀ : n₀ + x = n₀') (h₁ : n₁ + x = n₁') {Z : C} (h : (K.total (ComplexShape.up ℤ)).X n₁' ⟶ Z) : CategoryTheory.CategoryStruct.comp (((shiftFunctor₁ C x).obj K).D₂ (ComplexShape.up ℤ) n₀ n₁) (CategoryTheory.CategoryStruct.comp (K.totalShift₁XIso x n₁ n₁' h₁).hom h) = CategoryTheory.CategoryStruct.comp (x.negOnePow • CategoryTheory.CategoryStruct.comp (K.totalShift₁XIso x n₀ n₀' h₀).hom (K.D₂ (ComplexShape.up ℤ) n₀' n₁')) h

noncomputable def HomologicalComplex₂.totalShift₁Iso {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] (K : HomologicalComplex₂ C (ComplexShape.up ℤ) (ComplexShape.up ℤ)) (x : ℤ) [K.HasTotal (ComplexShape.up ℤ)] : ((shiftFunctor₁ C x).obj K).total (ComplexShape.up ℤ) ≅ (CategoryTheory.shiftFunctor (HomologicalComplex C (ComplexShape.up ℤ)) x).obj (K.total (ComplexShape.up ℤ))

The isomorphism ((shiftFunctor₁ C x).obj K).total (up ℤ) ≅ (K.total (up ℤ))⟦x⟧ expressing the compatibility of the total complex with the shift on the first indices. This isomorphism does not involve signs.

theorem HomologicalComplex₂.ι_totalShift₁Iso_hom_f {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] (K : HomologicalComplex₂ C (ComplexShape.up ℤ) (ComplexShape.up ℤ)) (x : ℤ) [K.HasTotal (ComplexShape.up ℤ)] (a b n : ℤ) (h : a + b = n) (a' : ℤ) (ha' : a' = a + x) (n' : ℤ) (hn' : n' = n + x) : CategoryTheory.CategoryStruct.comp (((shiftFunctor₁ C x).obj K).ιTotal (ComplexShape.up ℤ) a b n h) ((K.totalShift₁Iso x).hom.f n) = CategoryTheory.CategoryStruct.comp (K.shiftFunctor₁XXIso a x a' ha' b).hom (CategoryTheory.CategoryStruct.comp (K.ιTotal (ComplexShape.up ℤ) a' b n' ⋯) (CochainComplex.shiftFunctorObjXIso (K.total (ComplexShape.up ℤ)) x n n' hn').inv)

theorem HomologicalComplex₂.ι_totalShift₁Iso_hom_f_assoc {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] (K : HomologicalComplex₂ C (ComplexShape.up ℤ) (ComplexShape.up ℤ)) (x : ℤ) [K.HasTotal (ComplexShape.up ℤ)] (a b n : ℤ) (h : a + b = n) (a' : ℤ) (ha' : a' = a + x) (n' : ℤ) (hn' : n' = n + x) {Z : C} (h✝ : ((CategoryTheory.shiftFunctor (HomologicalComplex C (ComplexShape.up ℤ)) x).obj (K.total (ComplexShape.up ℤ))).X n ⟶ Z) : CategoryTheory.CategoryStruct.comp (((shiftFunctor₁ C x).obj K).ιTotal (ComplexShape.up ℤ) a b n h) (CategoryTheory.CategoryStruct.comp ((K.totalShift₁Iso x).hom.f n) h✝) = CategoryTheory.CategoryStruct.comp (K.shiftFunctor₁XXIso a x a' ha' b).hom (CategoryTheory.CategoryStruct.comp (K.ιTotal (ComplexShape.up ℤ) a' b n' ⋯) (CategoryTheory.CategoryStruct.comp (CochainComplex.shiftFunctorObjXIso (K.total (ComplexShape.up ℤ)) x n n' hn').inv h✝))

theorem HomologicalComplex₂.ι_totalShift₁Iso_inv_f {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] (K : HomologicalComplex₂ C (ComplexShape.up ℤ) (ComplexShape.up ℤ)) (x : ℤ) [K.HasTotal (ComplexShape.up ℤ)] (a b n : ℤ) (h : a + b = n) (a' n' : ℤ) (ha' : a' + b = n') (hn' : n' = n + x) : CategoryTheory.CategoryStruct.comp (K.ιTotal (ComplexShape.up ℤ) a' b n' ha') (CategoryTheory.CategoryStruct.comp (CochainComplex.shiftFunctorObjXIso (K.total (ComplexShape.up ℤ)) x n n' hn').inv ((K.totalShift₁Iso x).inv.f n)) = CategoryTheory.CategoryStruct.comp (K.shiftFunctor₁XXIso a x a' ⋯ b).inv (((shiftFunctor₁ C x).obj K).ιTotal (ComplexShape.up ℤ) a b n h)

theorem HomologicalComplex₂.ι_totalShift₁Iso_inv_f_assoc {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] (K : HomologicalComplex₂ C (ComplexShape.up ℤ) (ComplexShape.up ℤ)) (x : ℤ) [K.HasTotal (ComplexShape.up ℤ)] (a b n : ℤ) (h : a + b = n) (a' n' : ℤ) (ha' : a' + b = n') (hn' : n' = n + x) {Z : C} (h✝ : (((shiftFunctor₁ C x).obj K).total (ComplexShape.up ℤ)).X n ⟶ Z) : CategoryTheory.CategoryStruct.comp (K.ιTotal (ComplexShape.up ℤ) a' b n' ha') (CategoryTheory.CategoryStruct.comp (CochainComplex.shiftFunctorObjXIso (K.total (ComplexShape.up ℤ)) x n n' hn').inv (CategoryTheory.CategoryStruct.comp ((K.totalShift₁Iso x).inv.f n) h✝)) = CategoryTheory.CategoryStruct.comp (K.shiftFunctor₁XXIso a x a' ⋯ b).inv (CategoryTheory.CategoryStruct.comp (((shiftFunctor₁ C x).obj K).ιTotal (ComplexShape.up ℤ) a b n h) h✝)

theorem HomologicalComplex₂.totalShift₁Iso_hom_naturality {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] {K L : HomologicalComplex₂ C (ComplexShape.up ℤ) (ComplexShape.up ℤ)} (f : K ⟶ L) (x : ℤ) [K.HasTotal (ComplexShape.up ℤ)] [L.HasTotal (ComplexShape.up ℤ)] : CategoryTheory.CategoryStruct.comp (total.map ((shiftFunctor₁ C x).map f) (ComplexShape.up ℤ)) (L.totalShift₁Iso x).hom = CategoryTheory.CategoryStruct.comp (K.totalShift₁Iso x).hom ((CategoryTheory.shiftFunctor (HomologicalComplex C (ComplexShape.up ℤ)) x).map (total.map f (ComplexShape.up ℤ)))

theorem HomologicalComplex₂.totalShift₁Iso_hom_naturality_assoc {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] {K L : HomologicalComplex₂ C (ComplexShape.up ℤ) (ComplexShape.up ℤ)} (f : K ⟶ L) (x : ℤ) [K.HasTotal (ComplexShape.up ℤ)] [L.HasTotal (ComplexShape.up ℤ)] {Z : HomologicalComplex C (ComplexShape.up ℤ)} (h : (CategoryTheory.shiftFunctor (HomologicalComplex C (ComplexShape.up ℤ)) x).obj (L.total (ComplexShape.up ℤ)) ⟶ Z) : CategoryTheory.CategoryStruct.comp (total.map ((shiftFunctor₁ C x).map f) (ComplexShape.up ℤ)) (CategoryTheory.CategoryStruct.comp (L.totalShift₁Iso x).hom h) = CategoryTheory.CategoryStruct.comp (K.totalShift₁Iso x).hom (CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctor (HomologicalComplex C (ComplexShape.up ℤ)) x).map (total.map f (ComplexShape.up ℤ))) h)

noncomputable def HomologicalComplex₂.totalShift₂XIso {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] (K : HomologicalComplex₂ C (ComplexShape.up ℤ) (ComplexShape.up ℤ)) (y : ℤ) [K.HasTotal (ComplexShape.up ℤ)] (n n' : ℤ) (h : n + y = n') : (((shiftFunctor₂ C y).obj K).total (ComplexShape.up ℤ)).X n ≅ (K.total (ComplexShape.up ℤ)).X n'

Auxiliary definition for totalShift₂Iso.

theorem HomologicalComplex₂.D₁_totalShift₂XIso_hom {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] (K : HomologicalComplex₂ C (ComplexShape.up ℤ) (ComplexShape.up ℤ)) (y : ℤ) [K.HasTotal (ComplexShape.up ℤ)] (n₀ n₁ n₀' n₁' : ℤ) (h₀ : n₀ + y = n₀') (h₁ : n₁ + y = n₁') : CategoryTheory.CategoryStruct.comp (((shiftFunctor₂ C y).obj K).D₁ (ComplexShape.up ℤ) n₀ n₁) (K.totalShift₂XIso y n₁ n₁' h₁).hom = y.negOnePow • CategoryTheory.CategoryStruct.comp (K.totalShift₂XIso y n₀ n₀' h₀).hom (K.D₁ (ComplexShape.up ℤ) n₀' n₁')

theorem HomologicalComplex₂.D₁_totalShift₂XIso_hom_assoc {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] (K : HomologicalComplex₂ C (ComplexShape.up ℤ) (ComplexShape.up ℤ)) (y : ℤ) [K.HasTotal (ComplexShape.up ℤ)] (n₀ n₁ n₀' n₁' : ℤ) (h₀ : n₀ + y = n₀') (h₁ : n₁ + y = n₁') {Z : C} (h : (K.total (ComplexShape.up ℤ)).X n₁' ⟶ Z) : CategoryTheory.CategoryStruct.comp (((shiftFunctor₂ C y).obj K).D₁ (ComplexShape.up ℤ) n₀ n₁) (CategoryTheory.CategoryStruct.comp (K.totalShift₂XIso y n₁ n₁' h₁).hom h) = CategoryTheory.CategoryStruct.comp (y.negOnePow • CategoryTheory.CategoryStruct.comp (K.totalShift₂XIso y n₀ n₀' h₀).hom (K.D₁ (ComplexShape.up ℤ) n₀' n₁')) h

theorem HomologicalComplex₂.D₂_totalShift₂XIso_hom {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] (K : HomologicalComplex₂ C (ComplexShape.up ℤ) (ComplexShape.up ℤ)) (y : ℤ) [K.HasTotal (ComplexShape.up ℤ)] (n₀ n₁ n₀' n₁' : ℤ) (h₀ : n₀ + y = n₀') (h₁ : n₁ + y = n₁') : CategoryTheory.CategoryStruct.comp (((shiftFunctor₂ C y).obj K).D₂ (ComplexShape.up ℤ) n₀ n₁) (K.totalShift₂XIso y n₁ n₁' h₁).hom = y.negOnePow • CategoryTheory.CategoryStruct.comp (K.totalShift₂XIso y n₀ n₀' h₀).hom (K.D₂ (ComplexShape.up ℤ) n₀' n₁')

theorem HomologicalComplex₂.D₂_totalShift₂XIso_hom_assoc {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] (K : HomologicalComplex₂ C (ComplexShape.up ℤ) (ComplexShape.up ℤ)) (y : ℤ) [K.HasTotal (ComplexShape.up ℤ)] (n₀ n₁ n₀' n₁' : ℤ) (h₀ : n₀ + y = n₀') (h₁ : n₁ + y = n₁') {Z : C} (h : (K.total (ComplexShape.up ℤ)).X n₁' ⟶ Z) : CategoryTheory.CategoryStruct.comp (((shiftFunctor₂ C y).obj K).D₂ (ComplexShape.up ℤ) n₀ n₁) (CategoryTheory.CategoryStruct.comp (K.totalShift₂XIso y n₁ n₁' h₁).hom h) = CategoryTheory.CategoryStruct.comp (y.negOnePow • CategoryTheory.CategoryStruct.comp (K.totalShift₂XIso y n₀ n₀' h₀).hom (K.D₂ (ComplexShape.up ℤ) n₀' n₁')) h

noncomputable def HomologicalComplex₂.totalShift₂Iso {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] (K : HomologicalComplex₂ C (ComplexShape.up ℤ) (ComplexShape.up ℤ)) (y : ℤ) [K.HasTotal (ComplexShape.up ℤ)] : ((shiftFunctor₂ C y).obj K).total (ComplexShape.up ℤ) ≅ (CategoryTheory.shiftFunctor (HomologicalComplex C (ComplexShape.up ℤ)) y).obj (K.total (ComplexShape.up ℤ))

The isomorphism ((shiftFunctor₂ C y).obj K).total (up ℤ) ≅ (K.total (up ℤ))⟦y⟧ expressing the compatibility of the total complex with the shift on the second indices. This isomorphism involves signs: on the summand in degree (p, q) of K, it is given by the multiplication by (p * y).negOnePow.

theorem HomologicalComplex₂.ι_totalShift₂Iso_hom_f {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] (K : HomologicalComplex₂ C (ComplexShape.up ℤ) (ComplexShape.up ℤ)) (y : ℤ) [K.HasTotal (ComplexShape.up ℤ)] (a b n : ℤ) (h : a + b = n) (b' : ℤ) (hb' : b' = b + y) (n' : ℤ) (hn' : n' = n + y) : CategoryTheory.CategoryStruct.comp (((shiftFunctor₂ C y).obj K).ιTotal (ComplexShape.up ℤ) a b n h) ((K.totalShift₂Iso y).hom.f n) = (a * y).negOnePow • CategoryTheory.CategoryStruct.comp (K.shiftFunctor₂XXIso a b y b' hb').hom (CategoryTheory.CategoryStruct.comp (K.ιTotal (ComplexShape.up ℤ) a b' n' ⋯) (CochainComplex.shiftFunctorObjXIso (K.total (ComplexShape.up ℤ)) y n n' hn').inv)

theorem HomologicalComplex₂.ι_totalShift₂Iso_hom_f_assoc {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] (K : HomologicalComplex₂ C (ComplexShape.up ℤ) (ComplexShape.up ℤ)) (y : ℤ) [K.HasTotal (ComplexShape.up ℤ)] (a b n : ℤ) (h : a + b = n) (b' : ℤ) (hb' : b' = b + y) (n' : ℤ) (hn' : n' = n + y) {Z : C} (h✝ : ((CategoryTheory.shiftFunctor (HomologicalComplex C (ComplexShape.up ℤ)) y).obj (K.total (ComplexShape.up ℤ))).X n ⟶ Z) : CategoryTheory.CategoryStruct.comp (((shiftFunctor₂ C y).obj K).ιTotal (ComplexShape.up ℤ) a b n h) (CategoryTheory.CategoryStruct.comp ((K.totalShift₂Iso y).hom.f n) h✝) = CategoryTheory.CategoryStruct.comp ((a * y).negOnePow • CategoryTheory.CategoryStruct.comp (K.shiftFunctor₂XXIso a b y b' hb').hom (CategoryTheory.CategoryStruct.comp (K.ιTotal (ComplexShape.up ℤ) a b' n' ⋯) (CochainComplex.shiftFunctorObjXIso (K.total (ComplexShape.up ℤ)) y n n' hn').inv)) h✝

theorem HomologicalComplex₂.ι_totalShift₂Iso_inv_f {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] (K : HomologicalComplex₂ C (ComplexShape.up ℤ) (ComplexShape.up ℤ)) (y : ℤ) [K.HasTotal (ComplexShape.up ℤ)] (a b n : ℤ) (h : a + b = n) (b' n' : ℤ) (hb' : a + b' = n') (hn' : n' = n + y) : CategoryTheory.CategoryStruct.comp (K.ιTotal (ComplexShape.up ℤ) a b' n' hb') (CategoryTheory.CategoryStruct.comp (CochainComplex.shiftFunctorObjXIso (K.total (ComplexShape.up ℤ)) y n n' hn').inv ((K.totalShift₂Iso y).inv.f n)) = (a * y).negOnePow • CategoryTheory.CategoryStruct.comp (K.shiftFunctor₂XXIso a b y b' ⋯).inv (((shiftFunctor₂ C y).obj K).ιTotal (ComplexShape.up ℤ) a b n h)

theorem HomologicalComplex₂.ι_totalShift₂Iso_inv_f_assoc {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] (K : HomologicalComplex₂ C (ComplexShape.up ℤ) (ComplexShape.up ℤ)) (y : ℤ) [K.HasTotal (ComplexShape.up ℤ)] (a b n : ℤ) (h : a + b = n) (b' n' : ℤ) (hb' : a + b' = n') (hn' : n' = n + y) {Z : C} (h✝ : (((shiftFunctor₂ C y).obj K).total (ComplexShape.up ℤ)).X n ⟶ Z) : CategoryTheory.CategoryStruct.comp (K.ιTotal (ComplexShape.up ℤ) a b' n' hb') (CategoryTheory.CategoryStruct.comp (CochainComplex.shiftFunctorObjXIso (K.total (ComplexShape.up ℤ)) y n n' hn').inv (CategoryTheory.CategoryStruct.comp ((K.totalShift₂Iso y).inv.f n) h✝)) = CategoryTheory.CategoryStruct.comp ((a * y).negOnePow • CategoryTheory.CategoryStruct.comp (K.shiftFunctor₂XXIso a b y b' ⋯).inv (((shiftFunctor₂ C y).obj K).ιTotal (ComplexShape.up ℤ) a b n h)) h✝

theorem HomologicalComplex₂.totalShift₂Iso_hom_naturality {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] {K L : HomologicalComplex₂ C (ComplexShape.up ℤ) (ComplexShape.up ℤ)} (f : K ⟶ L) (y : ℤ) [K.HasTotal (ComplexShape.up ℤ)] [L.HasTotal (ComplexShape.up ℤ)] : CategoryTheory.CategoryStruct.comp (total.map ((shiftFunctor₂ C y).map f) (ComplexShape.up ℤ)) (L.totalShift₂Iso y).hom = CategoryTheory.CategoryStruct.comp (K.totalShift₂Iso y).hom ((CategoryTheory.shiftFunctor (HomologicalComplex C (ComplexShape.up ℤ)) y).map (total.map f (ComplexShape.up ℤ)))

theorem HomologicalComplex₂.totalShift₂Iso_hom_naturality_assoc {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] {K L : HomologicalComplex₂ C (ComplexShape.up ℤ) (ComplexShape.up ℤ)} (f : K ⟶ L) (y : ℤ) [K.HasTotal (ComplexShape.up ℤ)] [L.HasTotal (ComplexShape.up ℤ)] {Z : HomologicalComplex C (ComplexShape.up ℤ)} (h : (CategoryTheory.shiftFunctor (HomologicalComplex C (ComplexShape.up ℤ)) y).obj (L.total (ComplexShape.up ℤ)) ⟶ Z) : CategoryTheory.CategoryStruct.comp (total.map ((shiftFunctor₂ C y).map f) (ComplexShape.up ℤ)) (CategoryTheory.CategoryStruct.comp (L.totalShift₂Iso y).hom h) = CategoryTheory.CategoryStruct.comp (K.totalShift₂Iso y).hom (CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctor (HomologicalComplex C (ComplexShape.up ℤ)) y).map (total.map f (ComplexShape.up ℤ))) h)

def HomologicalComplex₂.shiftFunctor₁₂CommIso (C : Type u_1) [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] (x y : ℤ) : (shiftFunctor₂ C y).comp (shiftFunctor₁ C x) ≅ (shiftFunctor₁ C x).comp (shiftFunctor₂ C y)

The shift functors shiftFunctor₁ C x and shiftFunctor₂ C y on bicomplexes with respect to both variables commute.

theorem HomologicalComplex₂.totalShift₁Iso_trans_totalShift₂Iso {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] (K : HomologicalComplex₂ C (ComplexShape.up ℤ) (ComplexShape.up ℤ)) (x y : ℤ) [K.HasTotal (ComplexShape.up ℤ)] : ((shiftFunctor₂ C y).obj K).totalShift₁Iso x ≪≫ (CategoryTheory.shiftFunctor (CochainComplex C ℤ) x).mapIso (K.totalShift₂Iso y) = (x * y).negOnePow • total.mapIso ((shiftFunctor₁₂CommIso C x y).app K) (ComplexShape.up ℤ) ≪≫ ((shiftFunctor₁ C x).obj K).totalShift₂Iso y ≪≫ (CategoryTheory.shiftFunctor (HomologicalComplex C (ComplexShape.up ℤ)) y).mapIso (K.totalShift₁Iso x) ≪≫ (CategoryTheory.shiftFunctorComm (CochainComplex C ℤ) x y).app (K.total (ComplexShape.up ℤ))

The compatibility isomorphisms of the total complex with the shifts in both variables "commute" only up to a sign (x * y).negOnePow.

theorem HomologicalComplex₂.totalShift₁Iso_hom_totalShift₂Iso_hom {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] (K : HomologicalComplex₂ C (ComplexShape.up ℤ) (ComplexShape.up ℤ)) (x y : ℤ) [K.HasTotal (ComplexShape.up ℤ)] : CategoryTheory.CategoryStruct.comp (((shiftFunctor₂ C y).obj K).totalShift₁Iso x).hom ((CategoryTheory.shiftFunctor (HomologicalComplex C (ComplexShape.up ℤ)) x).map (K.totalShift₂Iso y).hom) = (x * y).negOnePow • CategoryTheory.CategoryStruct.comp (total.map ((shiftFunctor₁₂CommIso C x y).hom.app K) (ComplexShape.up ℤ)) (CategoryTheory.CategoryStruct.comp (((shiftFunctor₁ C x).obj K).totalShift₂Iso y).hom (CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctor (HomologicalComplex C (ComplexShape.up ℤ)) y).map (K.totalShift₁Iso x).hom) ((CategoryTheory.shiftFunctorComm (CochainComplex C ℤ) x y).hom.app (K.total (ComplexShape.up ℤ)))))

The compatibility isomorphisms of the total complex with the shifts in both variables "commute" only up to a sign (x * y).negOnePow.

theorem HomologicalComplex₂.totalShift₁Iso_hom_totalShift₂Iso_hom_assoc {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] (K : HomologicalComplex₂ C (ComplexShape.up ℤ) (ComplexShape.up ℤ)) (x y : ℤ) [K.HasTotal (ComplexShape.up ℤ)] {Z : HomologicalComplex C (ComplexShape.up ℤ)} (h : (CategoryTheory.shiftFunctor (HomologicalComplex C (ComplexShape.up ℤ)) x).obj ((CategoryTheory.shiftFunctor (HomologicalComplex C (ComplexShape.up ℤ)) y).obj (K.total (ComplexShape.up ℤ))) ⟶ Z) : CategoryTheory.CategoryStruct.comp (((shiftFunctor₂ C y).obj K).totalShift₁Iso x).hom (CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctor (HomologicalComplex C (ComplexShape.up ℤ)) x).map (K.totalShift₂Iso y).hom) h) = CategoryTheory.CategoryStruct.comp ((x * y).negOnePow • CategoryTheory.CategoryStruct.comp (total.map ((shiftFunctor₁₂CommIso C x y).hom.app K) (ComplexShape.up ℤ)) (CategoryTheory.CategoryStruct.comp (((shiftFunctor₁ C x).obj K).totalShift₂Iso y).hom (CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctor (HomologicalComplex C (ComplexShape.up ℤ)) y).map (K.totalShift₁Iso x).hom) ((CategoryTheory.shiftFunctorComm (CochainComplex C ℤ) x y).hom.app (K.total (ComplexShape.up ℤ)))))) h

The compatibility isomorphisms of the total complex with the shifts in both variables "commute" only up to a sign (x * y).negOnePow.