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) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] (n : ℤ) (K : CochainComplex C ℤ) (i : ℤ) (j : ℤ) : ((CochainComplex.shiftFunctor C n).toPrefunctor.obj K).d i j = n.negOnePow • K.d (i + n) (j + n)

@[simp]

theorem CochainComplex.shiftFunctor_obj_X (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] (n : ℤ) (K : CochainComplex C ℤ) (i : ℤ) : ((CochainComplex.shiftFunctor C n).toPrefunctor.obj K).X i = K.X (i + n)

@[simp]

theorem CochainComplex.shiftFunctor_map_f (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] (n : ℤ) : ∀ {X Y : CochainComplex C ℤ} (φ : X ⟶ Y) (i : ℤ), ((CochainComplex.shiftFunctor C n).toPrefunctor.map φ).f i = φ.f (i + n)

def CochainComplex.shiftFunctor (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] (n : ℤ) : CategoryTheory.Functor (CochainComplex C ℤ) (CochainComplex C ℤ)

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.

instance CochainComplex.instAdditiveCochainComplexPreadditiveHasZeroMorphismsIntToAddRightCancelSemigroupToAddRightCancelMonoidToAddCancelMonoidInstAddGroupIntToOneInstSemiringIntInstCategoryHomologicalComplexUpInstPreadditiveHomologicalComplexPreadditiveHasZeroMorphismsInstCategoryHomologicalComplexShiftFunctor (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] (n : ℤ) : CategoryTheory.Functor.Additive (CochainComplex.shiftFunctor C n)

Equations

• (_ : CategoryTheory.Functor.Additive (CochainComplex.shiftFunctor C n)) = (_ : CategoryTheory.Functor.Additive (CochainComplex.shiftFunctor C n))

def CochainComplex.shiftFunctorObjXIso {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] (K : CochainComplex C ℤ) (n : ℤ) (i : ℤ) (m : ℤ) (hm : m = i + n) : ((CochainComplex.shiftFunctor C n).toPrefunctor.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

• CochainComplex.shiftFunctorObjXIso K n i m hm = HomologicalComplex.XIsoOfEq K (_ : i + n = m)

@[simp]

theorem CochainComplex.shiftFunctorZero'_hom_app_f (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] (n : ℤ) (h : n = 0) (X : CochainComplex C ℤ) (i : ℤ) : ((CochainComplex.shiftFunctorZero' C n h).hom.app X).f i = (HomologicalComplex.XIsoOfEq X (_ : i + n = i)).hom

@[simp]

theorem CochainComplex.shiftFunctorZero'_inv_app_f (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] (n : ℤ) (h : n = 0) (X : CochainComplex C ℤ) (i : ℤ) : ((CochainComplex.shiftFunctorZero' C n h).inv.app X).f i = (HomologicalComplex.XIsoOfEq X (_ : i + n = i)).inv

def CochainComplex.shiftFunctorZero' (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] (n : ℤ) (h : n = 0) : CochainComplex.shiftFunctor C n ≅ CategoryTheory.Functor.id (CochainComplex C ℤ)

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.

@[simp]

theorem CochainComplex.shiftFunctorAdd'_inv_app_f (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] (n₁ : ℤ) (n₂ : ℤ) (n₁₂ : ℤ) (h : n₁ + n₂ = n₁₂) (X : CochainComplex C ℤ) (i : ℤ) : ((CochainComplex.shiftFunctorAdd' C n₁ n₂ n₁₂ h).inv.app X).f i = (HomologicalComplex.XIsoOfEq X (_ : i + n₁₂ = i + n₂ + n₁)).inv

@[simp]

theorem CochainComplex.shiftFunctorAdd'_hom_app_f (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] (n₁ : ℤ) (n₂ : ℤ) (n₁₂ : ℤ) (h : n₁ + n₂ = n₁₂) (X : CochainComplex C ℤ) (i : ℤ) : ((CochainComplex.shiftFunctorAdd' C n₁ n₂ n₁₂ h).hom.app X).f i = (HomologicalComplex.XIsoOfEq X (_ : i + n₁₂ = i + n₂ + n₁)).hom

def CochainComplex.shiftFunctorAdd' (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] (n₁ : ℤ) (n₂ : ℤ) (n₁₂ : ℤ) (h : n₁ + n₂ = n₁₂) : CochainComplex.shiftFunctor C n₁₂ ≅ CategoryTheory.Functor.comp (CochainComplex.shiftFunctor C n₁) (CochainComplex.shiftFunctor C n₂)

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.

instance CochainComplex.instHasShiftCochainComplexPreadditiveHasZeroMorphismsIntToAddRightCancelSemigroupToAddRightCancelMonoidToAddCancelMonoidInstAddGroupIntToOneInstSemiringIntInstCategoryHomologicalComplexUpInstAddMonoidInt (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] : CategoryTheory.HasShift (CochainComplex C ℤ) ℤ

Equations

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

instance CochainComplex.instAdditiveHomologicalComplexIntPreadditiveHasZeroMorphismsUpToAddRightCancelSemigroupToAddRightCancelMonoidToAddCancelMonoidInstAddGroupIntToOneInstSemiringIntInstCategoryHomologicalComplexInstPreadditiveHomologicalComplexPreadditiveHasZeroMorphismsInstCategoryHomologicalComplexShiftFunctorInstAddMonoidIntInstHasShiftCochainComplexPreadditiveHasZeroMorphismsIntToAddRightCancelSemigroupToAddRightCancelMonoidToAddCancelMonoidInstAddGroupIntToOneInstSemiringIntInstCategoryHomologicalComplexUpInstAddMonoidInt (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] (n : ℤ) : CategoryTheory.Functor.Additive (CategoryTheory.shiftFunctor (HomologicalComplex C (ComplexShape.up ℤ)) n)

Equations

• (_ : CategoryTheory.Functor.Additive (CategoryTheory.shiftFunctor (HomologicalComplex C (ComplexShape.up ℤ)) n)) = (_ : CategoryTheory.Functor.Additive (CochainComplex.shiftFunctor C n))

@[simp]

theorem CochainComplex.shiftFunctor_obj_X' {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] (K : CochainComplex C ℤ) (n : ℤ) (p : ℤ) : ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) n).toPrefunctor.obj K).X p = K.X (p + n)

@[simp]

theorem CochainComplex.shiftFunctor_map_f' {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {K : CochainComplex C ℤ} {L : CochainComplex C ℤ} (φ : K ⟶ L) (n : ℤ) (p : ℤ) : ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) n).toPrefunctor.map φ).f p = φ.f (p + n)

@[simp]

theorem CochainComplex.shiftFunctor_obj_d' {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] (K : CochainComplex C ℤ) (n : ℤ) (i : ℤ) (j : ℤ) : ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) n).toPrefunctor.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} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] (K : CochainComplex C ℤ) (a : ℤ) (b : ℤ) (n : ℤ) : ((CategoryTheory.shiftFunctorAdd (CochainComplex C ℤ) a b).inv.app K).f 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} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] (K : CochainComplex C ℤ) (a : ℤ) (b : ℤ) (n : ℤ) : ((CategoryTheory.shiftFunctorAdd (CochainComplex C ℤ) a b).hom.app K).f 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} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] (K : CochainComplex C ℤ) (a : ℤ) (b : ℤ) (ab : ℤ) (h : a + b = ab) (n : ℤ) : ((CategoryTheory.shiftFunctorAdd' (CochainComplex C ℤ) a b ab h).inv.app K).f 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} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] (K : CochainComplex C ℤ) (a : ℤ) (b : ℤ) (ab : ℤ) (h : a + b = ab) (n : ℤ) : ((CategoryTheory.shiftFunctorAdd' (CochainComplex C ℤ) a b ab h).hom.app K).f 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} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] (K : CochainComplex C ℤ) (n : ℤ) : ((CategoryTheory.shiftFunctorZero (CochainComplex C ℤ) ℤ).inv.app K).f n = (HomologicalComplex.XIsoOfEq K (_ : n = n + { as := 0 }.as)).hom

theorem CochainComplex.shiftFunctorZero_hom_app_f {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] (K : CochainComplex C ℤ) (n : ℤ) : ((CategoryTheory.shiftFunctorZero (CochainComplex C ℤ) ℤ).hom.app K).f n = (HomologicalComplex.XIsoOfEq K (_ : n + { as := 0 }.as = n)).hom

theorem CochainComplex.XIsoOfEq_shift {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] (K : CochainComplex C ℤ) (n : ℤ) {p : ℤ} {q : ℤ} (hpq : p = q) : HomologicalComplex.XIsoOfEq ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) n).toPrefunctor.obj K) hpq = HomologicalComplex.XIsoOfEq K (_ : p + n = q + n)

