Mapping-cone triangles of bounded complexes

The mapping cone of a morphism φ : K ⟶ L of bounded cochain complexes is bounded, so Mathlib's mapping-cone triangle K ⟶ L ⟶ cone φ ⟶ K⟦1⟧ is a triangle of bounded complexes, CochainComplex.Bounded.mappingConeTriangle φ. Its image in the bounded homotopy category is distinguished, and every distinguished triangle there is isomorphic to such an image (TauCeti.HomotopyCategory.Bounded.mem_distTriang_iff). This is the bounded counterpart of the definition of the distinguished triangles of Mathlib's HomotopyCategory C (.up ℤ).

Consequently a functor out of the bounded homotopy category which commutes with the shift is a triangle functor as soon as it sends the images of bounded mapping-cone triangles to distinguished triangles (TauCeti.HomotopyCategory.Bounded.isTriangulated_of_mappingConeTriangle).

@[reducible, inline]

noncomputable abbrev CochainComplex.Bounded.mappingCone {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasBinaryBiproducts C] {K L : Bounded C} (φ : K ⟶ L) : Bounded C

The mapping cone of a morphism of bounded cochain complexes, as a bounded complex.

@[implicit_reducible]

noncomputable def CochainComplex.Bounded.mappingConeTriangle {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasBinaryBiproducts C] {K L : Bounded C} (φ : K ⟶ L) : CategoryTheory.Pretriangulated.Triangle (Bounded C)

The mapping-cone triangle K ⟶ L ⟶ cone φ ⟶ K⟦1⟧ of a morphism of bounded cochain complexes. Its third morphism is induced by the cocycle -mappingCone.fst φ, as in Mathlib's CochainComplex.mappingCone.triangle, which is its image in all cochain complexes (CochainComplex.Bounded.ιMapTriangleMappingConeTriangleIso).

@[simp]

theorem CochainComplex.Bounded.mappingConeTriangle_mor₁ {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasBinaryBiproducts C] {K L : Bounded C} (φ : K ⟶ L) : (mappingConeTriangle φ).mor₁ = φ

@[simp]

theorem CochainComplex.Bounded.mappingConeTriangle_mor₃ {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasBinaryBiproducts C] {K L : Bounded C} (φ : K ⟶ L) : (mappingConeTriangle φ).mor₃ = CategoryTheory.ObjectProperty.homMk (CategoryTheory.CategoryStruct.comp ((-mappingCone.fst φ.hom).rightShift 1 0 mappingConeTriangle._proof_1).homOf ((CategoryTheory.Functor.commShiftIso (ι C) 1).inv.app K))

@[simp]

theorem CochainComplex.Bounded.mappingConeTriangle_mor₂ {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasBinaryBiproducts C] {K L : Bounded C} (φ : K ⟶ L) : (mappingConeTriangle φ).mor₂ = CategoryTheory.ObjectProperty.homMk (mappingCone.inr φ.hom)

@[simp]

theorem CochainComplex.Bounded.mappingConeTriangle_obj₃ {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasBinaryBiproducts C] {K L : Bounded C} (φ : K ⟶ L) : (mappingConeTriangle φ).obj₃ = mappingCone φ

@[simp]

theorem CochainComplex.Bounded.mappingConeTriangle_obj₂ {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasBinaryBiproducts C] {K L : Bounded C} (φ : K ⟶ L) : (mappingConeTriangle φ).obj₂ = L

@[simp]

theorem CochainComplex.Bounded.mappingConeTriangle_obj₁ {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasBinaryBiproducts C] {K L : Bounded C} (φ : K ⟶ L) : (mappingConeTriangle φ).obj₁ = K

noncomputable def CochainComplex.Bounded.ιMapTriangleMappingConeTriangleIso {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasBinaryBiproducts C] {K L : Bounded C} (φ : K ⟶ L) : (ι C).mapTriangle.obj (mappingConeTriangle φ) ≅ mappingCone.triangle φ.hom

The mapping-cone triangle of a morphism of bounded complexes is Mathlib's mapping-cone triangle of the underlying morphism of cochain complexes.

@[simp]

theorem CochainComplex.Bounded.ιMapTriangleMappingConeTriangleIso_inv_hom₃ {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasBinaryBiproducts C] {K L : Bounded C} (φ : K ⟶ L) : (ιMapTriangleMappingConeTriangleIso φ).inv.hom₃ = CategoryTheory.CategoryStruct.id (CochainComplex.mappingCone φ.hom)

