# The shift on cochain complexes and on the homotopy category #

In this file, we show that for any preadditive category C, the categories CochainComplex C ℤ and HomotopyCategory C (ComplexShape.up ℤ) are equipped with a shift by ℤ.

We also show that if F : C ⥤ D is an additive functor, then the functors F.mapHomologicalComplex (ComplexShape.up ℤ) and F.mapHomotopyCategory (ComplexShape.up ℤ) commute with the shift by ℤ.

@[simp]
theorem CochainComplex.shiftFunctor_map_f (C : Type u) (n : ) :
∀ {X Y : } (φ : X Y) (i : ), (.map φ).f i = φ.f (i + n)
@[simp]
theorem CochainComplex.shiftFunctor_obj_X (C : Type u) (n : ) (K : ) (i : ) :
(.obj K).X i = K.X (i + n)
@[simp]
theorem CochainComplex.shiftFunctor_obj_d (C : Type u) (n : ) (K : ) (i : ) (j : ) :
(.obj K).d i j = n.negOnePow K.d (i + n) (j + n)

The shift functor by n : ℤ on CochainComplex C ℤ which sends a cochain complex K to the complex which is K.X (i + n) in degree i, and which multiplies the differentials by (-1)^n.

Equations
• One or more equations did not get rendered due to their size.
Instances For
instance CochainComplex.instAdditiveIntShiftFunctor (C : Type u) (n : ) :
Equations
• =
def CochainComplex.shiftFunctorObjXIso {C : Type u} (K : ) (n : ) (i : ) (m : ) (hm : m = i + n) :
(.obj K).X i K.X m

The canonical isomorphism ((shiftFunctor C n).obj K).X i ≅ K.X m when m = i + n.

Equations
• K.shiftFunctorObjXIso n i m hm =
Instances For
@[simp]
theorem CochainComplex.shiftFunctorZero'_inv_app_f (C : Type u) (n : ) (h : n = 0) (X : ) (i : ) :
(.inv.app X).f i = .inv
@[simp]
theorem CochainComplex.shiftFunctorZero'_hom_app_f (C : Type u) (n : ) (h : n = 0) (X : ) (i : ) :
(.hom.app X).f i = .hom
def CochainComplex.shiftFunctorZero' (C : Type u) (n : ) (h : n = 0) :

