Bounded complexes are built from their terms

In the bounded homotopy category, a triangulated subcategory closed under isomorphisms which contains the terms of a bounded complex, each placed in degree zero, contains the complex. Splitting off the top term (CochainComplex.topShortComplexSplitting) is a degreewise split short exact sequence, hence a distinguished triangle, and expresses a bounded complex as an extension of a shorter complex by a complex concentrated in one degree; induction on the length concludes.

The induction is adapted from the proof of TauCeti.TriangulatedK0.of_bounded_quotient_obj in TauCeti/CategoryTheory/GrothendieckGroup/BoundedHomotopy/Basic.lean, which splits off the top term in the same way to express the class of a bounded complex in the triangulated Grothendieck group. Both results now use CochainComplex.bounded_induction and TauCeti.HomotopyCategory.Bounded.exists_distTriang_top from this file.

Main results

• CochainComplex.bounded_induction: induction on bounded complexes, from zero complexes and by passing from the brutal truncation below the top degree to the complex.
• TauCeti.HomotopyCategory.Bounded.exists_distTriang_top: the distinguished triangle of the bounded homotopy category splitting off the top term of a bounded complex.
• TauCeti.HomotopyCategory.Bounded.prop_quotient_obj: a triangulated subcategory containing every term of a bounded complex in degree zero contains the complex.

theorem CochainComplex.bounded_stupidTrunc_embeddingUpIntLE {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasZeroObject C] {K : CochainComplex C ℤ} (hK : bounded C K) (b : ℤ) : bounded C (HomologicalComplex.stupidTrunc K (ComplexShape.embeddingUpIntLE b))

The brutal truncation of a bounded complex in degrees ≤ b is bounded.

theorem CochainComplex.bounded_induction {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasZeroObject C] {motive : CochainComplex C ℤ → Prop} (zero : ∀ (K : CochainComplex C ℤ), CategoryTheory.Limits.IsZero K → motive K) (step : ∀ (K : CochainComplex C ℤ) (b : ℤ), bounded C K → K.IsStrictlyLE (b + 1) → motive (HomologicalComplex.stupidTrunc K (ComplexShape.embeddingUpIntLE b)) → motive K) (K : CochainComplex C ℤ) (hK : bounded C K) : motive K

Induction on bounded complexes by their top term. A property of cochain complexes that holds for zero complexes, and holds for a bounded complex vanishing above degree b + 1 as soon as it holds for its brutal truncation in degrees ≤ b, holds for every bounded complex.

theorem TauCeti.HomotopyCategory.Bounded.exists_distTriang_top {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasBinaryBiproducts C] [CategoryTheory.Limits.HasZeroObject C] (K : CochainComplex C ℤ) (hK : CochainComplex.bounded C K) (b : ℤ) [K.IsStrictlyLE (b + 1)] : ∃ T ∈ CategoryTheory.Pretriangulated.distinguishedTriangles, Nonempty (T.obj₁ ≅ (singleFunctor C (b + 1)).obj (K.X (b + 1))) ∧ Nonempty (T.obj₂ ≅ (quotient C).obj { obj := K, property := hK }) ∧ Nonempty (T.obj₃ ≅ (quotient C).obj { obj := HomologicalComplex.stupidTrunc K (ComplexShape.embeddingUpIntLE b), property := ⋯ })

Splitting off the top term: for a bounded complex K vanishing above degree b + 1, there is a distinguished triangle of the bounded homotopy category whose vertices are the top term placed in degree b + 1, the complex K, and its brutal truncation in degrees ≤ b.

theorem TauCeti.HomotopyCategory.Bounded.prop_quotient_obj {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasBinaryBiproducts C] [CategoryTheory.Limits.HasZeroObject C] (P : CategoryTheory.ObjectProperty (Bounded C)) [P.IsTriangulated] [P.IsClosedUnderIsomorphisms] (K : CochainComplex.Bounded C) (hK : ∀ (n : ℤ), P ((singleFunctor C 0).obj (K.obj.X n))) : P ((quotient C).obj K)

A bounded complex lies in a triangulated subcategory containing its terms: if a triangulated subcategory of the bounded homotopy category, closed under isomorphisms, contains each term of a bounded complex placed in degree zero, then it contains the complex.