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.

@[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
@[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
@[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
@[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
@[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
@[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

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

    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

      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
        Equations
        • One or more equations did not get rendered due to their size.