The homotopy category of bounded cochain complexes

This file constructs the full pretriangulated subcategory of the homotopy category whose objects are represented by cochain complexes vanishing outside a finite interval. It also constructs the quotient functor from bounded cochain complexes and proves that this functor is full and essentially surjective.

The boundedness predicate records both bounds at once. This matters for closure under cones: the mapping cone of a morphism between bounded complexes is bounded (CochainComplex.bounded_mappingCone). The explicit bounds are given by CochainComplex.isStrictlyGE_mappingCone and CochainComplex.isStrictlyLE_mappingCone: if the source has bounds (a₁, b₁) and the target has bounds (a₂, b₂), the cone is strictly bounded by (min (a₁ - 1) a₂, max (b₁ - 1) b₂). Consequently the full subcategory is stable under shifts and distinguished triangles.

The construction follows the organization of Mathlib's bounded-below category HomotopyCategory.Plus, replacing its one-sided support condition by two-sided boundedness.

Main definitions

• CochainComplex.bounded: the property of being strictly bounded above and below.
• CochainComplex.Bounded: the full subcategory of bounded cochain complexes.
• TauCeti.HomotopyCategory.bounded: the corresponding property in the homotopy category.
• TauCeti.HomotopyCategory.Bounded: the homotopy category of bounded cochain complexes.
• TauCeti.HomotopyCategory.Bounded.quotient: the quotient functor from bounded complexes. It is a localization functor with respect to the homotopy equivalences, so functors and their shift compatibilities descend along it.
• TauCeti.HomotopyCategory.Bounded.rep: the underlying cochain complex of an object of the bounded homotopy category.
• TauCeti.HomotopyCategory.Bounded.quotientCompιIso: the bounded quotient followed by the inclusion agrees with the ordinary homotopy quotient.
• TauCeti.HomotopyCategory.Bounded.singleFunctors: the single functors C ⥤ HomotopyCategory.Bounded C with their shift compatibilities, with singleFunctor the functor in degree n and singleFunctorCompιIso its comparison with HomotopyCategory.singleFunctor.

The homotopy category of bounded complexes over an essentially small category is essentially small (through HomotopyCategory.essentiallySmall and CategoryTheory.ObjectProperty.essentiallySmall_of_ambient), so it has a triangulated Grothendieck group.

References

• Mathlib's Mathlib/Algebra/Homology/HomotopyCategory/Plus.lean, whose construction of the bounded-below homotopy category supplies the formal pattern used here.
• Charles A. Weibel, The K-book: An Introduction to Algebraic K-theory, Chapter II, Exercise 9.15.

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 both below and above: the meet of Mathlib's CochainComplex.plus and CochainComplex.minus.

theorem CochainComplex.bounded_iff (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] (K : CochainComplex C ℤ) : bounded C K ↔ ∃ (a : ℤ) (b : ℤ), K.IsStrictlyGE a ∧ K.IsStrictlyLE b

A cochain complex is bounded iff it is strictly bounded below by some a and strictly bounded above by some b.

theorem CochainComplex.bounded_iff_exists_finset_isZero_X (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] (K : CochainComplex C ℤ) : bounded C K ↔ ∃ (s : Finset ℤ), ∀ n ∉ s, CategoryTheory.Limits.IsZero (K.X n)

A cochain complex is bounded exactly when it vanishes outside a finite set of degrees.

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

instance CochainComplex.instIsStableUnderShiftIntBounded (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] : (bounded C).IsStableUnderShift ℤ

@[reducible, inline]

abbrev CochainComplex.Bounded (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] : Type (max u v)

The full subcategory of bounded cochain complexes.

theorem CochainComplex.bounded_cylinder {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasBinaryBiproducts C] {K : CochainComplex C ℤ} (hK : bounded C K) : bounded C (HomologicalComplex.cylinder K)

The cylinder of a bounded cochain complex is bounded.

