Documentation

TauCeti.Algebra.Homology.Periodic.Suspension

Stable suspension is the signed periodic shift #

The componentwise split exact category of cyclic cochain complexes is Frobenius. Its suspension can be computed from the conflation X ⟶ cone(id_X) ⟶ X⟦1⟧: the middle term is contractible, hence relatively injective and projective. The resulting identification is natural, since a chain map induces a map of these cone sequences whose cokernel component is its signed shift.

This file identifies stable suspension with the signed cyclic shift and shows that the canonical stable-to-homotopy equivalence intertwines suspension with the existing shift by one on the periodic homotopy category. This identifies the translation functors needed to compare the stable triangulation with mapping-cone triangles; it does not yet identify their distinguished triangles.

No positivity hypothesis on the period is needed: at period zero these constructions apply to integer-indexed cochain complexes.

References #

The presentation comparison is ExactStructure.IsFrobenius.projectiveStableIsoSuspensionObj. The natural-isomorphism construction follows the analogous finite-projective duplex comparison in TauCeti.CommutativeAlgebra.MatrixFactorization.Shift.

source
noncomputable def TauCeti.PeriodicComplex.coneInjectivePresentation {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] {n : ℕ} (X : CochainComplex C (ZMod n)) :
((ExactStructure.split C).homologicalComplex (ComplexShape.up (ZMod n))).InjectivePresentation X

