A concrete HomFiniteBounded category (#543)

EulerForm.lean introduced HomFiniteBounded as supplied data and its own docstring recorded that no concrete k-linear pretriangulated category existed in this repository for it to be proved about. This file removes that caveat: the bounded homotopy category Kᵇ(C) of any Hom-finite k-linear additive category C satisfies it, and Kᵇ(FGModuleCat k) — bounded complexes of finite-dimensional vector spaces up to homotopy — is the named concrete witness.

Why the homotopy category and not the derived category

For Dᵇ the finiteness of Hom-spaces is a theorem about the localization. For Kᵇ every statement is elementary: a chain map out of a complex supported in a finite window is determined by finitely many components, each in a Hom-finite Hom-space, and homotopy classes are a quotient of that. So Kᵇ is where the witness is built, and it stands on its own as an honest k-linear pretriangulated category.

The route to Dᵇ does not need the semisimplicity argument (Dᵇ(k‑vect) ≃ ℤ-graded vector spaces) that an earlier reading of #543 took to be the only option. Over a field every bounded complex is K-projective, and CochainComplex.IsKProjective.Qh_map_bijective then says Hom in Dᵇ is Hom in Kᵇ. The Derived section below carries that out: boundedQh is fully faithful, its essential image is a triangulated subcategory of D(FGModuleCat k) and so k-linear pretriangulated, and HomFiniteBounded.of_essSurj moves the Kᵇ instance across.

So HomFiniteBounded now has a model on a genuine derived category, and no equivalence Dᵇ(k-vect) ≃ ℤ-graded vector spaces is constructed anywhere.

What this file proves and what it does not

• CochainComplex.module_finite_hom: a chain-map space out of a strictly bounded complex is a finite k-module when C is Hom-finite. No bound on the target is needed.
• subsingleton_hom_of_le_lt_ge / ..of_ge_lt_le: chain maps between complexes with disjoint support windows vanish.
• instHomFiniteBoundedBounded: Kᵇ(C) satisfies HomFiniteBounded k for Hom-finite k-linear C; homFiniteBounded_fgModuleCat instantiates it at C := FGModuleCat k.
• FGModuleCat.instProjective: every finite-dimensional vector space is a projective object. Mathlib has this for ModuleCat but not for FGModuleCat, and instance search does not find it unaided — it is an upstream candidate.
• isKProjective_of_isStrictlyLE: a bounded-above complex of finite-dimensional vector spaces is K-projective, with no hypothesis beyond the bound.
• homFiniteBounded_boundedDerived: HomFiniteBounded k on the essential image of boundedQh — a full subcategory of DerivedCategory (FGModuleCat k), k-linear pretriangulated. This is the honest Dᵇ witness #543 asked for.
• Not proved: that this essential image is all of the bounded derived category — it is defined as an image, and no t-structure characterisation of it is given. Nor any comparison of chiHom with an Euler characteristic of homology, nor IsRiemannRoch for anything. The obligation #513 named is discharged in the satisfiability sense only: the class has a genuine model, so the Euler-form chain is not vacuous.

def CategoryTheory.Triangulated.HomFiniteWitness.homRestrict (k : Type w) [DivisionRing k] {C : Type u} [Category.{v, u} C] [Preadditive C] [Linear k C] (K L : CochainComplex C ℤ) (s : Finset ℤ) : (K ⟶ L) →ₗ[k] (i : ↥s) → K.X ↑i ⟶ L.X ↑i

Restriction of a chain map to its components in a finite window, as a linear map.

Equations

• CategoryTheory.Triangulated.HomFiniteWitness.homRestrict k K L s = { toFun := fun (f : K ⟶ L) (i : ↥s) => f.f ↑i, map_add' := ⋯, map_smul' := ⋯ }

theorem CategoryTheory.Triangulated.HomFiniteWitness.module_finite_hom (k : Type w) [DivisionRing k] {C : Type u} [Category.{v, u} C] [Preadditive C] [Linear k C] [∀ (X Y : C), Module.Finite k (X ⟶ Y)] (K L : CochainComplex C ℤ) (a b : ℤ) [K.IsStrictlyGE a] [K.IsStrictlyLE b] : Module.Finite k (K ⟶ L)

A chain-map space out of a strictly bounded complex is a finite k-module when the base category is Hom-finite. The target complex needs no bound.

theorem CategoryTheory.Triangulated.HomFiniteWitness.subsingleton_hom_of_le_lt_ge {C : Type u} [Category.{v, u} C] [Preadditive C] (K L : CochainComplex C ℤ) (b c : ℤ) [K.IsStrictlyLE b] [L.IsStrictlyGE c] (h : b < c) : Subsingleton (K ⟶ L)

Chain maps from a complex bounded above into one bounded strictly below it vanish.

theorem CategoryTheory.Triangulated.HomFiniteWitness.subsingleton_hom_of_ge_lt_le {C : Type u} [Category.{v, u} C] [Preadditive C] (K L : CochainComplex C ℤ) (a d : ℤ) [K.IsStrictlyGE a] [L.IsStrictlyLE d] (h : d < a) : Subsingleton (K ⟶ L)

Chain maps from a complex bounded below into one bounded strictly above it vanish.

noncomputable def CategoryTheory.Triangulated.HomFiniteWitness.boundedHomEquiv (k : Type w) [DivisionRing k] {C : Type u} [Category.{v, u} C] [Preadditive C] [Linear k C] (X Y : HomotopyCategory.Bounded C) (i : ℤ) {KX KY : CochainComplex C ℤ} (hX : (HomotopyCategory.quotient C (ComplexShape.up ℤ)).obj KX = X.obj) (hY : (HomotopyCategory.quotient C (ComplexShape.up ℤ)).obj KY = Y.obj) : (X ⟶ (shiftFunctor (HomotopyCategory.Bounded C) i).obj Y) ≃ₗ[k] (HomotopyCategory.quotient C (ComplexShape.up ℤ)).obj KX ⟶ (HomotopyCategory.quotient C (ComplexShape.up ℤ)).obj ((shiftFunctor (HomologicalComplex C (ComplexShape.up ℤ)) i).obj KY)

The hom-space X ⟶ Y⟦i⟧ in Kᵇ(C), identified k-linearly with a hom-space between quotient images of honest complexes, along the two inclusion/quotient CommShift isomorphisms and the defining equalities of the boundedness property. Both instance fields below factor through this.

Equations

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

instance CategoryTheory.Triangulated.instHomFiniteBoundedBounded (k : Type w) [DivisionRing k] {C : Type u} [Category.{v, u} C] [Preadditive C] [Linear k C] [∀ (X Y : C), Module.Finite k (X ⟶ Y)] : HomFiniteBounded k (HomotopyCategory.Bounded C)

Kᵇ of a Hom-finite linear category is HomFiniteBounded. Every hom-space is a quotient of a chain-map space out of a bounded complex, and disjoint support windows kill all chain maps once the shift is large.

instance CategoryTheory.Triangulated.fgModuleCat_hom_finite (k : Type u) [Field k] (V W : FGModuleCat k) : Module.Finite k (V ⟶ W)

theorem CategoryTheory.Triangulated.homFiniteBounded_fgModuleCat (k : Type u) [Field k] : HomFiniteBounded k (HomotopyCategory.Bounded (FGModuleCat k))

The named concrete witness for #543: bounded complexes of finite-dimensional k-vector spaces up to homotopy form a k-linear pretriangulated category with finite-dimensional Hom-spaces and finite Ext-amplitude. The Euler-form chain of EulerForm.lean is therefore not vacuous: HomFiniteBounded has a model.

instance FGModuleCat.instProjective (k : Type u) [Field k] (V : FGModuleCat k) : CategoryTheory.Projective V

Every finite-dimensional vector space is a projective object.

Over a field every module is free, hence Module.Projective, and ModuleCat.projective_of_categoryTheory_projective turns that into categorical projectivity in ModuleCat k. The step this instance adds is descending it along forget₂, which is full, faithful and epimorphism- preserving, so Functor.projective_of_map_projective applies.

Instance search does not find this chain on its own — it times out at the default heartbeat budget — which is why the instance is written down rather than left implicit. Mathlib has no Projective result anywhere under Algebra/Category/FGModuleCat/; this is an upstream candidate.

theorem CategoryTheory.Triangulated.isKProjective_of_isStrictlyLE (k : Type u) [Field k] (K : CochainComplex (FGModuleCat k) ℤ) (d : ℤ) [K.IsStrictlyLE d] : K.IsKProjective

A bounded-above complex of finite-dimensional vector spaces is K-projective.

CochainComplex.isKProjective_of_projective asks for a bound above and degreewise projectivity; over a field the second hypothesis is free by FGModuleCat.instProjective, so only the bound survives.

This is the input to CochainComplex.IsKProjective.Qh_map_bijective, which is what would carry instHomFiniteBoundedBounded across to a derived category. That transport is not performed here.

instance CategoryTheory.Triangulated.isKProjective_bounded (k : Type u) [Field k] (X : HomotopyCategory.Bounded (FGModuleCat k)) : CochainComplex.IsKProjective X.obj.as

Every object of Kᵇ(FGModuleCat k) is K-projective. Boundedness supplies the bound above; FGModuleCat.instProjective supplies the rest.

@[reducible, inline]

noncomputable abbrev CategoryTheory.Triangulated.boundedQh (k : Type u) [Field k] : Functor (HomotopyCategory.Bounded (FGModuleCat k)) (DerivedCategory (FGModuleCat k))

Kᵇ(FGModuleCat k) ⥤ D(FGModuleCat k).

An abbrev deliberately: as a def the composite is opaque to instance search, and every structural instance below — CommShift, IsTriangulated, Additive, Linear — is found by unfolding it.

Equations

• CategoryTheory.Triangulated.boundedQh k = (HomotopyCategory.Bounded.ι (FGModuleCat k)).comp DerivedCategory.Qh

instance CategoryTheory.Triangulated.boundedQh_full (k : Type u) [Field k] : (boundedQh k).Full

Full, because a K-projective source makes Qh bijective on Hom.

instance CategoryTheory.Triangulated.boundedQh_faithful (k : Type u) [Field k] : (boundedQh k).Faithful

Faithful, by the injective half of the same bijection.

@[reducible, inline]

noncomputable abbrev CategoryTheory.Triangulated.boundedLift (k : Type u) [Field k] : Functor (HomotopyCategory.Bounded (FGModuleCat k)) (boundedQh k).essImage.FullSubcategory

The bounded derived locus: the essential image of boundedQh, as a full subcategory of D(FGModuleCat k).

It is k-linear pretriangulated for free. Mathlib's ObjectProperty.essImage.IsTriangulated makes the essential image of a full triangulated functor a triangulated subcategory, and ObjectProperty.instPretriangulatedFullSubcategory equips the full subcategory of a triangulated subcategory. Nothing here has to build a t-structure.

Equations

• CategoryTheory.Triangulated.boundedLift k = (CategoryTheory.Triangulated.boundedQh k).essImage.lift (CategoryTheory.Triangulated.boundedQh k) ⋯

instance CategoryTheory.Triangulated.boundedLift_linear (k : Type u) [Field k] : Functor.Linear k (boundedLift k)

instance CategoryTheory.Triangulated.boundedLift_essSurj (k : Type u) [Field k] : (boundedLift k).EssSurj

instance CategoryTheory.Triangulated.homFiniteBounded_boundedDerived (k : Type u) [Field k] : HomFiniteBounded k (boundedQh k).essImage.FullSubcategory

The Dᵇ witness for #543.

HomFiniteBounded holds on a full subcategory of a genuine derived category, not merely on a homotopy category. The route is the one HomFiniteWitness's docstring describes: bounded complexes of finite-dimensional vector spaces are K-projective, so Qh is fully faithful on them, and HomFiniteBounded.of_essSurj carries the Kᵇ instance across.

Semisimplicity is not used, and no equivalence Dᵇ(k-vect) ≃ ℤ-graded vector spaces is constructed or needed.