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 ℤ.

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 ℤ.

source
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
    source
    @[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✝ : ℤ) :
    ((CochainComplex.shiftFunctor C n).map φ).f x✝ = φ.f (x✝ + n)
    source
    @[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)
    source
    @[simp]
    theorem CochainComplex.shiftFunctor_obj_d (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] (n : ℤ) (K : CochainComplex C ℤ) (x✝ x✝¹ : ℤ) :
    ((CochainComplex.shiftFunctor C n).obj K).d x✝ x✝¹ = n.negOnePow • K.d (x✝ + n) (x✝¹ + n)
    source
    instance CochainComplex.instAdditiveIntShiftFunctor (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] (n : ℤ) :
    (CochainComplex.shiftFunctor C n).Additive
    Equations
    • ⋯ = ⋯
    source
    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
    Instances For
      source
      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
        source
        @[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
        source
        @[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
        source
        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
          source
          @[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
          source
          @[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
          source
          instance CochainComplex.instHasShiftInt (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.
          source
          instance CochainComplex.instAdditiveHomologicalComplexIntUpShiftFunctor (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] (n : ℤ) :
          (CategoryTheory.shiftFunctor (HomologicalComplex C (ComplexShape.up ℤ)) n).Additive
          Equations
          • ⋯ = ⋯
          source
          @[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)
          source
          @[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 : ℤ) :
          ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) n).map φ).f p = φ.f (p + n)
          source
          @[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)
          source
          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
          source
          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
          source
          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
          source
          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
          source
          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
          source
          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
          source
          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 ⋯
          source
          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
          source
          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) ⋯
          source
          theorem CochainComplex.shiftFunctorZero_eq (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] :
          CategoryTheory.shiftFunctorZero (CochainComplex C ℤ) ℤ = CochainComplex.shiftFunctorZero' C 0 ⋯
          source
          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
          source
          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
            source
            @[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
            source
            @[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
            source
            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
              source
              @[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)))
              source
              @[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)))
              source
              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 := ⋯ }
              source
              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
              source
              @[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)
              source
              @[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)
              source
              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
              • h.shift n = { hom := fun (x x_1 : ℤ) => n.negOnePow • h.hom (x + { as := n }.as) (x_1 + { as := n }.as), zero := ⋯, comm := ⋯ }
              Instances For
                source
                instance HomotopyCategory.instIsCompatibleWithShiftHomologicalComplexIntUpHomotopic (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] :
                (homotopic C (ComplexShape.up ℤ)).IsCompatibleWithShift ℤ
                Equations
                • ⋯ = ⋯
                source
                noncomputable instance HomotopyCategory.hasShift (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] :
                CategoryTheory.HasShift (HomotopyCategory C (ComplexShape.up ℤ)) ℤ
                Equations
                source
                noncomputable instance HomotopyCategory.commShiftQuotient (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] :
                (HomotopyCategory.quotient C (ComplexShape.up ℤ)).CommShift ℤ
                Equations
                source
                instance HomotopyCategory.instAdditiveIntUpShiftFunctor (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] (n : ℤ) :
                (CategoryTheory.shiftFunctor (HomotopyCategory C (ComplexShape.up ℤ)) n).Additive
                Equations
                • ⋯ = ⋯
                source
                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.
                source
                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
                • ⋯ = ⋯