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) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] (n : ℤ) (K : CochainComplex C ℤ) (i : ℤ) (j : ℤ) :

((CochainComplex.shiftFunctor C n).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).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).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.

Instances For

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

CategoryTheory.Functor.Additive (CochainComplex.shiftFunctor C n)

Equations

⋯ = ⋯

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

Instances For

@[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 ⋯).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 ⋯).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.

Instances For

@[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 ⋯).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 ⋯).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.

Instances For

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

⋯ = ⋯

@[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).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).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).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 ⋯).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 ⋯).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 ⋯).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 ⋯).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 ⋯).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 ⋯).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).obj K) hpq = HomologicalComplex.XIsoOfEq K ⋯

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

theorem CochainComplex.shiftFunctorZero_eq (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] :

CategoryTheory.shiftFunctorZero (CochainComplex C ℤ) ℤ = CochainComplex.shiftFunctorZero' C 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 ⋯).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.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.obj (X.X (i + 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.

Instances For

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 = { iso := CategoryTheory.Functor.mapCochainComplexShiftIso F, zero := ⋯, add := ⋯ }

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 ℤ))).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)).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).map φ₁) ((CategoryTheory.shiftFunctor (HomologicalComplex C (ComplexShape.up ℤ)) n).map φ₂)

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

Equations

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

Instances For

instance HomotopyCategory.instIsCompatibleWithShiftHomologicalComplexIntPreadditiveHasZeroMorphismsUpToAddRightCancelSemigroupToAddRightCancelMonoidToAddCancelMonoidInstAddGroupIntToOneInstSemiringIntInstCategoryHomologicalComplexHomotopicInstAddMonoidIntInstHasShiftCochainComplexPreadditiveHasZeroMorphismsIntToAddRightCancelSemigroupToAddRightCancelMonoidToAddCancelMonoidInstAddGroupIntToOneInstSemiringIntInstCategoryHomologicalComplexUpInstAddMonoidInt (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] :

HomRel.IsCompatibleWithShift (homotopic C (ComplexShape.up ℤ)) ℤ

Equations

⋯ = ⋯

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

⋯ = ⋯