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

TODO

• show that the two sorts of shift functors on bicomplexes "commute", but that signs appear when we compare the compositions of the two compatibilities with the total complex functor.
• deduce compatiblities with shifts on both variables of the action of a bifunctor on cochain complexes

@[reducible, inline]

abbrev HomologicalComplex₂.shiftFunctor₁ (C : Type u_1) [CategoryTheory.Category.{u_2, 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).

Equations

• HomologicalComplex₂.shiftFunctor₁ C x = CategoryTheory.shiftFunctor (HomologicalComplex₂ C (ComplexShape.up ℤ) (ComplexShape.up ℤ)) x

@[reducible, inline]

abbrev HomologicalComplex₂.shiftFunctor₂ (C : Type u_1) [CategoryTheory.Category.{u_2, 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).

Equations

• HomologicalComplex₂.shiftFunctor₂ C y = (CategoryTheory.shiftFunctor (HomologicalComplex C (ComplexShape.up ℤ)) y).mapHomologicalComplex (ComplexShape.up ℤ)

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

Auxiliary definition for totalShift₁Iso.

Equations

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

theorem HomologicalComplex₂.D₁_totalShift₁XIso_hom_assoc {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] (K : HomologicalComplex₂ C (ComplexShape.up ℤ) (ComplexShape.up ℤ)) (x : ℤ) [K.HasTotal (ComplexShape.up ℤ)] [((HomologicalComplex₂.shiftFunctor₁ C x).obj 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 (((HomologicalComplex₂.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.{u_2, u_1} C] [CategoryTheory.Preadditive C] (K : HomologicalComplex₂ C (ComplexShape.up ℤ) (ComplexShape.up ℤ)) (x : ℤ) [K.HasTotal (ComplexShape.up ℤ)] [((HomologicalComplex₂.shiftFunctor₁ C x).obj K).HasTotal (ComplexShape.up ℤ)] (n₀ : ℤ) (n₁ : ℤ) (n₀' : ℤ) (n₁' : ℤ) (h₀ : n₀ + x = n₀') (h₁ : n₁ + x = n₁') : CategoryTheory.CategoryStruct.comp (((HomologicalComplex₂.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.{u_2, u_1} C] [CategoryTheory.Preadditive C] (K : HomologicalComplex₂ C (ComplexShape.up ℤ) (ComplexShape.up ℤ)) (x : ℤ) [K.HasTotal (ComplexShape.up ℤ)] [((HomologicalComplex₂.shiftFunctor₁ C x).obj 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 (((HomologicalComplex₂.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.{u_2, u_1} C] [CategoryTheory.Preadditive C] (K : HomologicalComplex₂ C (ComplexShape.up ℤ) (ComplexShape.up ℤ)) (x : ℤ) [K.HasTotal (ComplexShape.up ℤ)] [((HomologicalComplex₂.shiftFunctor₁ C x).obj K).HasTotal (ComplexShape.up ℤ)] (n₀ : ℤ) (n₁ : ℤ) (n₀' : ℤ) (n₁' : ℤ) (h₀ : n₀ + x = n₀') (h₁ : n₁ + x = n₁') : CategoryTheory.CategoryStruct.comp (((HomologicalComplex₂.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₁')

noncomputable def HomologicalComplex₂.totalShift₁Iso {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] (K : HomologicalComplex₂ C (ComplexShape.up ℤ) (ComplexShape.up ℤ)) (x : ℤ) [K.HasTotal (ComplexShape.up ℤ)] [((HomologicalComplex₂.shiftFunctor₁ C x).obj K).HasTotal (ComplexShape.up ℤ)] : ((HomologicalComplex₂.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.

Equations

• K.totalShift₁Iso x = HomologicalComplex.Hom.isoOfComponents (fun (n : ℤ) => K.totalShift₁XIso x n (n + x) ⋯) ⋯

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

Auxiliary definition for totalShift₂Iso.

Equations

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

theorem HomologicalComplex₂.D₁_totalShift₂XIso_hom_assoc {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] (K : HomologicalComplex₂ C (ComplexShape.up ℤ) (ComplexShape.up ℤ)) (y : ℤ) [K.HasTotal (ComplexShape.up ℤ)] [((HomologicalComplex₂.shiftFunctor₂ C y).obj 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 (((HomologicalComplex₂.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.{u_2, u_1} C] [CategoryTheory.Preadditive C] (K : HomologicalComplex₂ C (ComplexShape.up ℤ) (ComplexShape.up ℤ)) (y : ℤ) [K.HasTotal (ComplexShape.up ℤ)] [((HomologicalComplex₂.shiftFunctor₂ C y).obj K).HasTotal (ComplexShape.up ℤ)] (n₀ : ℤ) (n₁ : ℤ) (n₀' : ℤ) (n₁' : ℤ) (h₀ : n₀ + y = n₀') (h₁ : n₁ + y = n₁') : CategoryTheory.CategoryStruct.comp (((HomologicalComplex₂.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.{u_2, u_1} C] [CategoryTheory.Preadditive C] (K : HomologicalComplex₂ C (ComplexShape.up ℤ) (ComplexShape.up ℤ)) (y : ℤ) [K.HasTotal (ComplexShape.up ℤ)] [((HomologicalComplex₂.shiftFunctor₂ C y).obj 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 (((HomologicalComplex₂.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.{u_2, u_1} C] [CategoryTheory.Preadditive C] (K : HomologicalComplex₂ C (ComplexShape.up ℤ) (ComplexShape.up ℤ)) (y : ℤ) [K.HasTotal (ComplexShape.up ℤ)] [((HomologicalComplex₂.shiftFunctor₂ C y).obj K).HasTotal (ComplexShape.up ℤ)] (n₀ : ℤ) (n₁ : ℤ) (n₀' : ℤ) (n₁' : ℤ) (h₀ : n₀ + y = n₀') (h₁ : n₁ + y = n₁') : CategoryTheory.CategoryStruct.comp (((HomologicalComplex₂.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₁')

noncomputable def HomologicalComplex₂.totalShift₂Iso {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] (K : HomologicalComplex₂ C (ComplexShape.up ℤ) (ComplexShape.up ℤ)) (y : ℤ) [K.HasTotal (ComplexShape.up ℤ)] [((HomologicalComplex₂.shiftFunctor₂ C y).obj K).HasTotal (ComplexShape.up ℤ)] : ((HomologicalComplex₂.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: in the summand in degree (p, q) of K, it is given by the multiplication by (p * y).negOnePow.

Equations

• K.totalShift₂Iso y = HomologicalComplex.Hom.isoOfComponents (fun (n : ℤ) => K.totalShift₂XIso y n (n + y) ⋯) ⋯