Compact generation in triangulated categories #
This file supplies the large-category vocabulary used in Appendix A.2 of
arXiv:2607.28411v1. Mathlib has cardinal-presentable objects and the finite
triangulated envelope, but it does not yet contain the triangulated notion of
a compact object or the coproduct-and-extension closure Coprod(G).
The definitions here follow A.9--A.11 literally:
Functor.PreservesSmallCoproductsandIsCompactObject(A.9, A.10) begin in the preadditive compact-object layer, while their thick-subcategory structure lives inCategoryTheory/Triangulated/CompactObject.lean, which this file imports;ObjectProperty.coprodClosureis the smallest isomorphism-, coproduct-, and extension-closed object property containing its generators;ObjectProperty.coprodClosure_le_shift_of_le_shifttransports that closure into a shift of another property, whichcoprodClosure_map_objcannot do because Mathlib installs noCommShiftinstance onshiftFunctor C n;TStructure.IsCompactlyGeneratedByrecords compact generation of an already constructed t-structure.
Theorem A.13, which constructs a t-structure from compact generators, is not
smuggled into a typeclass or a global existence hypothesis here. Its
constructive Brown-tower proof lives in CompactlyGenerated.Brown, with the
smallness, local-smallness, coproduct, compactness, and shift-closure
hypotheses stated explicitly.
Definition A.11's Coprod(P): the smallest full subcategory containing
P and closed under isomorphisms, small coproducts, and extensions.
The coproduct constructor is phrased using an arbitrary colimit presentation,
not a chosen ∐, so its universal property does not depend on implementation
choices for colimits.
- of_mem {C : Type u} [Category.{v, u} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] {P : ObjectProperty C} (X : C) (hX : P X) : P.coprodClosure X
- of_iso {C : Type u} [Category.{v, u} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] {P : ObjectProperty C} {X Y : C} (e : X ≅ Y) (hX : P.coprodClosure X) : P.coprodClosure Y
- of_coproduct {C : Type u} [Category.{v, u} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] {P : ObjectProperty C} {ι : Type w} {F : Functor (Discrete ι) C} (c : Limits.Cocone F) (hc : Limits.IsColimit c) (hF : ∀ (i : Discrete ι), P.coprodClosure (F.obj i)) : P.coprodClosure c.pt
- of_extension {C : Type u} [Category.{v, u} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] {P : ObjectProperty C} (T : Pretriangulated.Triangle C) (hT : T ∈ Pretriangulated.distinguishedTriangles) (h₁ : P.coprodClosure T.obj₁) (h₃ : P.coprodClosure T.obj₃) : P.coprodClosure T.obj₂
Instances For
Every generator belongs to its coproduct-and-extension closure.
Universal property of coprodClosure: it is the smallest property with
the three closure properties in Definition A.11.
Universal property of coprodClosure across a shift: a shift-compatible
containment of generators induces one of closures.
The target is a shift of a different property, which is what distinguishes
this from coprodClosure_le_shift in CompactlyGenerated/Existence.lean: that
one is the homogeneous statement G ≤ G.shift 1 → Coprod(G) ≤ Coprod(G).shift 1
(Remark A.12(1)), while the aisles this one compares sit at two different
phases.
It is coprodClosure_le at Q := R.shift n, which cannot be invoked
directly: Mathlib carries (R.shift n).IsClosedUnderIsomorphisms but neither
(R.shift n).IsClosedUnderColimitsOfShape (Discrete ι) nor
(R.shift n).IsTriangulatedClosed₂, so the induction is run by hand.
coprodClosure_map_obj is also unavailable, for a library reason rather than a
mathematical one: Mathlib registers no CommShift ℤ instance on
shiftFunctor C n. Three rotations of a distinguished triangle return the
shift with all three morphisms negated (Triangle.shiftFunctor carries
n.negOnePow), so only a sign-corrected commutation isomorphism makes the
shift triangulated, and none is installed. The signs land on the morphisms,
and coprodClosure constrains only the objects of the triangle in its
extension constructor, so Triangle.shift_distinguished is enough.
The coproduct-and-extension closure of a triangulated object property is again triangulated.
The extension and isomorphism clauses are built into coprodClosure. Shift
closure follows by applying coprodClosure_le_shift_of_le_shift to the
shift-stability of the generators.
A coproduct-preserving triangulated functor carries Coprod(P) into
Coprod(F(P)). This is the closure argument used in Step 1 of A.17.
A coproduct-preserving triangulated functor carries Coprod(P) into
Coprod(Q) as soon as the images of the generators P lie in
Coprod(Q).
Property-level form of coprodClosure_map_obj_of_le.
Inverse-image form of coprodClosure_map_obj_of_le, matching the
object-property inequality used to restrict a functor to full
subcategories.
Definition A.11: t is compactly generated by G when the generators
are compact and its aisle is exactly Coprod(G).
Instances For
A generator of a compactly generated t-structure lies in its aisle.
A coproduct-preserving triangulated functor which sends compact generators into the target aisle is right t-exact.
This is Lemma A.16(1) and the right-t-exact half of Step 1 in A.17, isolated from the geometric setting.
Step 1 of A.17 after the A.13 t-structure has been constructed.
If tD is generated by G, tC is generated by its left-adjoint image,
F preserves coproducts, and the monad L ⋙ F is right t-exact, then F
is t-exact. The proof follows the paper: L is right t-exact by generation,
so its right adjoint F is left t-exact; the monad condition sends the source
generators into the target aisle, giving right t-exactness by closure.
The premise is an actually constructed tC with a proved aisle formula, not
a global proposition asserting Theorem A.13 or A.17.