The bounded homotopy category `Kᵇ(C)` #

Mathlib has HomotopyCategory.Plus C, the triangulated full subcategory of HomotopyCategory C (.up ℤ) on bounded-below cochain complexes, but no bounded analogue. This file supplies it: HomotopyCategory.Bounded C is the full subcategory on complexes that are strictly bounded on both sides, with the same three subcategory instances (ContainsZero, IsStableUnderShift, IsTriangulated) proved the same way, so Mathlib's generic machinery makes it pretriangulated.

ForMathlib #

Everything here is stated for a general preadditive C with binary biproducts and mirrors Mathlib.Algebra.Homology.HomotopyCategory.Plus declaration by declaration; it is upstreamable as written. Filed in place, following the repository's ForMathlib pattern.

The repository's use is as substrate for a HomFiniteBounded witness (#543): Kᵇ of a Hom-finite linear category is Hom-finite with finite Ext-amplitude by inspection of components, with no localization Homs to compute. Nothing here mentions that; this file is category plumbing only.

source

def CochainComplex.bounded (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] :

CategoryTheory.ObjectProperty (CochainComplex C ℤ)

A cochain complex is bounded when it is strictly bounded on both sides.

Equations

CochainComplex.bounded C K = ((∃ (n : ℤ), K.IsStrictlyGE n) ∧ ∃ (n : ℤ), K.IsStrictlyLE n)

Instances For

source

theorem CochainComplex.bounded_iff {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] (K : CochainComplex C ℤ) :

CochainComplex.bounded C K ↔ (∃ (n : ℤ), K.IsStrictlyGE n) ∧ ∃ (n : ℤ), K.IsStrictlyLE n

source

theorem CochainComplex.isStrictlyLE_mappingCone {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasBinaryBiproducts C] {K L : CochainComplex C ℤ} (f : K ⟶ L) (n₁ n₂ n : ℤ) [K.IsStrictlyLE n₁] [L.IsStrictlyLE n₂] (hn₁ : n₁ ≤ n + 1 := by lia) (hn₂ : n₂ ≤ n := by lia) :

(mappingCone f).IsStrictlyLE n

The mapping cone of a map of complexes that are strictly bounded above is strictly bounded above; the companion of isStrictlyGE_mappingCone.

source

def HomotopyCategory.bounded (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] :

CategoryTheory.ObjectProperty (HomotopyCategory C (ComplexShape.up ℤ))

The property of objects in HomotopyCategory C (.up ℤ) whose underlying cochain complex is bounded on both sides. (Like HomotopyCategory.plus, this property of objects is not closed under isomorphisms.)

Equations

HomotopyCategory.bounded C = (CochainComplex.bounded C).strictMap (HomotopyCategory.quotient C (ComplexShape.up ℤ))

Instances For

source

@[simp]

theorem HomotopyCategory.bounded_quotient_obj_iff {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] (K : CochainComplex C ℤ) :

bounded C ((quotient C (ComplexShape.up ℤ)).obj K) ↔ CochainComplex.bounded C K

source

theorem HomotopyCategory.bounded_iff_exists {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] (X : HomotopyCategory C (ComplexShape.up ℤ)) :

bounded C X ↔ ∃ (K : CochainComplex C ℤ), CochainComplex.bounded C K ∧ (quotient C (ComplexShape.up ℤ)).obj K = X

Unfold the strictMap inductive into the existential a consumer can obtain from; dependent elimination on strictMap itself fails whenever the index is not already a literal (quotient _ _).obj K.

source