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 .

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

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

    Instances For

      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) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] (n₁ : ) (n₂ : ) (n₁₂ : ) (h : n₁ + n₂ = n₁₂) (X : CochainComplex C ) (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) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] (n₁ : ) (n₂ : ) (n₁₂ : ) (h : n₁ + n₂ = n₁₂) (X : CochainComplex C ) (i : ) :
        HomologicalComplex.Hom.f ((CochainComplex.shiftFunctorAdd' C n₁ n₂ n₁₂ h).hom.app X) i = (HomologicalComplex.XIsoOfEq X (_ : i + n₁₂ = i + n₂ + n₁)).hom

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

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

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

          Instances For