theorem CochainComplex.shiftFunctorAdd'_eq (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] (a : ℤ) (b : ℤ) (c : ℤ) (h : a + b = c) : CategoryTheory.shiftFunctorAdd' (CochainComplex C ℤ) a b c h = CochainComplex.shiftFunctorAdd' C a b c h

theorem CochainComplex.shiftFunctorAdd_eq (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] (a : ℤ) (b : ℤ) : CategoryTheory.shiftFunctorAdd (CochainComplex C ℤ) a b = CochainComplex.shiftFunctorAdd' C a b (a + b) (_ : a + b = a + b)

theorem CochainComplex.shiftFunctorZero_eq (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] : CategoryTheory.shiftFunctorZero (CochainComplex C ℤ) ℤ = CochainComplex.shiftFunctorZero' C 0 (_ : 0 = 0)

theorem CochainComplex.shiftFunctorComm_hom_app_f {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] (K : CochainComplex C ℤ) (a : ℤ) (b : ℤ) (p : ℤ) : ((CategoryTheory.shiftFunctorComm (CochainComplex C ℤ) a b).hom.app K).f p = (HomologicalComplex.XIsoOfEq K (_ : p + b + a = p + a + b)).hom

@[simp]

theorem CategoryTheory.Functor.mapCochainComplexShiftIso_inv_app_f {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] [CategoryTheory.Preadditive D] (F : CategoryTheory.Functor C D) [CategoryTheory.Functor.Additive F] (n : ℤ) (X : HomologicalComplex C (ComplexShape.up ℤ)) (i : ℤ) : ((CategoryTheory.Functor.mapCochainComplexShiftIso F n).inv.app X).f i = CategoryTheory.CategoryStruct.id (F.toPrefunctor.obj (X.X (i + n)))

@[simp]

theorem CategoryTheory.Functor.mapCochainComplexShiftIso_hom_app_f {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] [CategoryTheory.Preadditive D] (F : CategoryTheory.Functor C D) [CategoryTheory.Functor.Additive F] (n : ℤ) (X : HomologicalComplex C (ComplexShape.up ℤ)) (i : ℤ) : ((CategoryTheory.Functor.mapCochainComplexShiftIso F n).hom.app X).f i = CategoryTheory.CategoryStruct.id (F.toPrefunctor.obj (X.X (i + n)))

def CategoryTheory.Functor.mapCochainComplexShiftIso {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] [CategoryTheory.Preadditive D] (F : CategoryTheory.Functor C D) [CategoryTheory.Functor.Additive F] (n : ℤ) : CategoryTheory.Functor.comp (CategoryTheory.shiftFunctor (HomologicalComplex C (ComplexShape.up ℤ)) n) (CategoryTheory.Functor.mapHomologicalComplex F (ComplexShape.up ℤ)) ≅ CategoryTheory.Functor.comp (CategoryTheory.Functor.mapHomologicalComplex F (ComplexShape.up ℤ)) (CategoryTheory.shiftFunctor (HomologicalComplex D (ComplexShape.up ℤ)) n)

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.

instance CategoryTheory.Functor.commShiftMapCochainComplex {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] [CategoryTheory.Preadditive D] (F : CategoryTheory.Functor C D) [CategoryTheory.Functor.Additive F] : CategoryTheory.Functor.CommShift (CategoryTheory.Functor.mapHomologicalComplex F (ComplexShape.up ℤ)) ℤ

Equations

• CategoryTheory.Functor.commShiftMapCochainComplex F = CategoryTheory.Functor.CommShift.mk (CategoryTheory.Functor.mapCochainComplexShiftIso F)

theorem CategoryTheory.Functor.mapHomologicalComplex_commShiftIso_eq {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] [CategoryTheory.Preadditive D] (F : CategoryTheory.Functor C D) [CategoryTheory.Functor.Additive F] (n : ℤ) : CategoryTheory.Functor.commShiftIso (CategoryTheory.Functor.mapHomologicalComplex F (ComplexShape.up ℤ)) n = CategoryTheory.Functor.mapCochainComplexShiftIso F n

@[simp]

