Documentation

Mathlib.Algebra.Homology.HomotopyCategory.ShiftSequence

Compatibilities of the homology functor with the shift #

This files studies how homology of cochain complexes behaves with respect to the shift: there is a natural isomorphism (K⟦n⟧).homology a ≅ K.homology a when n + a = a'. This is summarized by instances (homologyFunctor C (ComplexShape.up ℤ) 0).ShiftSequence ℤ in the CochainComplex and HomotopyCategory namespaces.

source
@[simp]
theorem CochainComplex.shiftShortComplexFunctor'_inv_app_τ₂ (C : Type u_1) [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] (n : ℤ) (i : ℤ) (j : ℤ) (k : ℤ) (i' : ℤ) (j' : ℤ) (k' : ℤ) (hi : n + i = i') (hj : n + j = j') (hk : n + k = k') (X : CochainComplex C ℤ) :
((CochainComplex.shiftShortComplexFunctor' C n i j k i' j' k' hi hj hk).inv.app X).τ₂ = (HomologicalComplex.XIsoOfEq X ⋯).inv
source
@[simp]
theorem CochainComplex.shiftShortComplexFunctor'_hom_app_τ₂ (C : Type u_1) [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] (n : ℤ) (i : ℤ) (j : ℤ) (k : ℤ) (i' : ℤ) (j' : ℤ) (k' : ℤ) (hi : n + i = i') (hj : n + j = j') (hk : n + k = k') (X : CochainComplex C ℤ) :
((CochainComplex.shiftShortComplexFunctor' C n i j k i' j' k' hi hj hk).hom.app X).τ₂ = (HomologicalComplex.XIsoOfEq X ⋯).hom
source
@[simp]
theorem CochainComplex.shiftShortComplexFunctor'_inv_app_τ₁ (C : Type u_1) [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] (n : ℤ) (i : ℤ) (j : ℤ) (k : ℤ) (i' : ℤ) (j' : ℤ) (k' : ℤ) (hi : n + i = i') (hj : n + j = j') (hk : n + k = k') (X : CochainComplex C ℤ) :
((CochainComplex.shiftShortComplexFunctor' C n i j k i' j' k' hi hj hk).inv.app X).τ₁ = n.negOnePow • (HomologicalComplex.XIsoOfEq X ⋯).inv
source
@[simp]
theorem CochainComplex.shiftShortComplexFunctor'_hom_app_τ₃ (C : Type u_1) [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] (n : ℤ) (i : ℤ) (j : ℤ) (k : ℤ) (i' : ℤ) (j' : ℤ) (k' : ℤ) (hi : n + i = i') (hj : n + j = j') (hk : n + k = k') (X : CochainComplex C ℤ) :
((CochainComplex.shiftShortComplexFunctor' C n i j k i' j' k' hi hj hk).hom.app X).τ₃ = n.negOnePow • (HomologicalComplex.XIsoOfEq X ⋯).hom
source
@[simp]
theorem CochainComplex.shiftShortComplexFunctor'_inv_app_τ₃ (C : Type u_1) [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] (n : ℤ) (i : ℤ) (j : ℤ) (k : ℤ) (i' : ℤ) (j' : ℤ) (k' : ℤ) (hi : n + i = i') (hj : n + j = j') (hk : n + k = k') (X : CochainComplex C ℤ) :
((CochainComplex.shiftShortComplexFunctor' C n i j k i' j' k' hi hj hk).inv.app X).τ₃ = n.negOnePow • (HomologicalComplex.XIsoOfEq X ⋯).inv
source
@[simp]
theorem CochainComplex.shiftShortComplexFunctor'_hom_app_τ₁ (C : Type u_1) [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] (n : ℤ) (i : ℤ) (j : ℤ) (k : ℤ) (i' : ℤ) (j' : ℤ) (k' : ℤ) (hi : n + i = i') (hj : n + j = j') (hk : n + k = k') (X : CochainComplex C ℤ) :
((CochainComplex.shiftShortComplexFunctor' C n i j k i' j' k' hi hj hk).hom.app X).τ₁ = n.negOnePow • (HomologicalComplex.XIsoOfEq X ⋯).hom
source
def CochainComplex.shiftShortComplexFunctor' (C : Type u_1) [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] (n : ℤ) (i : ℤ) (j : ℤ) (k : ℤ) (i' : ℤ) (j' : ℤ) (k' : ℤ) (hi : n + i = i') (hj : n + j = j') (hk : n + k = k') :
CategoryTheory.Functor.comp (CategoryTheory.shiftFunctor (CochainComplex C ℤ) n) (HomologicalComplex.shortComplexFunctor' C (ComplexShape.up ℤ) i j k) ≅ HomologicalComplex.shortComplexFunctor' C (ComplexShape.up ℤ) i' j' k'

The natural isomorphism (K⟦n⟧).sc' i j k ≅ K.sc' i' j' k' when n + i = i', n + j = j' and n + k = k'.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    @[simp]
    theorem CochainComplex.shiftShortComplexFunctorIso_inv_app_τ₂ (C : Type u_1) [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] (n : ℤ) (i : ℤ) (i' : ℤ) (hi : n + i = i') (X : CochainComplex C ℤ) :
    ((CochainComplex.shiftShortComplexFunctorIso C n i i' hi).inv.app X).τ₂ = (HomologicalComplex.XIsoOfEq X ⋯).inv
    source
    @[simp]
    theorem CochainComplex.shiftShortComplexFunctorIso_hom_app_τ₂ (C : Type u_1) [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] (n : ℤ) (i : ℤ) (i' : ℤ) (hi : n + i = i') (X : CochainComplex C ℤ) :
    ((CochainComplex.shiftShortComplexFunctorIso C n i i' hi).hom.app X).τ₂ = (HomologicalComplex.XIsoOfEq X ⋯).hom
    source
    @[simp]
    theorem CochainComplex.shiftShortComplexFunctorIso_hom_app_τ₁ (C : Type u_1) [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] (n : ℤ) (i : ℤ) (i' : ℤ) (hi : n + i = i') (X : CochainComplex C ℤ) :
    ((CochainComplex.shiftShortComplexFunctorIso C n i i' hi).hom.app X).τ₁ = n.negOnePow • (HomologicalComplex.XIsoOfEq X ⋯).hom
    source
    @[simp]
    theorem CochainComplex.shiftShortComplexFunctorIso_inv_app_τ₁ (C : Type u_1) [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] (n : ℤ) (i : ℤ) (i' : ℤ) (hi : n + i = i') (X : CochainComplex C ℤ) :
    ((CochainComplex.shiftShortComplexFunctorIso C n i i' hi).inv.app X).τ₁ = n.negOnePow • (HomologicalComplex.XIsoOfEq X ⋯).inv
    source
    @[simp]
    theorem CochainComplex.shiftShortComplexFunctorIso_hom_app_τ₃ (C : Type u_1) [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] (n : ℤ) (i : ℤ) (i' : ℤ) (hi : n + i = i') (X : CochainComplex C ℤ) :
    ((CochainComplex.shiftShortComplexFunctorIso C n i i' hi).hom.app X).τ₃ = n.negOnePow • (HomologicalComplex.XIsoOfEq X ⋯).hom
    source
    @[simp]
    theorem CochainComplex.shiftShortComplexFunctorIso_inv_app_τ₃ (C : Type u_1) [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] (n : ℤ) (i : ℤ) (i' : ℤ) (hi : n + i = i') (X : CochainComplex C ℤ) :
    ((CochainComplex.shiftShortComplexFunctorIso C n i i' hi).inv.app X).τ₃ = n.negOnePow • (HomologicalComplex.XIsoOfEq X ⋯).inv
    source
    noncomputable def CochainComplex.shiftShortComplexFunctorIso (C : Type u_1) [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] (n : ℤ) (i : ℤ) (i' : ℤ) (hi : n + i = i') :
    CategoryTheory.Functor.comp (CochainComplex.shiftFunctor C n) (HomologicalComplex.shortComplexFunctor C (ComplexShape.up ℤ) i) ≅ HomologicalComplex.shortComplexFunctor C (ComplexShape.up ℤ) i'

    The natural isomorphism (K⟦n⟧).sc i ≅ K.sc i' when n + i = i'.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      theorem CochainComplex.shiftShortComplexFunctorIso_zero_add_hom_app {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] (a : ℤ) (K : CochainComplex C ℤ) :
      (CochainComplex.shiftShortComplexFunctorIso C 0 a a ⋯).hom.app K = (HomologicalComplex.shortComplexFunctor C (ComplexShape.up ℤ) a).map ((CategoryTheory.shiftFunctorZero (CochainComplex C ℤ) ℤ).hom.app K)
      source
      theorem CochainComplex.shiftShortComplexFunctorIso_add'_hom_app {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] (n : ℤ) (m : ℤ) (mn : ℤ) (hmn : m + n = mn) (a : ℤ) (a' : ℤ) (a'' : ℤ) (ha' : n + a = a') (ha'' : m + a' = a'') (K : CochainComplex C ℤ) :
      (CochainComplex.shiftShortComplexFunctorIso C mn a a'' ⋯).hom.app K = CategoryTheory.CategoryStruct.comp ((HomologicalComplex.shortComplexFunctor C (ComplexShape.up ℤ) a).map ((CategoryTheory.shiftFunctorAdd' (CochainComplex C ℤ) m n mn hmn).hom.app K)) (CategoryTheory.CategoryStruct.comp ((CochainComplex.shiftShortComplexFunctorIso C n a a' ha').hom.app ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) m).obj K)) ((CochainComplex.shiftShortComplexFunctorIso C m a' a'' ha'').hom.app K))
      source
      noncomputable def CochainComplex.ShiftSequence.shiftIso (C : Type u_1) [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] [CategoryTheory.CategoryWithHomology C] (n : ℤ) (a : ℤ) (a' : ℤ) (ha' : n + a = a') :
      CategoryTheory.Functor.comp (CategoryTheory.shiftFunctor (HomologicalComplex C (ComplexShape.up ℤ)) n) (HomologicalComplex.homologyFunctor C (ComplexShape.up ℤ) a) ≅ HomologicalComplex.homologyFunctor C (ComplexShape.up ℤ) a'

      The natural isomorphism (K⟦n⟧).homology a ≅ K.homology a'when n + a = a.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        theorem CochainComplex.ShiftSequence.shiftIso_hom_app {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] [CategoryTheory.CategoryWithHomology C] (n : ℤ) (a : ℤ) (a' : ℤ) (ha' : n + a = a') (K : CochainComplex C ℤ) :
        (CochainComplex.ShiftSequence.shiftIso C n a a' ha').hom.app K = CategoryTheory.ShortComplex.homologyMap ((CochainComplex.shiftShortComplexFunctorIso C n a a' ha').hom.app K)
        source
        theorem CochainComplex.ShiftSequence.shiftIso_inv_app {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] [CategoryTheory.CategoryWithHomology C] (n : ℤ) (a : ℤ) (a' : ℤ) (ha' : n + a = a') (K : CochainComplex C ℤ) :
        (CochainComplex.ShiftSequence.shiftIso C n a a' ha').inv.app K = CategoryTheory.ShortComplex.homologyMap ((CochainComplex.shiftShortComplexFunctorIso C n a a' ha').inv.app K)
        source
        noncomputable instance CochainComplex.instShiftSequenceHomologicalComplexIntPreadditiveHasZeroMorphismsUpToAddRightCancelSemigroupToAddRightCancelMonoidToAddCancelMonoidInstAddGroupToOneInstSemiringInstCategoryHomologicalComplexHomologyFunctorOfNatInstOfNatInstAddMonoidInstHasShiftCochainComplexPreadditiveHasZeroMorphismsIntToAddRightCancelSemigroupToAddRightCancelMonoidToAddCancelMonoidInstAddGroupToOneInstSemiringInstCategoryHomologicalComplexUpInstAddMonoid {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] [CategoryTheory.CategoryWithHomology C] :
        CategoryTheory.Functor.ShiftSequence (HomologicalComplex.homologyFunctor C (ComplexShape.up ℤ) 0) ℤ
        Equations
        • One or more equations did not get rendered due to their size.
        source
        instance CochainComplex.instQuasiIsoIntPreadditiveHasZeroMorphismsUpToAddRightCancelSemigroupToAddRightCancelMonoidToAddCancelMonoidInstAddGroupToOneInstSemiringObjHomologicalComplexToQuiverToCategoryStructInstCategoryHomologicalComplexToPrefunctorShiftFunctorInstAddMonoidMapHasHomologySc {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] [CategoryTheory.CategoryWithHomology C] {K : CochainComplex C ℤ} {L : CochainComplex C ℤ} (φ : K ⟶ L) (n : ℤ) [QuasiIso φ] :
        QuasiIso ((CategoryTheory.shiftFunctor (HomologicalComplex C (ComplexShape.up ℤ)) n).map φ)
        Equations
        • ⋯ = ⋯
        source
        noncomputable instance HomotopyCategory.instShiftSequenceHomotopyCategoryIntUpToAddRightCancelSemigroupToAddRightCancelMonoidToAddCancelMonoidInstAddGroupToOneInstSemiringInstCategoryHomotopyCategoryHomologyFunctorOfNatInstOfNatInstAddMonoidHasShift (C : Type u_1) [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] [CategoryTheory.CategoryWithHomology C] :
        CategoryTheory.Functor.ShiftSequence (HomotopyCategory.homologyFunctor C (ComplexShape.up ℤ) 0) ℤ
        Equations
        • One or more equations did not get rendered due to their size.
        source
        theorem HomotopyCategory.homologyShiftIso_hom_app {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] [CategoryTheory.CategoryWithHomology C] (n : ℤ) (a : ℤ) (a' : ℤ) (ha' : n + a = a') (K : CochainComplex C ℤ) :
        (CategoryTheory.Functor.shiftIso (HomotopyCategory.homologyFunctor C (ComplexShape.up ℤ) 0) n a a' ha').hom.app ((HomotopyCategory.quotient C (ComplexShape.up ℤ)).obj K) = CategoryTheory.CategoryStruct.comp ((HomotopyCategory.homologyFunctor C (ComplexShape.up ℤ) a).map ((CategoryTheory.Functor.commShiftIso (HomotopyCategory.quotient C (ComplexShape.up ℤ)) n).inv.app K)) (CategoryTheory.CategoryStruct.comp ((HomotopyCategory.homologyFunctorFactors C (ComplexShape.up ℤ) a).hom.app ((CategoryTheory.shiftFunctor (HomologicalComplex C (ComplexShape.up ℤ)) n).obj K)) (CategoryTheory.CategoryStruct.comp ((CategoryTheory.Functor.shiftIso (HomologicalComplex.homologyFunctor C (ComplexShape.up ℤ) 0) n a a' ha').hom.app K) ((HomotopyCategory.homologyFunctorFactors C (ComplexShape.up ℤ) a').inv.app K)))