The identity-cone injective presentation of a periodic complex. Its cokernel is the signed cyclic shift, and its middle term is contractible.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    @[simp]
    theorem TauCeti.PeriodicComplex.coneInjectivePresentation_I {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] {n : ℕ} (X : CochainComplex C (ZMod n)) :
    (coneInjectivePresentation X).I = HomologicalComplex.homotopyCofiber (CategoryTheory.CategoryStruct.id X)
    source
    @[simp]
    theorem TauCeti.PeriodicComplex.coneInjectivePresentation_K {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] {n : ℕ} (X : CochainComplex C (ZMod n)) :
    (coneInjectivePresentation X).K = (CategoryTheory.shiftFunctor (CochainComplex C (ZMod n)) 1).obj X
    source
    @[simp]
    theorem TauCeti.PeriodicComplex.coneInjectivePresentation_i {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] {n : ℕ} (X : CochainComplex C (ZMod n)) :
    (coneInjectivePresentation X).i = HomologicalComplex.homotopyCofiber.inr (CategoryTheory.CategoryStruct.id X)
    source
    @[simp]
    theorem TauCeti.PeriodicComplex.coneInjectivePresentation_p {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] {n : ℕ} (X : CochainComplex C (ZMod n)) :
    (coneInjectivePresentation X).p = coneProjection (CategoryTheory.CategoryStruct.id X)
    source
    @[simp]
    theorem TauCeti.PeriodicComplex.projectiveStableFunctor_map_coneInjectivePresentation_cokernelMap {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] {n : ℕ} {X Y : CochainComplex C (ZMod n)} (f : X ⟶ Y) :
    ((ExactStructure.split C).homologicalComplex (ComplexShape.up (ZMod n))).projectiveStableFunctor.map ((coneInjectivePresentation X).cokernelMap (coneInjectivePresentation Y) f) = ((ExactStructure.split C).homologicalComplex (ComplexShape.up (ZMod n))).projectiveStableFunctor.map ((CategoryTheory.shiftFunctor (HomologicalComplex C (ComplexShape.up (ZMod n))) 1).map f)

    The map induced on the cokernels of identity-cone presentations is the signed shift of the original chain map, in the projective stable category.

    source
    noncomputable def TauCeti.PeriodicComplex.splitStableSuspensionIsoShift (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] (n : ℕ) :
    ((ExactStructure.split C).homologicalComplex (ComplexShape.up (ZMod n))).projectiveStableFunctor.comp ⋯.stableSuspension ≅ (CategoryTheory.shiftFunctor (CochainComplex C (ZMod n)) 1).comp ((ExactStructure.split C).homologicalComplex (ComplexShape.up (ZMod n))).projectiveStableFunctor

    Stable suspension of the componentwise split exact category is naturally the image of the signed cyclic shift.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      @[simp]
      theorem TauCeti.PeriodicComplex.splitStableSuspensionIsoShift_hom_app (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] (n : ℕ) (X : CochainComplex C (ZMod n)) :
      (splitStableSuspensionIsoShift C n).hom.app X = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (((ExactStructure.split C).homologicalComplex (ComplexShape.up (ZMod n))).projectiveStableFunctor.map ((⋯.suspensionPresentation X).cokernelMap (coneInjectivePresentation X) (CategoryTheory.CategoryStruct.id X)))

      The suspension comparison is induced by the identity from the chosen injective presentation to the identity-cone presentation.

      source
      @[simp]
      theorem TauCeti.PeriodicComplex.splitStableSuspensionIsoShift_inv_app (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] (n : ℕ) (X : CochainComplex C (ZMod n)) :
      (splitStableSuspensionIsoShift C n).inv.app X = CategoryTheory.CategoryStruct.comp (((ExactStructure.split C).homologicalComplex (ComplexShape.up (ZMod n))).projectiveStableFunctor.map ((coneInjectivePresentation X).cokernelMap (⋯.suspensionPresentation X) (CategoryTheory.CategoryStruct.id X))) (CategoryTheory.eqToHom ⋯)

      The inverse suspension comparison is induced by the identity in the other direction.

      source
      noncomputable def TauCeti.PeriodicComplex.stableSuspensionCompStableToHomotopyIso (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] (n : ℕ) :
      ⋯.stableSuspension.comp (ExactStructure.homologicalComplexSplitStableToHomotopy C (ComplexShape.up (ZMod n)) ⋯) ≅ (ExactStructure.homologicalComplexSplitStableToHomotopy C (ComplexShape.up (ZMod n)) ⋯).comp (CategoryTheory.shiftFunctor (HomotopyCategory C (ComplexShape.up (ZMod n))) 1)

      The stable-to-homotopy equivalence intertwines stable suspension with the existing signed shift by one on the periodic homotopy category.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        @[simp]
        theorem TauCeti.PeriodicComplex.stableSuspensionCompStableToHomotopyIso_hom_app (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] (n : ℕ) (X : CochainComplex C (ZMod n)) :
        (stableSuspensionCompStableToHomotopyIso C n).hom.app (((ExactStructure.split C).homologicalComplex (ComplexShape.up (ZMod n))).projectiveStableFunctor.obj X) = CategoryTheory.CategoryStruct.comp ((ExactStructure.homologicalComplexSplitStableToHomotopy C (ComplexShape.up (ZMod n)) ⋯).map ((splitStableSuspensionIsoShift C n).hom.app X)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (CategoryTheory.CategoryStruct.comp ((CategoryTheory.Functor.commShiftIso (HomotopyCategory.quotient C (ComplexShape.up (ZMod n))) 1).hom.app X) (CategoryTheory.eqToHom ⋯)))

        On a represented complex, the intertwining isomorphism is the image of the suspension comparison, followed by the quotient's shift comparison.

        source
        @[simp]
        theorem TauCeti.PeriodicComplex.stableSuspensionCompStableToHomotopyIso_inv_app (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] (n : ℕ) (X : CochainComplex C (ZMod n)) :
        (stableSuspensionCompStableToHomotopyIso C n).inv.app (((ExactStructure.split C).homologicalComplex (ComplexShape.up (ZMod n))).projectiveStableFunctor.obj X) = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (CategoryTheory.CategoryStruct.comp ((CategoryTheory.Functor.commShiftIso (HomotopyCategory.quotient C (ComplexShape.up (ZMod n))) 1).inv.app X) (CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) ((ExactStructure.homologicalComplexSplitStableToHomotopy C (ComplexShape.up (ZMod n)) ⋯).map ((splitStableSuspensionIsoShift C n).inv.app X))))

        The inverse intertwining comparison uses the inverse quotient shift comparison and then the image of the inverse suspension comparison.