Documentation

TauCeti.Algebra.Homology.Periodic.Connecting

Connecting maps of periodic cone conflations #

The identity-cone presentation computes suspension in the componentwise split exact category of periodic complexes. This file computes connecting maps through that presentation and expresses Happel's conflation triangles using the signed cyclic shift of actual complexes. In particular, the conflation Y ⟶ cone(f) ⟶ X⟦1⟧ has connecting map f⟦1⟧, after identifying the two suspension objects. Rotation then shows that the usual mapping-cone triangle is distinguished in the stable category.

The cone differential has lower-left block f. Thus the connecting map of this cone conflation is positive; the last map of the usual triangle X ⟶ Y ⟶ cone(f) ⟶ X⟦1⟧ has minus the cone projection, as required by rotation. The results here concern the stable triangulation and do not install a triangulation on the periodic homotopy category.

These comparisons apply to every positive period and also to the integer-indexed case ZMod 0. The base category needs only a preadditive structure, a zero object, and binary biproducts.

References #

The construction uses PeriodicComplex.splitStableSuspensionIsoShift and the presentation-independent connecting-map API ExactStructure.IsFrobenius.projectiveStableFunctor_map_eq_connectingMap_comp.

source
noncomputable def TauCeti.PeriodicComplex.splitStableShiftObjIso (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))).projectiveStableFunctor.obj ((CategoryTheory.shiftFunctor (HomologicalComplex C (ComplexShape.up (ZMod n))) 1).obj X) ≅ (CategoryTheory.shiftFunctor ((ExactStructure.split C).homologicalComplex (ComplexShape.up (ZMod n))).ProjectiveStableCategory 1).obj (((ExactStructure.split C).homologicalComplex (ComplexShape.up (ZMod n))).projectiveStableFunctor.obj X)

The stable image of the signed cyclic shift is isomorphic to the stable shift by one. The isomorphism comes from the identity-cone injective presentation.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    @[simp]
    theorem TauCeti.PeriodicComplex.splitStableShiftObjIso_hom (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)) :
    (splitStableShiftObjIso C n X).hom = CategoryTheory.CategoryStruct.comp ((splitStableSuspensionIsoShift C n).inv.app X) (⋯.stableShiftFunctorOneIso.inv.app (((ExactStructure.split C).homologicalComplex (ComplexShape.up (ZMod n))).projectiveStableFunctor.obj X))

    The forward shift comparison passes through stable suspension.

    source
    @[simp]
    theorem TauCeti.PeriodicComplex.splitStableShiftObjIso_inv (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)) :
    (splitStableShiftObjIso C n X).inv = CategoryTheory.CategoryStruct.comp (⋯.stableShiftFunctorOneIso.hom.app (((ExactStructure.split C).homologicalComplex (ComplexShape.up (ZMod n))).projectiveStableFunctor.obj X)) ((splitStableSuspensionIsoShift C n).hom.app X)

    The inverse shift comparison passes from the stable shift through stable suspension.

    source
    theorem TauCeti.PeriodicComplex.splitStableShiftObjIso_hom_naturality {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) :
    CategoryTheory.CategoryStruct.comp (((ExactStructure.split C).homologicalComplex (ComplexShape.up (ZMod n))).projectiveStableFunctor.map ((CategoryTheory.shiftFunctor (HomologicalComplex C (ComplexShape.up (ZMod n))) 1).map f)) (splitStableShiftObjIso C n Y).hom = CategoryTheory.CategoryStruct.comp (splitStableShiftObjIso C n X).hom ((CategoryTheory.shiftFunctor ((ExactStructure.split C).homologicalComplex (ComplexShape.up (ZMod n))).ProjectiveStableCategory 1).map (((ExactStructure.split C).homologicalComplex (ComplexShape.up (ZMod n))).projectiveStableFunctor.map f))

    The comparison between the two shifts is natural in periodic chain maps.

    source
    theorem TauCeti.PeriodicComplex.splitStableShiftObjIso_hom_naturality_assoc {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) {Z : ((ExactStructure.split C).homologicalComplex (ComplexShape.up (ZMod n))).ProjectiveStableCategory} (h : (CategoryTheory.shiftFunctor ((ExactStructure.split C).homologicalComplex (ComplexShape.up (ZMod n))).ProjectiveStableCategory 1).obj (((ExactStructure.split C).homologicalComplex (ComplexShape.up (ZMod n))).projectiveStableFunctor.obj Y) ⟶ Z) :
    CategoryTheory.CategoryStruct.comp (((ExactStructure.split C).homologicalComplex (ComplexShape.up (ZMod n))).projectiveStableFunctor.map ((CategoryTheory.shiftFunctor (HomologicalComplex C (ComplexShape.up (ZMod n))) 1).map f)) (CategoryTheory.CategoryStruct.comp (splitStableShiftObjIso C n Y).hom h) = CategoryTheory.CategoryStruct.comp (splitStableShiftObjIso C n X).hom (CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctor ((ExactStructure.split C).homologicalComplex (ComplexShape.up (ZMod n))).ProjectiveStableCategory 1).map (((ExactStructure.split C).homologicalComplex (ComplexShape.up (ZMod n))).projectiveStableFunctor.map f)) h)

    The comparison between the two shifts is natural in periodic chain maps.

    source
    theorem TauCeti.PeriodicComplex.projectiveStableFunctor_map_comp_splitStableShiftObjIso {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] {n : ℕ} {T : CategoryTheory.ShortComplex (CochainComplex C (ZMod n))} (hT : ((ExactStructure.split C).homologicalComplex (ComplexShape.up (ZMod n))).Conflation T) (a : T.X₂ ⟶ HomologicalComplex.homotopyCofiber (CategoryTheory.CategoryStruct.id T.X₁)) (δ : T.X₃ ⟶ (CategoryTheory.shiftFunctor (CochainComplex C (ZMod n)) 1).obj T.X₁) (ha : CategoryTheory.CategoryStruct.comp T.f a = HomologicalComplex.homotopyCofiber.inr (CategoryTheory.CategoryStruct.id T.X₁)) (hδ : CategoryTheory.CategoryStruct.comp T.g δ = CategoryTheory.CategoryStruct.comp a (coneProjection (CategoryTheory.CategoryStruct.id T.X₁))) :
    CategoryTheory.CategoryStruct.comp (((ExactStructure.split C).homologicalComplex (ComplexShape.up (ZMod n))).projectiveStableFunctor.map δ) (splitStableShiftObjIso C n T.X₁).hom = CategoryTheory.CategoryStruct.comp (((ExactStructure.split C).homologicalComplex (ComplexShape.up (ZMod n))).projectiveStableFunctor.map (⋯.connectingMap hT)) (⋯.stableSuspensionObjIsoShift T.X₁).hom

    A connecting map computed with the identity-cone presentation agrees with Happel's connecting map, after passing to the stable category and identifying the shifts.

    source
    theorem TauCeti.PeriodicComplex.stableConflationTriangle_eq_mk_of_conePresentation {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] {n : ℕ} {T : CategoryTheory.ShortComplex (CochainComplex C (ZMod n))} (hT : ((ExactStructure.split C).homologicalComplex (ComplexShape.up (ZMod n))).Conflation T) (a : T.X₂ ⟶ HomologicalComplex.homotopyCofiber (CategoryTheory.CategoryStruct.id T.X₁)) (δ : T.X₃ ⟶ (CategoryTheory.shiftFunctor (CochainComplex C (ZMod n)) 1).obj T.X₁) (ha : CategoryTheory.CategoryStruct.comp T.f a = HomologicalComplex.homotopyCofiber.inr (CategoryTheory.CategoryStruct.id T.X₁)) (hδ : CategoryTheory.CategoryStruct.comp T.g δ = CategoryTheory.CategoryStruct.comp a (coneProjection (CategoryTheory.CategoryStruct.id T.X₁))) :
    ⋯.stableConflationTriangle T hT = CategoryTheory.Pretriangulated.Triangle.mk (((ExactStructure.split C).homologicalComplex (ComplexShape.up (ZMod n))).projectiveStableFunctor.map T.f) (((ExactStructure.split C).homologicalComplex (ComplexShape.up (ZMod n))).projectiveStableFunctor.map T.g) (CategoryTheory.CategoryStruct.comp (((ExactStructure.split C).homologicalComplex (ComplexShape.up (ZMod n))).projectiveStableFunctor.map δ) (splitStableShiftObjIso C n T.X₁).hom)

    The standard stable triangle of a componentwise split conflation can be written using any connecting map computed through the identity cone.

    source
    theorem TauCeti.PeriodicComplex.projectiveStableFunctor_map_shift_comp_splitStableShiftObjIso {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) :
    CategoryTheory.CategoryStruct.comp (((ExactStructure.split C).homologicalComplex (ComplexShape.up (ZMod n))).projectiveStableFunctor.map ((CategoryTheory.shiftFunctor (HomologicalComplex C (ComplexShape.up (ZMod n))) 1).map f)) (splitStableShiftObjIso C n Y).hom = CategoryTheory.CategoryStruct.comp (((ExactStructure.split C).homologicalComplex (ComplexShape.up (ZMod n))).projectiveStableFunctor.map (⋯.connectingMap ⋯)) (⋯.stableSuspensionObjIsoShift Y).hom

    The connecting map of Y ⟶ cone(f) ⟶ X⟦1⟧ is the signed shift of f, under the identity-cone comparison of suspension objects.

    source
    theorem TauCeti.PeriodicComplex.stableConflationTriangle_coneSequence_eq_mk {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) :
    ⋯.stableConflationTriangle (coneSequence f) ⋯ = CategoryTheory.Pretriangulated.Triangle.mk (((ExactStructure.split C).homologicalComplex (ComplexShape.up (ZMod n))).projectiveStableFunctor.map (HomologicalComplex.homotopyCofiber.inr f)) (((ExactStructure.split C).homologicalComplex (ComplexShape.up (ZMod n))).projectiveStableFunctor.map (coneProjection f)) (CategoryTheory.CategoryStruct.comp (((ExactStructure.split C).homologicalComplex (ComplexShape.up (ZMod n))).projectiveStableFunctor.map ((CategoryTheory.shiftFunctor (HomologicalComplex C (ComplexShape.up (ZMod n))) 1).map f)) (splitStableShiftObjIso C n Y).hom)

    The standard triangle of the cone conflation has the shifted original map as its connecting arrow, expressed through the stable shift comparison.

    source
    theorem TauCeti.PeriodicComplex.coneSequence_distinguished {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) :
    CategoryTheory.Pretriangulated.Triangle.mk (((ExactStructure.split C).homologicalComplex (ComplexShape.up (ZMod n))).projectiveStableFunctor.map (HomologicalComplex.homotopyCofiber.inr f)) (((ExactStructure.split C).homologicalComplex (ComplexShape.up (ZMod n))).projectiveStableFunctor.map (coneProjection f)) (CategoryTheory.CategoryStruct.comp (((ExactStructure.split C).homologicalComplex (ComplexShape.up (ZMod n))).projectiveStableFunctor.map ((CategoryTheory.shiftFunctor (HomologicalComplex C (ComplexShape.up (ZMod n))) 1).map f)) (splitStableShiftObjIso C n Y).hom) ∈ CategoryTheory.Pretriangulated.distinguishedTriangles

    The periodic cone conflation gives a distinguished stable triangle with explicit connecting map f⟦1⟧.

    source
    theorem TauCeti.PeriodicComplex.mappingCone_distinguished {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) :
    CategoryTheory.Pretriangulated.Triangle.mk (((ExactStructure.split C).homologicalComplex (ComplexShape.up (ZMod n))).projectiveStableFunctor.map f) (((ExactStructure.split C).homologicalComplex (ComplexShape.up (ZMod n))).projectiveStableFunctor.map (HomologicalComplex.homotopyCofiber.inr f)) (-CategoryTheory.CategoryStruct.comp (((ExactStructure.split C).homologicalComplex (ComplexShape.up (ZMod n))).projectiveStableFunctor.map (coneProjection f)) (splitStableShiftObjIso C n X).hom) ∈ CategoryTheory.Pretriangulated.distinguishedTriangles

    The concrete periodic mapping cone realizes a distinguished stable triangle. Its last arrow is minus the cone projection, followed by the comparison with stable suspension.