Documentation

TauCeti.Algebra.Homology.Periodic.Compression.Triangulated

Compression is a triangle functor #

The n-periodic compression K^b(C) ⥤ K_n(C) from the homotopy category of bounded cochain complexes to the n-periodic homotopy category is a triangle functor (TauCeti.PeriodicComplex.homotopyCompressionFunctor_isTriangulated), for every additive category C and every period n.

Every distinguished triangle of K^b(C) is isomorphic to the image of the mapping-cone triangle of a morphism φ of bounded complexes. The compression functor sends that image to the class of the compression of the mapping-cone triangle of φ, with the shift datum descended from TauCeti.PeriodicComplex.compressionShiftIso, and this compression is the periodic mapping-cone triangle of the compression of φ, which is distinguished.

References #

source
noncomputable def TauCeti.PeriodicComplex.compressionFunctorMapTriangleMappingConeTriangleIso {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasBinaryBiproducts C] [CategoryTheory.Limits.HasFiniteCoproducts C] (n : ℕ) {K L : CochainComplex.Bounded C} (φ : K ⟶ L) :
(compressionFunctor n).mapTriangle.obj (CochainComplex.Bounded.mappingConeTriangle φ) ≅ compressionMappingConeTriangle n φ.hom

Compression of bounded complexes carries the mapping-cone triangle of φ, with the shift datum compressionFunctorShiftIso, to the compression of the mapping-cone triangle of the underlying morphism of cochain complexes.

Instances For
    source
    @[simp]
    theorem TauCeti.PeriodicComplex.compressionFunctorMapTriangleMappingConeTriangleIso_inv_hom₂ {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasBinaryBiproducts C] [CategoryTheory.Limits.HasFiniteCoproducts C] (n : ℕ) {K L : CochainComplex.Bounded C} (φ : K ⟶ L) :
    (compressionFunctorMapTriangleMappingConeTriangleIso n φ).inv.hom₂ = CategoryTheory.eqToHom ⋯
    source
    @[simp]
    theorem TauCeti.PeriodicComplex.compressionFunctorMapTriangleMappingConeTriangleIso_inv_hom₃ {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasBinaryBiproducts C] [CategoryTheory.Limits.HasFiniteCoproducts C] (n : ℕ) {K L : CochainComplex.Bounded C} (φ : K ⟶ L) :
    (compressionFunctorMapTriangleMappingConeTriangleIso n φ).inv.hom₃ = CategoryTheory.eqToHom ⋯
    source
    @[simp]
    theorem TauCeti.PeriodicComplex.compressionFunctorMapTriangleMappingConeTriangleIso_hom_hom₁ {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasBinaryBiproducts C] [CategoryTheory.Limits.HasFiniteCoproducts C] (n : ℕ) {K L : CochainComplex.Bounded C} (φ : K ⟶ L) :
    (compressionFunctorMapTriangleMappingConeTriangleIso n φ).hom.hom₁ = CategoryTheory.eqToHom ⋯
    source
    @[simp]
    theorem TauCeti.PeriodicComplex.compressionFunctorMapTriangleMappingConeTriangleIso_inv_hom₁ {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasBinaryBiproducts C] [CategoryTheory.Limits.HasFiniteCoproducts C] (n : ℕ) {K L : CochainComplex.Bounded C} (φ : K ⟶ L) :
    (compressionFunctorMapTriangleMappingConeTriangleIso n φ).inv.hom₁ = CategoryTheory.eqToHom ⋯
    source
    @[simp]
    theorem TauCeti.PeriodicComplex.compressionFunctorMapTriangleMappingConeTriangleIso_hom_hom₂ {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasBinaryBiproducts C] [CategoryTheory.Limits.HasFiniteCoproducts C] (n : ℕ) {K L : CochainComplex.Bounded C} (φ : K ⟶ L) :
    (compressionFunctorMapTriangleMappingConeTriangleIso n φ).hom.hom₂ = CategoryTheory.eqToHom ⋯
    source
    @[simp]
    theorem TauCeti.PeriodicComplex.compressionFunctorMapTriangleMappingConeTriangleIso_hom_hom₃ {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasBinaryBiproducts C] [CategoryTheory.Limits.HasFiniteCoproducts C] (n : ℕ) {K L : CochainComplex.Bounded C} (φ : K ⟶ L) :
    (compressionFunctorMapTriangleMappingConeTriangleIso n φ).hom.hom₃ = CategoryTheory.eqToHom ⋯
    source
    instance TauCeti.PeriodicComplex.homotopyCompressionFunctor_isTriangulated {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasBinaryBiproducts C] [CategoryTheory.Limits.HasFiniteCoproducts C] (n : ℕ) [CategoryTheory.Limits.HasZeroObject C] :
    (homotopyCompressionFunctor n).IsTriangulated

    Compression is a triangle functor. The n-periodic compression functor from the homotopy category of bounded cochain complexes to the n-periodic homotopy category sends distinguished triangles to distinguished triangles.