# Documentation

Mathlib.Algebra.Homology.HomotopyCategory.Shift

# 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 ℤ.

@[simp]
theorem CochainComplex.shiftFunctor_obj_d (C : Type u) (n : ) (K : ) (i : ) (j : ) :
HomologicalComplex.d (().obj K) i j = n.negOnePow HomologicalComplex.d K (i + n) (j + n)
@[simp]
theorem CochainComplex.shiftFunctor_obj_X (C : Type u) (n : ) (K : ) (i : ) :
@[simp]
theorem CochainComplex.shiftFunctor_map_f (C : Type u) (n : ) :
∀ {X Y : } (φ : X Y) (i : ), HomologicalComplex.Hom.f (().map φ) i = HomologicalComplex.Hom.f φ (i + 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.

Instances For
def CochainComplex.shiftFunctorObjXIso {C : Type u} (K : ) (n : ) (i : ) (m : ) (hm : m = i + n) :

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

Instances For
@[simp]
theorem CochainComplex.shiftFunctorZero'_hom_app_f (C : Type u) (n : ) (h : n = 0) (X : ) (i : ) :
HomologicalComplex.Hom.f (().hom.app X) i = (HomologicalComplex.XIsoOfEq X (_ : i + n = i)).hom
@[simp]
theorem CochainComplex.shiftFunctorZero'_inv_app_f (C : Type u) (n : ) (h : n = 0) (X : ) (i : ) :
HomologicalComplex.Hom.f (().inv.app X) i = (HomologicalComplex.XIsoOfEq X (_ : i + n = i)).inv
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.

Instances For
@[simp]
theorem CochainComplex.shiftFunctorAdd'_inv_app_f (C : Type u) (n₁ : ) (n₂ : ) (n₁₂ : ) (h : n₁ + n₂ = n₁₂) (X : ) (i : ) :
HomologicalComplex.Hom.f ((CochainComplex.shiftFunctorAdd' C n₁ n₂ n₁₂ h).inv.app X) i = (HomologicalComplex.XIsoOfEq X (_ : i + n₁₂ = i + n₂ + n₁)).inv
@[simp]
theorem CochainComplex.shiftFunctorAdd'_hom_app_f (C : Type u) (n₁ : ) (n₂ : ) (n₁₂ : ) (h : n₁ + n₂ = n₁₂) (X : ) (i : ) :
HomologicalComplex.Hom.f ((CochainComplex.shiftFunctorAdd' C n₁ n₂ n₁₂ h).hom.app X) i = (HomologicalComplex.XIsoOfEq X (_ : i + n₁₂ = i + n₂ + n₁)).hom
def CochainComplex.shiftFunctorAdd' (C : Type u) (n₁ : ) (n₂ : ) (n₁₂ : ) (h : n₁ + n₂ = n₁₂) :

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

Instances For
@[simp]
theorem CochainComplex.shiftFunctor_map_f' {C : Type u} {K : } {L : } (φ : K L) (n : ) (p : ) :
@[simp]
theorem CochainComplex.shiftFunctor_obj_d' {C : Type u} (K : ) (n : ) (i : ) (j : ) :
HomologicalComplex.d (().obj K) i j = n.negOnePow HomologicalComplex.d K (i + { as := n }.as) (j + { as := n }.as)
theorem CochainComplex.shiftFunctorAdd_inv_app_f {C : Type u} (K : ) (a : ) (b : ) (n : ) :
HomologicalComplex.Hom.f (().inv.app K) n = (HomologicalComplex.XIsoOfEq K (_ : n + { as := b }.as + { as := a }.as = n + { as := a + b }.as)).hom
theorem CochainComplex.shiftFunctorAdd_hom_app_f {C : Type u} (K : ) (a : ) (b : ) (n : ) :
HomologicalComplex.Hom.f (().hom.app K) n = (HomologicalComplex.XIsoOfEq K (_ : n + { as := a + b }.as = n + { as := b }.as + { as := a }.as)).hom
theorem CochainComplex.shiftFunctorAdd'_inv_app_f' {C : Type u} (K : ) (a : ) (b : ) (ab : ) (h : a + b = ab) (n : ) :
HomologicalComplex.Hom.f (().inv.app K) n = (HomologicalComplex.XIsoOfEq K (_ : n + { as := b }.as + { as := a }.as = n + { as := ab }.as)).hom
theorem CochainComplex.shiftFunctorAdd'_hom_app_f' {C : Type u} (K : ) (a : ) (b : ) (ab : ) (h : a + b = ab) (n : ) :
HomologicalComplex.Hom.f (().hom.app K) n = (HomologicalComplex.XIsoOfEq K (_ : n + { as := ab }.as = n + { as := b }.as + { as := a }.as)).hom
theorem CochainComplex.shiftFunctorZero_inv_app_f {C : Type u} (K : ) (n : ) :
HomologicalComplex.Hom.f (().inv.app K) n = (HomologicalComplex.XIsoOfEq K (_ : n = n + { as := 0 }.as)).hom
theorem CochainComplex.shiftFunctorZero_hom_app_f {C : Type u} (K : ) (n : ) :
HomologicalComplex.Hom.f (().hom.app K) n = (HomologicalComplex.XIsoOfEq K (_ : n + { as := 0 }.as = 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.shiftFunctorAdd_eq (C : Type u) (a : ) (b : ) :
= CochainComplex.shiftFunctorAdd' C a b (a + b) (_ : a + b = a + b)
theorem CochainComplex.shiftFunctorComm_hom_app_f {C : Type u} (K : ) (a : ) (b : ) (p : ) :
HomologicalComplex.Hom.f (().hom.app K) p = (HomologicalComplex.XIsoOfEq K (_ : p + b + a = p + a + b)).hom
@[simp]
@[simp]

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

Instances For
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⟧'.

Instances For
noncomputable instance HomotopyCategory.hasShift (C : Type u) :
noncomputable instance HomotopyCategory.commShiftQuotient (C : Type u) :