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_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 : ℤ)
:
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)
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
(n : ℤ)
:
(CochainComplex.shiftFunctor C n).Additive
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
- K.shiftFunctorObjXIso 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)
:
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)
[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
@[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
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₁₂ ≅ (CochainComplex.shiftFunctor C n₁).comp (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.instHasShiftInt
(C : Type u)
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
:
Equations
- One or more equations did not get rendered due to their size.
instance
CochainComplex.instAdditiveHomologicalComplexIntUpShiftFunctor
(C : Type u)
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
(n : ℤ)
:
(CategoryTheory.shiftFunctor (HomologicalComplex C (ComplexShape.up ℤ)) n).Additive
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.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
CochainComplex.shiftEval_inv_app
(C : Type u)
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
(n : ℤ)
(i : ℤ)
(i' : ℤ)
(hi : n + i = i')
(X : CochainComplex C ℤ)
:
(CochainComplex.shiftEval C n i i' hi).inv.app X = (HomologicalComplex.XIsoOfEq X ⋯).inv
@[simp]
theorem
CochainComplex.shiftEval_hom_app
(C : Type u)
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
(n : ℤ)
(i : ℤ)
(i' : ℤ)
(hi : n + i = i')
(X : CochainComplex C ℤ)
:
(CochainComplex.shiftEval C n i i' hi).hom.app X = (HomologicalComplex.XIsoOfEq X ⋯).hom
def
CochainComplex.shiftEval
(C : Type u)
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
(n : ℤ)
(i : ℤ)
(i' : ℤ)
(hi : n + i = i')
:
(CategoryTheory.shiftFunctor (CochainComplex C ℤ) n).comp (HomologicalComplex.eval C (ComplexShape.up ℤ) i) ≅ HomologicalComplex.eval C (ComplexShape.up ℤ) i'
Shifting cochain complexes by n and evaluating in a degree i identifies
to the evaluation in degree i' when n + i = i'.
Equations
- CochainComplex.shiftEval C n i i' hi = CategoryTheory.NatIso.ofComponents (fun (K : CochainComplex C ℤ) => HomologicalComplex.XIsoOfEq K ⋯) ⋯
Instances For
@[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)
[F.Additive]
(n : ℤ)
(X : HomologicalComplex C (ComplexShape.up ℤ))
(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}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
{D : Type u'}
[CategoryTheory.Category.{v', u'} D]
[CategoryTheory.Preadditive D]
(F : CategoryTheory.Functor C D)
[F.Additive]
(n : ℤ)
(X : HomologicalComplex C (ComplexShape.up ℤ))
(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}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
{D : Type u'}
[CategoryTheory.Category.{v', u'} D]
[CategoryTheory.Preadditive D]
(F : CategoryTheory.Functor C D)
[F.Additive]
(n : ℤ)
:
(CategoryTheory.shiftFunctor (HomologicalComplex C (ComplexShape.up ℤ)) n).comp
(F.mapHomologicalComplex (ComplexShape.up ℤ)) ≅ (F.mapHomologicalComplex (ComplexShape.up ℤ)).comp
(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.
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)
[F.Additive]
:
(F.mapHomologicalComplex (ComplexShape.up ℤ)).CommShift ℤ
Equations
- F.commShiftMapCochainComplex = { iso := F.mapCochainComplexShiftIso, 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)
[F.Additive]
(n : ℤ)
:
(F.mapHomologicalComplex (ComplexShape.up ℤ)).commShiftIso n = F.mapCochainComplexShiftIso 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)
[F.Additive]
(K : CochainComplex C ℤ)
(n : ℤ)
(i : ℤ)
:
(((F.mapHomologicalComplex (ComplexShape.up ℤ)).commShiftIso n).hom.app K).f i = CategoryTheory.CategoryStruct.id
((((CategoryTheory.shiftFunctor (HomologicalComplex C (ComplexShape.up ℤ)) n).comp
(F.mapHomologicalComplex (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)
[F.Additive]
(K : CochainComplex C ℤ)
(n : ℤ)
(i : ℤ)
:
(((F.mapHomologicalComplex (ComplexShape.up ℤ)).commShiftIso n).inv.app K).f i = CategoryTheory.CategoryStruct.id
((((F.mapHomologicalComplex (ComplexShape.up ℤ)).comp
(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
Instances For
instance
HomotopyCategory.instIsCompatibleWithShiftHomologicalComplexIntUpHomotopic
(C : Type u)
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
:
(homotopic C (ComplexShape.up ℤ)).IsCompatibleWithShift ℤ
Equations
- ⋯ = ⋯
noncomputable instance
HomotopyCategory.hasShift
(C : Type u)
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
:
Equations
- HomotopyCategory.hasShift C = id inferInstance
noncomputable instance
HomotopyCategory.commShiftQuotient
(C : Type u)
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
:
(HomotopyCategory.quotient C (ComplexShape.up ℤ)).CommShift ℤ
instance
HomotopyCategory.instAdditiveIntUpShiftFunctor
(C : Type u)
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
(n : ℤ)
:
(CategoryTheory.shiftFunctor (HomotopyCategory C (ComplexShape.up ℤ)) n).Additive
Equations
- ⋯ = ⋯
noncomputable instance
HomotopyCategory.instCommShiftIntUpMapHomotopyCategory
{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)
[F.Additive]
:
(F.mapHomotopyCategory (ComplexShape.up ℤ)).CommShift ℤ
Equations
- One or more equations did not get rendered due to their size.
instance
HomotopyCategory.instCommShiftHomologicalComplexIntUpHomFunctorMapHomotopyCategoryFactors
{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)
[F.Additive]
:
CategoryTheory.NatTrans.CommShift (F.mapHomotopyCategoryFactors (ComplexShape.up ℤ)).hom ℤ
Equations
- ⋯ = ⋯