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 ℤ.
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
Instances For
@[simp]
theorem
CochainComplex.shiftFunctor_map_f
(C : Type u)
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
(n : ℤ)
{X✝ Y✝ : CochainComplex C ℤ}
(φ : X✝ ⟶ Y✝)
(x✝ : ℤ)
:
@[simp]
theorem
CochainComplex.shiftFunctor_obj_X
(C : Type u)
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
(n : ℤ)
(K : CochainComplex C ℤ)
(i : ℤ)
:
@[simp]
theorem
CochainComplex.shiftFunctor_obj_d
(C : Type u)
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
(n : ℤ)
(K : CochainComplex C ℤ)
(x✝ x✝¹ : ℤ)
:
instance
CochainComplex.instAdditiveIntShiftFunctor
(C : Type u)
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
(n : ℤ)
:
(shiftFunctor C n).Additive
def
CochainComplex.shiftFunctorObjXIso
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
(K : CochainComplex C ℤ)
(n i m : ℤ)
(hm : m = i + n)
:
The canonical isomorphism ((shiftFunctor C n).obj K).X i ≅ K.X m when m = i + n.
Equations
Instances For
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
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 : ℤ)
:
@[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 : ℤ)
:
def
CochainComplex.shiftFunctorAdd'
(C : Type u)
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
(n₁ n₂ n₁₂ : ℤ)
(h : n₁ + n₂ = n₁₂)
:
The compatibility of the shift functors on CochainComplex C ℤ with respect
to the addition of integers.
Equations
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 : ℤ)
:
@[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 : ℤ)
:
instance
CochainComplex.instHasShiftInt
(C : Type u)
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
:
Equations
instance
CochainComplex.instAdditiveHomologicalComplexIntUpShiftFunctor
(C : Type u)
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
(n : ℤ)
:
@[simp]
theorem
CochainComplex.shiftFunctor_obj_X'
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
(K : CochainComplex C ℤ)
(n p : ℤ)
:
@[simp]
theorem
CochainComplex.shiftFunctor_map_f'
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
{K L : CochainComplex C ℤ}
(φ : K ⟶ L)
(n p : ℤ)
:
@[simp]
theorem
CochainComplex.shiftFunctor_obj_d'
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
(K : CochainComplex C ℤ)
(n i j : ℤ)
:
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)
:
theorem
CochainComplex.shiftFunctorAdd_eq
(C : Type u)
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
(a b : ℤ)
:
theorem
CochainComplex.shiftFunctorZero_eq
(C : Type u)
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
:
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
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
Instances For
@[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 ℤ)
:
@[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 ℤ)
:
def
CategoryTheory.Functor.mapCochainComplexShiftIso
{C : Type u}
[Category.{v, u} C]
[Preadditive C]
{D : Type u'}
[Category.{v', u'} D]
[Preadditive D]
(F : Functor C D)
[F.Additive]
(n : ℤ)
:
(shiftFunctor (HomologicalComplex C (ComplexShape.up ℤ)) n).comp (F.mapHomologicalComplex (ComplexShape.up ℤ)) ≅ (F.mapHomologicalComplex (ComplexShape.up ℤ)).comp (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
Instances For
@[simp]
theorem
CategoryTheory.Functor.mapCochainComplexShiftIso_inv_app_f
{C : Type u}
[Category.{v, u} C]
[Preadditive C]
{D : Type u'}
[Category.{v', u'} D]
[Preadditive D]
(F : Functor C D)
[F.Additive]
(n : ℤ)
(X : HomologicalComplex C (ComplexShape.up ℤ))
(i : ℤ)
:
@[simp]
theorem
CategoryTheory.Functor.mapCochainComplexShiftIso_hom_app_f
{C : Type u}
[Category.{v, u} C]
[Preadditive C]
{D : Type u'}
[Category.{v', u'} D]
[Preadditive D]
(F : Functor C D)
[F.Additive]
(n : ℤ)
(X : HomologicalComplex C (ComplexShape.up ℤ))
(i : ℤ)
:
instance
CategoryTheory.Functor.commShiftMapCochainComplex
{C : Type u}
[Category.{v, u} C]
[Preadditive C]
{D : Type u'}
[Category.{v', u'} D]
[Preadditive D]
(F : Functor C D)
[F.Additive]
:
Equations
theorem
CategoryTheory.Functor.mapHomologicalComplex_commShiftIso_eq
{C : Type u}
[Category.{v, u} C]
[Preadditive C]
{D : Type u'}
[Category.{v', u'} D]
[Preadditive D]
(F : Functor C D)
[F.Additive]
(n : ℤ)
:
@[simp]
theorem
CategoryTheory.Functor.mapHomologicalComplex_commShiftIso_hom_app_f
{C : Type u}
[Category.{v, u} C]
[Preadditive C]
{D : Type u'}
[Category.{v', u'} D]
[Preadditive D]
(F : Functor C D)
[F.Additive]
(K : CochainComplex C ℤ)
(n i : ℤ)
:
(((F.mapHomologicalComplex (ComplexShape.up ℤ)).commShiftIso n).hom.app K).f i = CategoryStruct.id
((((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}
[Category.{v, u} C]
[Preadditive C]
{D : Type u'}
[Category.{v', u'} D]
[Preadditive D]
(F : Functor C D)
[F.Additive]
(K : CochainComplex C ℤ)
(n i : ℤ)
:
(((F.mapHomologicalComplex (ComplexShape.up ℤ)).commShiftIso n).inv.app K).f i = CategoryStruct.id
((((F.mapHomologicalComplex (ComplexShape.up ℤ)).comp
(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 L : CochainComplex C ℤ}
{φ₁ φ₂ : 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
noncomputable instance
HomotopyCategory.hasShift
(C : Type u)
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
:
Equations
noncomputable instance
HomotopyCategory.commShiftQuotient
(C : Type u)
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
:
(quotient C (ComplexShape.up ℤ)).CommShift ℤ
Equations
instance
HomotopyCategory.instAdditiveIntUpShiftFunctor
(C : Type u)
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
(n : ℤ)
:
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]
:
Equations
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]
: