Documentation

TauCeti.Algebra.Homology.Periodic.Cone

The mapping-cone conflation of periodic complexes #

Mathlib's HomologicalComplex.homotopyCofiber supplies mapping cones for arbitrary complex shapes. For a cyclic cochain complex its first projection is a chain map to the cochain shift: the differential on the shifted summand carries a minus sign. This gives the short complex Y ⟶ homotopyCofiber f ⟶ X⟦1⟧, split in every degree, for any map f : X ⟶ Y.

The sequence is a conflation for the degreewise extension of every exact structure on the base category, including the componentwise split structure. Taking f to be the identity gives the cone sequence used to compute suspension in the componentwise split exact category. The splitting is only degreewise: its retraction and section need not commute with differentials.

All constructions also work at period zero, where ZMod 0 is integer indexing; finite periodic complexes are obtained by taking a positive period.

References #

The cone and its component calculus are Mathlib's HomologicalComplex.homotopyCofiber.

source
noncomputable def TauCeti.PeriodicComplex.coneProjection {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasBinaryBiproducts C] {n : ℕ} {X Y : CochainComplex C (ZMod n)} (f : X ⟶ Y) :
HomologicalComplex.homotopyCofiber f ⟶ (CategoryTheory.shiftFunctor (HomologicalComplex C (ComplexShape.up (ZMod n))) 1).obj X

The first projection of the periodic mapping cone, with target the signed cochain shift.

Equations
Instances For
    source
    @[simp]
    theorem TauCeti.PeriodicComplex.coneProjection_f {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasBinaryBiproducts C] {n : ℕ} {X Y : CochainComplex C (ZMod n)} (f : X ⟶ Y) (i : ZMod n) :
    (coneProjection f).f i = HomologicalComplex.homotopyCofiber.fstX f i (i + ↑1) ⋯

    The projection in degree i is Mathlib's first cone projection.

    source
    @[simp]
    theorem TauCeti.PeriodicComplex.coneInclusion_comp_coneProjection {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasBinaryBiproducts C] {n : ℕ} {X Y : CochainComplex C (ZMod n)} (f : X ⟶ Y) :
    CategoryTheory.CategoryStruct.comp (HomologicalComplex.homotopyCofiber.inr f) (coneProjection f) = 0

    The cone inclusion followed by its shift projection is zero.

    source
    @[simp]
    theorem TauCeti.PeriodicComplex.coneInclusion_comp_coneProjection_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasBinaryBiproducts C] {n : ℕ} {X Y : CochainComplex C (ZMod n)} (f : X ⟶ Y) {Z : HomologicalComplex C (ComplexShape.up (ZMod n))} (h : (CategoryTheory.shiftFunctor (HomologicalComplex C (ComplexShape.up (ZMod n))) 1).obj X ⟶ Z) :
    CategoryTheory.CategoryStruct.comp (HomologicalComplex.homotopyCofiber.inr f) (CategoryTheory.CategoryStruct.comp (coneProjection f) h) = CategoryTheory.CategoryStruct.comp 0 h

    The cone inclusion followed by its shift projection is zero.

    source
    @[implicit_reducible]
    noncomputable def TauCeti.PeriodicComplex.coneSequence {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasBinaryBiproducts C] {n : ℕ} {X Y : CochainComplex C (ZMod n)} (f : X ⟶ Y) :
    CategoryTheory.ShortComplex (CochainComplex C (ZMod n))

    The mapping-cone short complex Y ⟶ homotopyCofiber f ⟶ X⟦1⟧.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      @[simp]
      theorem TauCeti.PeriodicComplex.coneSequence_X₁ {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasBinaryBiproducts C] {n : ℕ} {X Y : CochainComplex C (ZMod n)} (f : X ⟶ Y) :
      (coneSequence f).X₁ = Y
      source
      @[simp]
      theorem TauCeti.PeriodicComplex.coneSequence_X₂ {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasBinaryBiproducts C] {n : ℕ} {X Y : CochainComplex C (ZMod n)} (f : X ⟶ Y) :
      (coneSequence f).X₂ = HomologicalComplex.homotopyCofiber f
      source
      @[simp]
      theorem TauCeti.PeriodicComplex.coneSequence_X₃ {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasBinaryBiproducts C] {n : ℕ} {X Y : CochainComplex C (ZMod n)} (f : X ⟶ Y) :
      (coneSequence f).X₃ = (CategoryTheory.shiftFunctor (CochainComplex C (ZMod n)) 1).obj X
      source
      @[simp]
      theorem TauCeti.PeriodicComplex.coneSequence_f {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasBinaryBiproducts C] {n : ℕ} {X Y : CochainComplex C (ZMod n)} (f : X ⟶ Y) :
      (coneSequence f).f = HomologicalComplex.homotopyCofiber.inr f
      source
      @[simp]
      theorem TauCeti.PeriodicComplex.coneSequence_g {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasBinaryBiproducts C] {n : ℕ} {X Y : CochainComplex C (ZMod n)} (f : X ⟶ Y) :
      (coneSequence f).g = coneProjection f
      source
      noncomputable def TauCeti.PeriodicComplex.coneSequenceSplitting {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasBinaryBiproducts C] {n : ℕ} {X Y : CochainComplex C (ZMod n)} (f : X ⟶ Y) (i : ZMod n) :
      ((coneSequence f).map (HomologicalComplex.eval C (ComplexShape.up (ZMod n)) i)).Splitting

      The mapping-cone sequence splits in every degree. The retraction is the second projection and the section is the first inclusion; neither is asserted to be a chain map.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        @[simp]
        theorem TauCeti.PeriodicComplex.coneSequenceSplitting_r {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasBinaryBiproducts C] {n : ℕ} {X Y : CochainComplex C (ZMod n)} (f : X ⟶ Y) (i : ZMod n) :
        (coneSequenceSplitting f i).r = HomologicalComplex.homotopyCofiber.sndX f i
        source
        @[simp]
        theorem TauCeti.PeriodicComplex.coneSequenceSplitting_s {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasBinaryBiproducts C] {n : ℕ} {X Y : CochainComplex C (ZMod n)} (f : X ⟶ Y) (i : ZMod n) :
        (coneSequenceSplitting f i).s = HomologicalComplex.homotopyCofiber.inlX f (i + ↑1) i ⋯
        source
        @[simp]
        theorem TauCeti.PeriodicComplex.mapArrowHom_comp_coneProjection {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasBinaryBiproducts C] {n : ℕ} {X Y X' Y' : CochainComplex C (ZMod n)} (f : X ⟶ Y) (g : X' ⟶ Y') (α : CategoryTheory.Arrow.mk f ⟶ CategoryTheory.Arrow.mk g) :
        CategoryTheory.CategoryStruct.comp (HomologicalComplex.homotopyCofiber.mapArrowHom f g ⋯ α) (coneProjection g) = CategoryTheory.CategoryStruct.comp (coneProjection f) ((CategoryTheory.shiftFunctor (HomologicalComplex C (ComplexShape.up (ZMod n))) 1).map (CategoryTheory.Arrow.Hom.left α))

        The first cone projection is natural under commutative squares of periodic chain maps.

        source
        @[simp]
        theorem TauCeti.PeriodicComplex.mapArrowHom_comp_coneProjection_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasBinaryBiproducts C] {n : ℕ} {X Y X' Y' : CochainComplex C (ZMod n)} (f : X ⟶ Y) (g : X' ⟶ Y') (α : CategoryTheory.Arrow.mk f ⟶ CategoryTheory.Arrow.mk g) {Z : HomologicalComplex C (ComplexShape.up (ZMod n))} (h : (CategoryTheory.shiftFunctor (HomologicalComplex C (ComplexShape.up (ZMod n))) 1).obj X' ⟶ Z) :
        CategoryTheory.CategoryStruct.comp (HomologicalComplex.homotopyCofiber.mapArrowHom f g ⋯ α) (CategoryTheory.CategoryStruct.comp (coneProjection g) h) = CategoryTheory.CategoryStruct.comp (coneProjection f) (CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctor (HomologicalComplex C (ComplexShape.up (ZMod n))) 1).map (CategoryTheory.Arrow.Hom.left α)) h)

        The first cone projection is natural under commutative squares of periodic chain maps.

        source
        noncomputable def TauCeti.PeriodicComplex.coneSequenceMap {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasBinaryBiproducts C] {n : ℕ} {X Y X' Y' : CochainComplex C (ZMod n)} (f : X ⟶ Y) (g : X' ⟶ Y') (α : CategoryTheory.Arrow.mk f ⟶ CategoryTheory.Arrow.mk g) :
        coneSequence f ⟶ coneSequence g

        A commutative square induces a morphism of the corresponding mapping-cone short complexes.

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          source
          @[simp]
          theorem TauCeti.PeriodicComplex.coneSequenceMap_τ₁ {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasBinaryBiproducts C] {n : ℕ} {X Y X' Y' : CochainComplex C (ZMod n)} (f : X ⟶ Y) (g : X' ⟶ Y') (α : CategoryTheory.Arrow.mk f ⟶ CategoryTheory.Arrow.mk g) :
          (coneSequenceMap f g α).τ₁ = CategoryTheory.Arrow.Hom.right α
          source
          @[simp]
          theorem TauCeti.PeriodicComplex.coneSequenceMap_τ₂ {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasBinaryBiproducts C] {n : ℕ} {X Y X' Y' : CochainComplex C (ZMod n)} (f : X ⟶ Y) (g : X' ⟶ Y') (α : CategoryTheory.Arrow.mk f ⟶ CategoryTheory.Arrow.mk g) :
          (coneSequenceMap f g α).τ₂ = HomologicalComplex.homotopyCofiber.mapArrowHom f g ⋯ α
          source
          @[simp]
          theorem TauCeti.PeriodicComplex.coneSequenceMap_τ₃ {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasBinaryBiproducts C] {n : ℕ} {X Y X' Y' : CochainComplex C (ZMod n)} (f : X ⟶ Y) (g : X' ⟶ Y') (α : CategoryTheory.Arrow.mk f ⟶ CategoryTheory.Arrow.mk g) :
          (coneSequenceMap f g α).τ₃ = (CategoryTheory.shiftFunctor (CochainComplex C (ZMod n)) 1).map (CategoryTheory.Arrow.Hom.left α)
          source
          @[implicit_reducible]
          noncomputable def TauCeti.PeriodicComplex.coneSequenceFunctor {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasBinaryBiproducts C] {n : ℕ} :
          CategoryTheory.Functor (CategoryTheory.Arrow (CochainComplex C (ZMod n))) (CategoryTheory.ShortComplex (CochainComplex C (ZMod n)))

          Mapping-cone sequences depend functorially on arrows of periodic complexes.

          Equations
          • One or more equations did not get rendered due to their size.
          Instances For
            source
            @[simp]
            theorem TauCeti.PeriodicComplex.coneSequenceFunctor_obj {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasBinaryBiproducts C] {n : ℕ} (f : CategoryTheory.Arrow (CochainComplex C (ZMod n))) :
            coneSequenceFunctor.obj f = coneSequence f.hom
            source
            @[simp]
            theorem TauCeti.PeriodicComplex.coneSequenceFunctor_map {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasBinaryBiproducts C] {n : ℕ} {f g : CategoryTheory.Arrow (CochainComplex C (ZMod n))} (α : f ⟶ g) :
            coneSequenceFunctor.map α = coneSequenceMap f.hom g.hom α
            source
            theorem TauCeti.PeriodicComplex.conflation_coneSequence {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasBinaryBiproducts C] {n : ℕ} {X Y : CochainComplex C (ZMod n)} [CategoryTheory.Limits.HasZeroObject C] (E : ExactStructure C) (f : X ⟶ Y) :
            (E.homologicalComplex (ComplexShape.up (ZMod n))).Conflation (coneSequence f)

            The mapping-cone sequence is a conflation for the degreewise extension of any exact structure on the base category.