theorem CochainComplex.isStrictlyLE_mappingCone {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {K L : CochainComplex C ℤ} (f : K ⟶ L) [HomologicalComplex.HasHomotopyCofiber f] (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 morphism K ⟶ L is strictly bounded above by n when K is strictly bounded above by n + 1 and L by n. This is the upper-bound counterpart of Mathlib's CochainComplex.isStrictlyGE_mappingCone.

theorem CochainComplex.bounded_mappingCone {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasBinaryBiproducts C] {K L : CochainComplex C ℤ} (f : K ⟶ L) (hK : bounded C K) (hL : bounded C L) : bounded C (mappingCone f)

The mapping cone of a morphism between bounded cochain complexes is bounded. The explicit bounds are given by CochainComplex.isStrictlyGE_mappingCone and isStrictlyLE_mappingCone.

@[reducible, inline]

abbrev CochainComplex.Bounded.ι (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] : CategoryTheory.Functor (Bounded C) (CochainComplex C ℤ)

The inclusion of bounded cochain complexes into all cochain complexes.

@[reducible, inline]

abbrev CochainComplex.Bounded.fullyFaithfulι (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] : (ι C).FullyFaithful

The inclusion of bounded cochain complexes is fully faithful.

def TauCeti.HomotopyCategory.bounded (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] : CategoryTheory.ObjectProperty (HomotopyCategory C (ComplexShape.up ℤ))

The property of objects of the homotopy category which are represented by bounded cochain complexes. As for Mathlib's HomotopyCategory.plus, the representative is remembered strictly; the induced full subcategory is nevertheless closed under the pretriangulated operations.

@[simp]

theorem TauCeti.HomotopyCategory.bounded_quotient_obj_iff {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] (K : CochainComplex C ℤ) : bounded C ((HomotopyCategory.quotient C (ComplexShape.up ℤ)).obj K) ↔ CochainComplex.bounded C K

The ordinary homotopy quotient of a cochain complex is bounded exactly when the complex itself is bounded.

instance TauCeti.HomotopyCategory.instContainsZeroHomotopyCategoryIntUpBoundedOfHasZeroObject (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] : (bounded C).ContainsZero

instance TauCeti.HomotopyCategory.instIsStableUnderShiftHomotopyCategoryIntUpBounded (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] : (bounded C).IsStableUnderShift ℤ

instance TauCeti.HomotopyCategory.instIsTriangulatedClosed₃HomotopyCategoryIntUpBounded (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] : (bounded C).IsTriangulatedClosed₃

instance TauCeti.HomotopyCategory.instIsTriangulatedHomotopyCategoryIntUpBounded (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] : (bounded C).IsTriangulated

theorem TauCeti.HomotopyCategory.bounded_le_plus (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] : bounded C ≤ HomotopyCategory.plus C

Every object of the homotopy category represented by a bounded complex is represented by a bounded below complex.

@[reducible, inline]

abbrev TauCeti.HomotopyCategory.Bounded (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] : Type (max u v)

The homotopy category of bounded cochain complexes.

@[reducible, inline]

abbrev TauCeti.HomotopyCategory.Bounded.ι (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] : CategoryTheory.Functor (Bounded C) (HomotopyCategory C (ComplexShape.up ℤ))

The inclusion of the bounded homotopy category into the homotopy category of all cochain complexes.

@[reducible, inline]

abbrev TauCeti.HomotopyCategory.Bounded.fullyFaithfulι (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] : (ι C).FullyFaithful

The inclusion of the bounded homotopy category is fully faithful.

def TauCeti.HomotopyCategory.Bounded.rep {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] (K : Bounded C) : CochainComplex C ℤ

The bounded cochain complex underlying an object of the bounded homotopy category.

@[simp]

theorem TauCeti.HomotopyCategory.Bounded.quotient_obj_rep {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] (K : Bounded C) : (HomotopyCategory.quotient C (ComplexShape.up ℤ)).obj K.rep = K.obj

An object of the bounded homotopy category is the homotopy class of its underlying complex.

theorem TauCeti.HomotopyCategory.Bounded.bounded_rep {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] (K : Bounded C) : CochainComplex.bounded C K.rep

The underlying complex of an object of the bounded homotopy category is bounded.

@[implicit_reducible]

def TauCeti.HomotopyCategory.Bounded.quotient (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] : CategoryTheory.Functor (CochainComplex.Bounded C) (Bounded C)

The quotient functor from bounded cochain complexes to their bounded homotopy category.

@[simp]

theorem TauCeti.HomotopyCategory.Bounded.quotient_obj_obj (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] (X : CochainComplex.Bounded C) : ((quotient C).obj X).obj = (HomotopyCategory.quotient C (ComplexShape.up ℤ)).obj X.obj

Inclusion sends a bounded quotient object to the ordinary homotopy quotient.

@[simp]

theorem TauCeti.HomotopyCategory.Bounded.quotient_map_hom (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {X Y : CochainComplex.Bounded C} (f : X ⟶ Y) : ((quotient C).map f).hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (CategoryTheory.CategoryStruct.comp ((HomotopyCategory.quotient C (ComplexShape.up ℤ)).map f.hom) (CategoryTheory.eqToHom ⋯))

The bounded quotient acts on maps by the ordinary homotopy quotient, after transporting along the object comparison equalities.

theorem TauCeti.HomotopyCategory.Bounded.quotient_obj_rep_quotient_obj {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] (K : CochainComplex.Bounded C) : (HomotopyCategory.quotient C (ComplexShape.up ℤ)).obj ((quotient C).obj K).rep = (HomotopyCategory.quotient C (ComplexShape.up ℤ)).obj K.obj

The underlying complex of the class of a bounded complex has the same homotopy class as that complex.

def TauCeti.HomotopyCategory.Bounded.quotientCompιIso (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] : (quotient C).comp (ι C) ≅ (CochainComplex.Bounded.ι C).comp (HomotopyCategory.quotient C (ComplexShape.up ℤ))

The bounded quotient followed by the inclusion agrees with the ordinary homotopy quotient.

@[simp]

theorem TauCeti.HomotopyCategory.Bounded.quotientCompιIso_hom_app (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] (X : CochainComplex.Bounded C) : (quotientCompιIso C).hom.app X = CategoryTheory.eqToHom ⋯

The comparison isomorphism has the canonical component at each bounded complex.

@[simp]

theorem TauCeti.HomotopyCategory.Bounded.quotientCompιIso_inv_app (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] (X : CochainComplex.Bounded C) : (quotientCompιIso C).inv.app X = CategoryTheory.eqToHom ⋯

The inverse comparison has the reverse canonical component at each bounded complex.

@[instance_reducible]

noncomputable instance TauCeti.HomotopyCategory.Bounded.instCommShiftBoundedQuotientInt (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] : (quotient C).CommShift ℤ

instance TauCeti.HomotopyCategory.Bounded.instCommShiftBoundedHomotopyCategoryIntUpHomFunctorQuotientCompιIso (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] : CategoryTheory.NatTrans.CommShift (quotientCompιIso C).hom ℤ

theorem TauCeti.HomotopyCategory.Bounded.quotient_obj_surjective {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] : Function.Surjective (quotient C).obj

Every bounded homotopy object is represented by a bounded cochain complex.

instance TauCeti.HomotopyCategory.Bounded.instEssSurjBoundedQuotient {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] : (quotient C).EssSurj

instance TauCeti.HomotopyCategory.Bounded.instFullBoundedQuotient {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] : (quotient C).Full

instance TauCeti.HomotopyCategory.Bounded.instIsLocalizationBoundedQuotientInverseImageHomologicalComplexIntUpHomotopyEquivalencesιOfHasBinaryBiproducts (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasBinaryBiproducts C] : (quotient C).IsLocalization ((HomologicalComplex.homotopyEquivalences C (ComplexShape.up ℤ)).inverseImage (CochainComplex.Bounded.ι C))

The quotient functor from bounded cochain complexes is a localization functor with respect to the homotopy equivalences. This is the bounded analogue of Mathlib's corresponding instance for HomotopyCategory.Plus.quotient.

noncomputable def TauCeti.HomotopyCategory.Bounded.singleFunctors (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] : CategoryTheory.SingleFunctors C (Bounded C) ℤ

The collection of all single functors C ⥤ HomotopyCategory.Bounded C for n : ℤ, along with their compatibilities with shifts.

@[reducible, inline]

noncomputable abbrev TauCeti.HomotopyCategory.Bounded.singleFunctor (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] (n : ℤ) : CategoryTheory.Functor C (Bounded C)

The single functor C ⥤ HomotopyCategory.Bounded C.

noncomputable def TauCeti.HomotopyCategory.Bounded.singleFunctorCompιIso (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] (n : ℤ) : (singleFunctor C n).comp (ι C) ≅ HomotopyCategory.singleFunctor C n

The bounded single functor is induced by HomotopyCategory.singleFunctor C n : C ⥤ HomotopyCategory C (.up ℤ).

instance TauCeti.HomotopyCategory.Bounded.instAdditiveSingleFunctor (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] (n : ℤ) : (singleFunctor C n).Additive