theorem CategoryTheory.Functor.mapHomologicalComplex_commShiftIso_hom_app_f {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] [CategoryTheory.Preadditive D] (F : CategoryTheory.Functor C D) [CategoryTheory.Functor.Additive F] (K : CochainComplex C ℤ) (n : ℤ) (i : ℤ) : ((CategoryTheory.Functor.commShiftIso (CategoryTheory.Functor.mapHomologicalComplex F (ComplexShape.up ℤ)) n).hom.app K).f i = CategoryTheory.CategoryStruct.id (((CategoryTheory.Functor.comp (CategoryTheory.shiftFunctor (HomologicalComplex C (ComplexShape.up ℤ)) n) (CategoryTheory.Functor.mapHomologicalComplex F (ComplexShape.up ℤ))).toPrefunctor.obj K).X i)

@[simp]

theorem CategoryTheory.Functor.mapHomologicalComplex_commShiftIso_inv_app_f {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] [CategoryTheory.Preadditive D] (F : CategoryTheory.Functor C D) [CategoryTheory.Functor.Additive F] (K : CochainComplex C ℤ) (n : ℤ) (i : ℤ) : ((CategoryTheory.Functor.commShiftIso (CategoryTheory.Functor.mapHomologicalComplex F (ComplexShape.up ℤ)) n).inv.app K).f i = CategoryTheory.CategoryStruct.id (((CategoryTheory.Functor.comp (CategoryTheory.Functor.mapHomologicalComplex F (ComplexShape.up ℤ)) (CategoryTheory.shiftFunctor (HomologicalComplex D (ComplexShape.up ℤ)) n)).toPrefunctor.obj K).X i)

def Homotopy.shift {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {K : CochainComplex C ℤ} {L : CochainComplex C ℤ} {φ₁ : K ⟶ L} {φ₂ : K ⟶ L} (h : Homotopy φ₁ φ₂) (n : ℤ) : Homotopy ((CategoryTheory.shiftFunctor (HomologicalComplex C (ComplexShape.up ℤ)) n).toPrefunctor.map φ₁) ((CategoryTheory.shiftFunctor (HomologicalComplex C (ComplexShape.up ℤ)) n).toPrefunctor.map φ₂)

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

Equations

• Homotopy.shift h n = Homotopy.mk fun (i j : ℤ) => n.negOnePow • h.hom (i + { as := n }.as) (j + { as := n }.as)

instance HomotopyCategory.instIsCompatibleWithShiftHomologicalComplexIntPreadditiveHasZeroMorphismsUpToAddRightCancelSemigroupToAddRightCancelMonoidToAddCancelMonoidInstAddGroupIntToOneInstSemiringIntInstCategoryHomologicalComplexHomotopicInstAddMonoidIntInstHasShiftCochainComplexPreadditiveHasZeroMorphismsIntToAddRightCancelSemigroupToAddRightCancelMonoidToAddCancelMonoidInstAddGroupIntToOneInstSemiringIntInstCategoryHomologicalComplexUpInstAddMonoidInt (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] : HomRel.IsCompatibleWithShift (homotopic C (ComplexShape.up ℤ)) ℤ

Equations

• (_ : HomRel.IsCompatibleWithShift (homotopic C (ComplexShape.up ℤ)) ℤ) = (_ : HomRel.IsCompatibleWithShift (homotopic C (ComplexShape.up ℤ)) ℤ)

noncomputable instance HomotopyCategory.hasShift (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] : CategoryTheory.HasShift (HomotopyCategory C (ComplexShape.up ℤ)) ℤ

Equations

• HomotopyCategory.hasShift C = id inferInstance

noncomputable instance HomotopyCategory.commShiftQuotient (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] : CategoryTheory.Functor.CommShift (HomotopyCategory.quotient C (ComplexShape.up ℤ)) ℤ

Equations

• HomotopyCategory.commShiftQuotient C = CategoryTheory.Quotient.functor_commShift (homotopic C (ComplexShape.up ℤ)) ℤ

instance HomotopyCategory.instAdditiveHomotopyCategoryIntUpToAddRightCancelSemigroupToAddRightCancelMonoidToAddCancelMonoidInstAddGroupIntToOneInstSemiringIntInstCategoryHomotopyCategoryInstPreadditiveHomotopyCategoryInstCategoryHomotopyCategoryShiftFunctorInstAddMonoidIntHasShift (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] (n : ℤ) : CategoryTheory.Functor.Additive (CategoryTheory.shiftFunctor (HomotopyCategory C (ComplexShape.up ℤ)) n)

Equations

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