@[simp]

theorem CochainComplex.Bounded.ιMapTriangleMappingConeTriangleIso_inv_hom₂ {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasBinaryBiproducts C] {K L : Bounded C} (φ : K ⟶ L) : (ιMapTriangleMappingConeTriangleIso φ).inv.hom₂ = CategoryTheory.CategoryStruct.id L.obj

@[simp]

theorem CochainComplex.Bounded.ιMapTriangleMappingConeTriangleIso_hom_hom₂ {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasBinaryBiproducts C] {K L : Bounded C} (φ : K ⟶ L) : (ιMapTriangleMappingConeTriangleIso φ).hom.hom₂ = CategoryTheory.CategoryStruct.id L.obj

@[simp]

theorem CochainComplex.Bounded.ιMapTriangleMappingConeTriangleIso_hom_hom₁ {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasBinaryBiproducts C] {K L : Bounded C} (φ : K ⟶ L) : (ιMapTriangleMappingConeTriangleIso φ).hom.hom₁ = CategoryTheory.CategoryStruct.id K.obj

@[simp]

theorem CochainComplex.Bounded.ιMapTriangleMappingConeTriangleIso_hom_hom₃ {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasBinaryBiproducts C] {K L : Bounded C} (φ : K ⟶ L) : (ιMapTriangleMappingConeTriangleIso φ).hom.hom₃ = CategoryTheory.CategoryStruct.id (CochainComplex.mappingCone φ.hom)

@[simp]

theorem CochainComplex.Bounded.ιMapTriangleMappingConeTriangleIso_inv_hom₁ {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasBinaryBiproducts C] {K L : Bounded C} (φ : K ⟶ L) : (ιMapTriangleMappingConeTriangleIso φ).inv.hom₁ = CategoryTheory.CategoryStruct.id K.obj

theorem TauCeti.HomotopyCategory.Bounded.quotient_mapTriangle_mappingConeTriangle_mem_distTriang {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasBinaryBiproducts C] [CategoryTheory.Limits.HasZeroObject C] {K L : CochainComplex.Bounded C} (φ : K ⟶ L) : (quotient C).mapTriangle.obj (CochainComplex.Bounded.mappingConeTriangle φ) ∈ CategoryTheory.Pretriangulated.distinguishedTriangles

The image in the bounded homotopy category of the mapping-cone triangle of a morphism of bounded complexes is distinguished.

theorem TauCeti.HomotopyCategory.Bounded.mem_distTriang_iff {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasBinaryBiproducts C] [CategoryTheory.Limits.HasZeroObject C] (T : CategoryTheory.Pretriangulated.Triangle (Bounded C)) : T ∈ CategoryTheory.Pretriangulated.distinguishedTriangles ↔ ∃ (K : CochainComplex.Bounded C) (L : CochainComplex.Bounded C) (φ : K ⟶ L), Nonempty (T ≅ (quotient C).mapTriangle.obj (CochainComplex.Bounded.mappingConeTriangle φ))

A triangle in the bounded homotopy category is distinguished exactly when it is isomorphic to the image of the mapping-cone triangle of a morphism of bounded complexes.

theorem TauCeti.HomotopyCategory.Bounded.isTriangulated_of_mappingConeTriangle {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasBinaryBiproducts C] [CategoryTheory.Limits.HasZeroObject C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] [CategoryTheory.Limits.HasZeroObject D] [CategoryTheory.Preadditive D] [CategoryTheory.HasShift D ℤ] [∀ (n : ℤ), (CategoryTheory.shiftFunctor D n).Additive] [CategoryTheory.Pretriangulated D] (F : CategoryTheory.Functor (Bounded C) D) [F.CommShift ℤ] (hF : ∀ {K L : CochainComplex.Bounded C} (φ : K ⟶ L), F.mapTriangle.obj ((quotient C).mapTriangle.obj (CochainComplex.Bounded.mappingConeTriangle φ)) ∈ CategoryTheory.Pretriangulated.distinguishedTriangles) : F.IsTriangulated

A functor out of the bounded homotopy category which commutes with the shift is a triangle functor when it sends the image of the mapping-cone triangle of every morphism of bounded complexes to a distinguished triangle.