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: if the source has bounds (a₁, b₁) and the target has bounds (a₂, b₂), the standard mapping cone has bounds (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.

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.

Equations

• CochainComplex.bounded C K = (CochainComplex.plus C K ∧ ∃ (b : ℤ), K.IsStrictlyLE b)

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

The elementwise characterization of a bounded cochain complex.

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.

Equations

• CochainComplex.Bounded C = (CochainComplex.bounded C).FullSubcategory

@[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.

Equations

• CochainComplex.Bounded.ι C = (CochainComplex.bounded C).ι

@[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.

Equations

• CochainComplex.Bounded.fullyFaithfulι C = (CochainComplex.bounded C).fullyFaithfulι

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.

Equations

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

@[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

@[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.

Equations

• TauCeti.HomotopyCategory.Bounded C = (TauCeti.HomotopyCategory.bounded C).FullSubcategory

@[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.

Equations

• TauCeti.HomotopyCategory.Bounded.ι C = (TauCeti.HomotopyCategory.bounded C).ι

@[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.

Equations

• TauCeti.HomotopyCategory.Bounded.fullyFaithfulι C = (TauCeti.HomotopyCategory.bounded C).fullyFaithfulι

@[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.

Equations

• TauCeti.HomotopyCategory.Bounded.quotient C = (TauCeti.HomotopyCategory.bounded C).lift ((CochainComplex.Bounded.ι C).comp (HomotopyCategory.quotient C (ComplexShape.up ℤ))) ⋯

@[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.

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.

Equations

• TauCeti.HomotopyCategory.Bounded.quotientCompιIso C = TauCeti.HomotopyCategory.Bounded.quotientCompιIsoAux✝ C

@[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 ℤ

Equations

• TauCeti.HomotopyCategory.Bounded.instCommShiftBoundedQuotientInt C = CategoryTheory.Functor.CommShift.ofComp (TauCeti.HomotopyCategory.Bounded.quotientCompιIso C) ℤ

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

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.

Equations

• One or more equations did not get rendered due to their size.

@[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.

Equations

• TauCeti.HomotopyCategory.Bounded.singleFunctor C n = (TauCeti.HomotopyCategory.Bounded.singleFunctors C).functor n

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 ℤ).

Equations

• One or more equations did not get rendered due to their size.

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