Compact objects in a preadditive category

The vocabulary of Appendix A.2 of arXiv:2607.28411v1 that needs no triangulated structure, following A.9 and A.10 literally:

• Functor.PreservesSmallCoproducts means preservation of all coproducts indexed in a fixed universe;
• IsCompactObject means that Hom(K, -) preserves those coproducts;
• ObjectProperty.compactObjects is the resulting object property, closed under isomorphisms;
• a left adjoint to a small-coproduct-preserving functor carries compact objects to compact objects.

The coproduct-and-extension closure Coprod(G) and compactly generated t-structures need distinguished triangles and live in CategoryTheory/Triangulated/CompactlyGenerated.lean.

def CategoryTheory.Functor.PreservesSmallCoproducts {C : Type u₁} [Category.{v, u₁} C] {D : Type u₂} [Category.{v, u₂} D] (F : Functor C D) : Prop

A functor preserves the coproducts indexed by types in universe w.

Keeping the indexing universe explicit matches Mathlib's universe-sensitive colimit API and avoids pretending that one category has literally all large-universe coproducts.

Equations

• F.PreservesSmallCoproducts = ∀ (ι : Type ?u.4), CategoryTheory.Limits.PreservesColimitsOfShape (CategoryTheory.Discrete ι) F

def CategoryTheory.IsCompactObject {C : Type u} [Category.{v, u} C] [Preadditive C] (K : C) : Prop

Definition A.9: K is compact when Hom(K, -) preserves all small coproducts in the indexing universe w.

The Hom functor is valued in additive commutative groups, so the colimit on the target side is the direct sum of Hom groups. Using ordinary set-valued coyoneda here would instead form a disjoint union of Hom sets, which is not the triangulated notion of compactness.

Equations

• CategoryTheory.IsCompactObject K = ∀ (ι : Type ?u.3), CategoryTheory.Limits.PreservesColimitsOfShape (CategoryTheory.Discrete ι) (CategoryTheory.preadditiveCoyoneda.obj (Opposite.op K))

noncomputable def CategoryTheory.IsCompactObject.coproductComparisonIso {C : Type u} [Category.{v, u} C] [Preadditive C] {K : C} (hK : IsCompactObject K) {ι : Type w} (X : ι → C) [Limits.HasCoproduct X] [Limits.HasColimit ((Discrete.functor X).comp (preadditiveCoyoneda.obj (Opposite.op K)))] : (preadditiveCoyoneda.obj (Opposite.op K)).obj (∐ X) ≅ Limits.colimit ((Discrete.functor X).comp (preadditiveCoyoneda.obj (Opposite.op K)))

The defining compactness comparison: maps from K into a coproduct form the direct sum of the Hom groups into its summands.

Equations

• hK.coproductComparisonIso X = CategoryTheory.preservesColimitIso (CategoryTheory.preadditiveCoyoneda.obj (Opposite.op K)) (CategoryTheory.Discrete.functor X)

@[simp]

theorem CategoryTheory.IsCompactObject.map_ι_coproductComparisonIso_hom {C : Type u} [Category.{v, u} C] [Preadditive C] {K : C} (hK : IsCompactObject K) {ι : Type w} (X : ι → C) [Limits.HasCoproduct X] [Limits.HasColimit ((Discrete.functor X).comp (preadditiveCoyoneda.obj (Opposite.op K)))] (i : ι) : CategoryStruct.comp ((preadditiveCoyoneda.obj (Opposite.op K)).map (Limits.Sigma.ι X i)) (hK.coproductComparisonIso X).hom = Limits.colimit.ι ((Discrete.functor X).comp (preadditiveCoyoneda.obj (Opposite.op K))) { as := i }

Under the compactness comparison, postcomposition with a coproduct injection is the corresponding direct-sum injection.

@[simp]

theorem CategoryTheory.IsCompactObject.map_ι_coproductComparisonIso_hom_assoc {C : Type u} [Category.{v, u} C] [Preadditive C] {K : C} (hK : IsCompactObject K) {ι : Type w} (X : ι → C) [Limits.HasCoproduct X] [Limits.HasColimit ((Discrete.functor X).comp (preadditiveCoyoneda.obj (Opposite.op K)))] (i : ι) {Z : AddCommGrpCat} (h : Limits.colimit ((Discrete.functor X).comp (preadditiveCoyoneda.obj (Opposite.op K))) ⟶ Z) : CategoryStruct.comp ((preadditiveCoyoneda.obj (Opposite.op K)).map (Limits.Sigma.ι X i)) (CategoryStruct.comp (hK.coproductComparisonIso X).hom h) = CategoryStruct.comp (Limits.colimit.ι ((Discrete.functor X).comp (preadditiveCoyoneda.obj (Opposite.op K))) { as := i }) h

Under the compactness comparison, postcomposition with a coproduct injection is the corresponding direct-sum injection.

def CategoryTheory.ObjectProperty.compactObjects {C : Type u} [Category.{v, u} C] [Preadditive C] : ObjectProperty C

The object property of compact objects.

Equations

• CategoryTheory.ObjectProperty.compactObjects K = CategoryTheory.IsCompactObject K

theorem CategoryTheory.ObjectProperty.isCompactObject_of_iso {C : Type u} [Category.{v, u} C] [Preadditive C] {K K' : C} (e : K ≅ K') (hK : IsCompactObject K) : IsCompactObject K'

Compactness is invariant under isomorphism.

instance CategoryTheory.ObjectProperty.instIsClosedUnderIsomorphismsCompactObjects {C : Type u} [Category.{v, u} C] [Preadditive C] : compactObjects.IsClosedUnderIsomorphisms

theorem CategoryTheory.Adjunction.isCompactObject_leftAdjoint_obj {C : Type u₁} [Category.{v, u₁} C] [Preadditive C] {D : Type u₂} [Category.{v, u₂} D] [Preadditive D] {L : Functor D C} {F : Functor C D} [L.Additive] (adj : L ⊣ F) (hF : F.PreservesSmallCoproducts) {K : D} (hK : IsCompactObject K) : IsCompactObject (L.obj K)

A left adjoint to a small-coproduct-preserving functor carries compact objects to compact objects. This is the compactness step in A.16 and A.17.

theorem CategoryTheory.Adjunction.compactObjects_map_leftAdjoint {C : Type u₁} [Category.{v, u₁} C] [Preadditive C] {D : Type u₂} [Category.{v, u₂} D] [Preadditive D] {L : Functor D C} {F : Functor C D} [L.Additive] (adj : L ⊣ F) (hF : F.PreservesSmallCoproducts) {G : ObjectProperty D} (hG : G ≤ ObjectProperty.compactObjects) : G.map L ≤ ObjectProperty.compactObjects

The essential image under a left adjoint of compact objects is compact when the right adjoint preserves small coproducts.