The shift functor by n on CochainComplex C ℤ identifies to the identity functor when n = 0.

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem CochainComplex.shiftFunctorAdd'_hom_app_f (C : Type u) (n₁ : ) (n₂ : ) (n₁₂ : ) (h : n₁ + n₂ = n₁₂) (X : ) (i : ) :
((CochainComplex.shiftFunctorAdd' C n₁ n₂ n₁₂ h).hom.app X).f i = .hom
@[simp]
theorem CochainComplex.shiftFunctorAdd'_inv_app_f (C : Type u) (n₁ : ) (n₂ : ) (n₁₂ : ) (h : n₁ + n₂ = n₁₂) (X : ) (i : ) :
((CochainComplex.shiftFunctorAdd' C n₁ n₂ n₁₂ h).inv.app X).f i = .inv
def CochainComplex.shiftFunctorAdd' (C : Type u) (n₁ : ) (n₂ : ) (n₁₂ : ) (h : n₁ + n₂ = n₁₂) :
.comp

The compatibility of the shift functors on CochainComplex C ℤ with respect to the addition of integers.

Equations
• One or more equations did not get rendered due to their size.
Instances For
Equations
• One or more equations did not get rendered due to their size.
Equations
• =
@[simp]
theorem CochainComplex.shiftFunctor_obj_X' {C : Type u} (K : ) (n : ) (p : ) :
(.obj K).X p = K.X (p + n)
@[simp]
theorem CochainComplex.shiftFunctor_map_f' {C : Type u} {K : } {L : } (φ : K L) (n : ) (p : ) :
(.map φ).f p = φ.f (p + n)
@[simp]
theorem CochainComplex.shiftFunctor_obj_d' {C : Type u} (K : ) (n : ) (i : ) (j : ) :
(.obj K).d i j = n.negOnePow K.d (i + { as := n }.as) (j + { as := n }.as)
theorem CochainComplex.shiftFunctorAdd_inv_app_f {C : Type u} (K : ) (a : ) (b : ) (n : ) :
(.inv.app K).f n = .hom
theorem CochainComplex.shiftFunctorAdd_hom_app_f {C : Type u} (K : ) (a : ) (b : ) (n : ) :
(.hom.app K).f n = .hom
theorem CochainComplex.shiftFunctorAdd'_inv_app_f' {C : Type u} (K : ) (a : ) (b : ) (ab : ) (h : a + b = ab) (n : ) :
((CategoryTheory.shiftFunctorAdd' a b ab h).inv.app K).f n = .hom
theorem CochainComplex.shiftFunctorAdd'_hom_app_f' {C : Type u} (K : ) (a : ) (b : ) (ab : ) (h : a + b = ab) (n : ) :
((CategoryTheory.shiftFunctorAdd' a b ab h).hom.app K).f n = .hom
theorem CochainComplex.shiftFunctorZero_inv_app_f {C : Type u} (K : ) (n : ) :
(.inv.app K).f n = .hom
theorem CochainComplex.shiftFunctorZero_hom_app_f {C : Type u} (K : ) (n : ) :
(.hom.app K).f n = .hom
theorem CochainComplex.XIsoOfEq_shift {C : Type u} (K : ) (n : ) {p : } {q : } (hpq : p = q) :
theorem CochainComplex.shiftFunctorAdd'_eq (C : Type u) (a : ) (b : ) (c : ) (h : a + b = c) :
=
theorem CochainComplex.shiftFunctorComm_hom_app_f {C : Type u} (K : ) (a : ) (b : ) (p : ) :
(.hom.app K).f p = .hom
@[simp]
theorem CochainComplex.shiftEval_inv_app (C : Type u) (n : ) (i : ) (i' : ) (hi : n + i = i') (X : ) :
(CochainComplex.shiftEval C n i i' hi).inv.app X = .inv
@[simp]
theorem CochainComplex.shiftEval_hom_app (C : Type u) (n : ) (i : ) (i' : ) (hi : n + i = i') (X : ) :
(CochainComplex.shiftEval C n i i' hi).hom.app X = .hom
def CochainComplex.shiftEval (C : Type u) (n : ) (i : ) (i' : ) (hi : n + i = i') :
.comp

Shifting cochain complexes by n and evaluating in a degree i identifies to the evaluation in degree i' when n + i = i'.

Equations
Instances For
@[simp]
theorem CategoryTheory.Functor.mapCochainComplexShiftIso_inv_app_f {C : Type u} {D : Type u'} [] (F : ) [F.Additive] (n : ) (X : ) (i : ) :
((F.mapCochainComplexShiftIso n).inv.app X).f i = CategoryTheory.CategoryStruct.id (F.obj (X.X (i + n)))
@[simp]
theorem CategoryTheory.Functor.mapCochainComplexShiftIso_hom_app_f {C : Type u} {D : Type u'} [] (F : ) [F.Additive] (n : ) (X : ) (i : ) :
((F.mapCochainComplexShiftIso n).hom.app X).f i = CategoryTheory.CategoryStruct.id (F.obj (X.X (i + n)))
def CategoryTheory.Functor.mapCochainComplexShiftIso {C : Type u} {D : Type u'} [] (F : ) [F.Additive] (n : ) :
.comp (F.mapHomologicalComplex ) (F.mapHomologicalComplex ).comp

The commutation with the shift isomorphism for the functor on cochain complexes induced by an additive functor between preadditive categories.

Equations
• One or more equations did not get rendered due to their size.
Instances For
instance CategoryTheory.Functor.commShiftMapCochainComplex {C : Type u} {D : Type u'} [] (F : ) [F.Additive] :
(F.mapHomologicalComplex ).CommShift
Equations
• F.commShiftMapCochainComplex = { iso := F.mapCochainComplexShiftIso, zero := , add := }
theorem CategoryTheory.Functor.mapHomologicalComplex_commShiftIso_eq {C : Type u} {D : Type u'} [] (F : ) [F.Additive] (n : ) :
(F.mapHomologicalComplex ).commShiftIso n = F.mapCochainComplexShiftIso n
@[simp]
theorem CategoryTheory.Functor.mapHomologicalComplex_commShiftIso_hom_app_f {C : Type u} {D : Type u'} [] (F : ) [F.Additive] (K : ) (n : ) (i : ) :
(((F.mapHomologicalComplex ).commShiftIso n).hom.app K).f i = CategoryTheory.CategoryStruct.id (((.comp (F.mapHomologicalComplex )).obj K).X i)
@[simp]
theorem CategoryTheory.Functor.mapHomologicalComplex_commShiftIso_inv_app_f {C : Type u} {D : Type u'} [] (F : ) [F.Additive] (K : ) (n : ) (i : ) :
(((F.mapHomologicalComplex ).commShiftIso n).inv.app K).f i = CategoryTheory.CategoryStruct.id ((((F.mapHomologicalComplex ).comp ).obj K).X i)
def Homotopy.shift {C : Type u} {K : } {L : } {φ₁ : K L} {φ₂ : K L} (h : Homotopy φ₁ φ₂) (n : ) :
Homotopy (.map φ₁) (.map φ₂)

If h : Homotopy φ₁ φ₂ and n : ℤ, this is the induced homotopy between φ₁⟦n⟧' and φ₂⟦n⟧'.

Equations
• h.shift n = { hom := fun (i j : ) => n.negOnePow h.hom (i + { as := n }.as) (j + { as := n }.as), zero := , comm := }
Instances For
Equations
• =
noncomputable instance HomotopyCategory.hasShift (C : Type u) :
Equations
• = id inferInstance
noncomputable instance HomotopyCategory.commShiftQuotient (C : Type u) :
.CommShift
Equations
instance HomotopyCategory.instAdditiveIntUpShiftFunctor (C : Type u) (n : ) :