feat(CategoryTheory): strong generators (#29519)

In this PR, we introduce a condition `IsStrongGenerator P` on `P : ObjectProperty C` which is stronger than `IsSeparating P` as we also require that for any proper subobject `A ⊂ X`, there exists a morphism `G ⟶ X` from an
object satisfying `P` which does not factor through `A`.

In case coproducts exists, we give a characterization of `IsStrongSeparator P` in terms of the existence, for each object `X : C` of an extremal epi to `X` from a coproduct of objects in `S`. 

In future works (#30241), this shall be used in order to characterize locally `κ`-presentable categories as cocomplete categories that have a strong generator consisting of `κ`-presentable objects.

Author: joelriou

Mathlib.lean

@@ -2345,6 +2345,7 @@ import Mathlib.CategoryTheory.Generator.Indization
 import Mathlib.CategoryTheory.Generator.Preadditive
 import Mathlib.CategoryTheory.Generator.Presheaf
 import Mathlib.CategoryTheory.Generator.Sheaf
+import Mathlib.CategoryTheory.Generator.StrongGenerator
 import Mathlib.CategoryTheory.GlueData
 import Mathlib.CategoryTheory.GradedObject
 import Mathlib.CategoryTheory.GradedObject.Associator

Mathlib/CategoryTheory/Comma/StructuredArrow/Small.lean

@@ -17,14 +17,20 @@ be used in the proof of the Special Adjoint Functor Theorem.
 namespace CategoryTheory
 
 -- morphism levels before object levels. See note [category theory universes].
-universe v₁ v₂ u₁ u₂
+universe w v₁ v₂ u₁ u₂
 
 variable {C : Type u₁} [Category.{v₁} C] {D : Type u₂} [Category.{v₂} D]
 
 namespace StructuredArrow
 
 variable {S : D} {T : C ⥤ D}
 
+instance [Small.{w} C] [LocallySmall.{w} D] : Small.{w} (StructuredArrow S T) :=
+  small_of_surjective (f := fun (f : Σ (X : C), S ⟶ T.obj X) ↦ StructuredArrow.mk f.2)
+    (fun f ↦ by
+      obtain ⟨X, f, rfl⟩ := f.mk_surjective
+      exact ⟨⟨X, f⟩, rfl⟩)
+
 instance small_inverseImage_proj_of_locallySmall
     {P : ObjectProperty C} [ObjectProperty.Small.{v₁} P] [LocallySmall.{v₁} D] :
     ObjectProperty.Small.{v₁} (P.inverseImage (proj S T)) := by
@@ -45,6 +51,12 @@ namespace CostructuredArrow
 
 variable {S : C ⥤ D} {T : D}
 
+instance [Small.{w} C] [LocallySmall.{w} D] : Small.{w} (CostructuredArrow S T) :=
+  small_of_surjective (f := fun (f : Σ (X : C), S.obj X ⟶ T) ↦ CostructuredArrow.mk f.2)
+    (fun f ↦ by
+      obtain ⟨X, f, rfl⟩ := f.mk_surjective
+      exact ⟨⟨X, f⟩, rfl⟩)
+
 instance small_inverseImage_proj_of_locallySmall
     {P : ObjectProperty C} [ObjectProperty.Small.{v₁} P] [LocallySmall.{v₁} D] :
     ObjectProperty.Small.{v₁} (P.inverseImage (proj S T)) := by

Mathlib/CategoryTheory/Generator/Basic.lean

@@ -7,6 +7,7 @@ import Mathlib.CategoryTheory.Limits.EssentiallySmall
 import Mathlib.CategoryTheory.Limits.Shapes.Opposites.Equalizers
 import Mathlib.CategoryTheory.Subobject.Lattice
 import Mathlib.CategoryTheory.ObjectProperty.Small
+import Mathlib.CategoryTheory.Comma.StructuredArrow.Small
 
 /-!
 # Separating and detecting sets
@@ -287,31 +288,103 @@ lemma isCodetecting_bot_of_isGroupoid [IsGroupoid C] :
 
 end Empty
 
+lemma IsSeparating.mk_of_exists_epi
+    (hP : ∀ (X : C), ∃ (ι : Type w) (s : ι → C) (_ : ∀ i, P (s i)) (c : Cofan s) (_ : IsColimit c)
+      (p : c.pt ⟶ X), Epi p) :
+    P.IsSeparating := by
+  intro X Y f g h
+  obtain ⟨ι, s, hs, c, hc, p, _⟩ := hP X
+  rw [← cancel_epi p]
+  exact Cofan.IsColimit.hom_ext hc _ _
+    (fun i ↦ by simpa using h _ (hs i) (c.inj i ≫ p))
+
+lemma IsCoseparating.mk_of_exists_mono
+    (hP : ∀ (X : C), ∃ (ι : Type w) (s : ι → C) (_ : ∀ i, P (s i)) (c : Fan s) (_ : IsLimit c)
+      (j : X ⟶ c.pt), Mono j) :
+    P.IsCoseparating := by
+  intro X Y f g h
+  obtain ⟨ι, s, hs, c, hc, j, _⟩ := hP Y
+  rw [← cancel_mono j]
+  exact Fan.IsLimit.hom_ext hc _ _
+    (fun i ↦ by simpa using h _ (hs i) (j ≫ c.proj i))
+
 variable (P)
 
+section
+
+/-- Given `P : ObjectProperty C` and `X : C`, this is the map which
+sends `i : CostructuredArrow P.ι X` to `i.left.obj : C`. The coproduct
+of this family is the source of the morphism `P.coproductFrom X`. -/
+abbrev coproductFromFamily (X : C) (i : CostructuredArrow P.ι X) : C := i.left.obj
+
+variable (X : C)
+
+variable [HasCoproduct (P.coproductFromFamily X)]
+
+/-- Given `P : ObjectProperty C` and `X : C`, this is the coproduct of
+all the morphisms `Y ⟶ X` such that `P Y` holds. -/
+noncomputable abbrev coproductFrom : ∐ (P.coproductFromFamily X) ⟶ X :=
+  Sigma.desc (fun i ↦ i.hom)
+
+variable {X} in
+/-- The inclusion morphisms to `∐ (P.coproductFromFamily X)`. -/
+noncomputable abbrev ιCoproductFrom {Y : C} (f : Y ⟶ X) (hY : P Y) :
+    Y ⟶ ∐ (P.coproductFromFamily X) := by
+  exact Sigma.ι (P.coproductFromFamily X) (CostructuredArrow.mk (Y := ⟨Y, hY⟩) (by exact f))
+
+end
+
+variable {P} in
+lemma IsSeparating.epi_coproductFrom (hP : P.IsSeparating)
+    (X : C) [HasCoproduct (P.coproductFromFamily X)] :
+    Epi (P.coproductFrom X) where
+  left_cancellation u v huv :=
+    hP _ _ (fun G hG h ↦ by simpa using P.ιCoproductFrom h hG ≫= huv)
+
 theorem isSeparating_iff_epi
-    [∀ A : C, HasCoproduct fun f : Σ G : Subtype P, G.1 ⟶ A ↦ f.1.1] :
-    IsSeparating P ↔
-      ∀ A : C, Epi (Sigma.desc (Sigma.snd (β := fun (G : Subtype P) ↦ G.1 ⟶ A))) := by
-  let β (A : C) (G : Subtype P) := G.1 ⟶ A
-  let b (A : C) (x : Σ G, β A G) := x.1.1
-  refine ⟨fun h A ↦ ⟨fun u v huv ↦ h _ _ fun G hG f ↦ ?_⟩, fun h X Y f g hh ↦ ?_⟩
-  · simpa [β, b] using Sigma.ι (b A) ⟨⟨G, hG⟩, f⟩ ≫= huv
-  · rw [← cancel_epi (Sigma.desc (Sigma.snd (β := β X)))]
-    ext ⟨⟨_, hG⟩, _⟩
-    simpa using hh _ hG _
+    [∀ (X : C), HasCoproduct (P.coproductFromFamily X)] :
+    IsSeparating P ↔ ∀ X : C, Epi (P.coproductFrom X) :=
+  ⟨fun hP X ↦ hP.epi_coproductFrom X,
+    fun hP ↦ IsSeparating.mk_of_exists_epi (fun X ↦ ⟨_, P.coproductFromFamily X,
+      fun i ↦ i.left.2, _, colimit.isColimit _, _, hP X⟩)⟩
+
+section
+
+/-- Given `P : ObjectProperty C` and `X : C`, this is the map which
+sends `i : StructuredArrow P.ι X` to `i.right.obj : C`. The product
+of this family is the target of the morphism `P.productTo X`. -/
+abbrev productToFamily (X : C) (i : StructuredArrow X P.ι) : C := i.right.obj
+
+variable (X : C)
+
+variable [HasProduct (P.productToFamily X)]
+
+/-- Given `P : ObjectProperty C` and `X : C`, this is the product of
+all the morphisms `X ⟶ Y` such that `P Y` holds. -/
+noncomputable abbrev productTo : X ⟶ ∏ᶜ (P.productToFamily X) :=
+  Pi.lift (fun i ↦ i.hom)
+
+variable {X} in
+/-- The projection morphisms from `∏ᶜ (P.productToFamily X)`. -/
+noncomputable abbrev πProductTo {Y : C} (f : X ⟶ Y) (hY : P Y) :
+    ∏ᶜ (P.productToFamily X) ⟶ Y := by
+  exact Pi.π (P.productToFamily X) (StructuredArrow.mk (Y := ⟨Y, hY⟩) (by exact f))
+
+end
+
+variable {P} in
+lemma IsCoseparating.mono_productTo (hP : P.IsCoseparating)
+    (X : C) [HasProduct (P.productToFamily X)] :
+    Mono (P.productTo X) where
+  right_cancellation u v huv :=
+    hP _ _ (fun G hG h ↦ by simpa using huv =≫ P.πProductTo h hG)
 
 theorem isCoseparating_iff_mono
-    [∀ A : C, HasProduct fun f : Σ G : Subtype P, A ⟶ G.1 ↦ f.1.1] :
-    IsCoseparating P ↔
-      ∀ A : C, Mono (Pi.lift (Sigma.snd (β := fun (G : Subtype P) ↦ A ⟶ G.1))) := by
-  let β (A : C) (G : Subtype P) := A ⟶ G.1
-  let b (A : C) (x : Σ G, β A G) := x.1.1
-  refine ⟨fun h A ↦ ⟨fun u v huv ↦ h _ _ fun G hG f ↦ ?_⟩, fun h X Y f g hh ↦ ?_⟩
-  · simpa [β, b] using huv =≫ Pi.π (b A) ⟨⟨G, hG⟩, f⟩
-  · rw [← cancel_mono (Pi.lift (Sigma.snd (β := β Y)))]
-    ext ⟨⟨_, hG⟩, _⟩
-    simpa using hh _ hG _
+    [∀ (X : C), HasProduct (P.productToFamily X)] :
+    IsCoseparating P ↔ ∀ X : C, Mono (P.productTo X) :=
+  ⟨fun hP X ↦ hP.mono_productTo X,
+    fun hP ↦ IsCoseparating.mk_of_exists_mono (fun X ↦ ⟨_, P.productToFamily X,
+      fun i ↦ i.right.2, _, limit.isLimit _, _, hP X⟩)⟩
 
 end ObjectProperty
 
@@ -324,16 +397,17 @@ theorem hasInitial_of_isCoseparating [LocallySmall.{w} C] [WellPowered.{w} C]
     [HasLimitsOfSize.{w, w} C] {P : ObjectProperty C} [ObjectProperty.Small.{w} P]
     (hP : P.IsCoseparating) : HasInitial C := by
   have := hasFiniteLimits_of_hasLimitsOfSize C
-  haveI : HasProductsOfShape (Subtype P) C := hasProductsOfShape_of_small C (Subtype P)
-  haveI := fun A => hasProductsOfShape_of_small.{w} C (Σ G : Subtype P, A ⟶ (G : C))
+  haveI := hasProductsOfShape_of_small C (Subtype P)
+  haveI := fun A => hasProductsOfShape_of_small.{w} C (StructuredArrow A P.ι)
   letI := completeLatticeOfCompleteSemilatticeInf (Subobject (piObj (Subtype.val : Subtype P → C)))
   suffices ∀ A : C, Unique (((⊥ : Subobject (piObj (Subtype.val : Subtype P → C))) : C) ⟶ A) by
     exact hasInitial_of_unique ((⊥ : Subobject (piObj (Subtype.val : Subtype P → C))) : C)
+  have := hP.mono_productTo
   refine fun A => ⟨⟨?_⟩, fun f => ?_⟩
-  · let s := Pi.lift fun f : Σ G : Subtype P, A ⟶ (G : C) => Pi.π (Subtype.val : Subtype P → C) f.1
-    let t := Pi.lift (@Sigma.snd (Subtype P) fun G => A ⟶ (G : C))
-    haveI : Mono t := P.isCoseparating_iff_mono.1 hP A
-    exact Subobject.ofLEMk _ (pullback.fst _ _ : pullback s t ⟶ _) bot_le ≫ pullback.snd _ _
+  · let s : ∏ᶜ (Subtype.val (p := P)) ⟶ ∏ᶜ P.productToFamily A :=
+      Pi.lift (fun f ↦ Pi.π Subtype.val ⟨f.right.obj, f.right.property⟩)
+    exact Subobject.ofLEMk _
+      (pullback.fst _ _ : pullback s (P.productTo A) ⟶ _) bot_le ≫ pullback.snd _ _
   · suffices ∀ (g : Subobject.underlying.obj ⊥ ⟶ A), f = g by
       apply this
     intro g

Mathlib/CategoryTheory/Generator/StrongGenerator.lean

@@ -0,0 +1,135 @@
+/-
+Copyright (c) 2025 Joël Riou. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Joël Riou
+-/
+import Mathlib.CategoryTheory.ExtremalEpi
+import Mathlib.CategoryTheory.Generator.Basic
+
+/-!
+# Strong generators
+
+If `P : ObjectProperty C`, we say that `P` is a strong generator if it is a
+generator (in the sense that `IsSeparating P` holds) such that for any
+proper subobject `A ⊂ X`, there exists a morphism `G ⟶ X` which does not factor
+through `A` from an object satisfying `P`.
+
+The main result is the lemma `isStrongGenerator_iff_exists_extremalEpi` which
+says that if `P` is `w`-small, `C` is locally `w`-small and
+has coproducts of size `w`, then `P` is a strong generator iff any
+object of `C` is the target of an extremal epimorphism from a coproduct of
+objects satisfying `P`.
+
+## References
+* [Adámek, J. and Rosický, J., *Locally presentable and accessible categories*][Adamek_Rosicky_1994]
+
+-/
+
+universe w v u
+
+namespace CategoryTheory
+
+open Limits
+
+
+namespace ObjectProperty
+
+variable {C : Type u} [Category.{v} C] (P : ObjectProperty C)
+
+/-- A property `P : ObjectProperty C` is a strong generator
+if it is separating and for any proper subobject `A ⊂ X`, there exists
+a morphism `G ⟶ X` which does not factor through `A` from an object
+such that `P G` holds. -/
+def IsStrongGenerator : Prop :=
+  P.IsSeparating ∧ ∀ ⦃X : C⦄ (A : Subobject X),
+    (∀ (G : C) (_ : P G) (f : G ⟶ X), Subobject.Factors A f) → A = ⊤
+
+variable {P}
+
+lemma isStrongGenerator_iff :
+    P.IsStrongGenerator ↔ P.IsSeparating ∧
+      ∀ ⦃X Y : C⦄ (i : X ⟶ Y) [Mono i],
+        (∀ (G : C) (_ : P G), Function.Surjective (fun (f : G ⟶ X) ↦ f ≫ i)) → IsIso i := by
+  refine ⟨fun ⟨hS₁, hS₂⟩ ↦ ⟨hS₁, fun X Y i _ h ↦ ?_⟩,
+    fun ⟨hS₁, hS₂⟩ ↦ ⟨hS₁, fun X A hA ↦ ?_⟩⟩
+  · rw [Subobject.isIso_iff_mk_eq_top]
+    refine hS₂ _ (fun G hG g ↦ ?_)
+    rw [Subobject.mk_factors_iff]
+    exact h G hG g
+  · rw [← Subobject.isIso_arrow_iff_eq_top]
+    exact hS₂ A.arrow (fun G hG g ↦ ⟨_, Subobject.factorThru_arrow _ _ (hA G hG g)⟩)
+
+namespace IsStrongGenerator
+
+section
+
+variable (hP : P.IsStrongGenerator)
+
+include hP
+
+lemma isSeparating : P.IsSeparating := hP.1
+
+lemma subobject_eq_top {X : C} {A : Subobject X}
+    (hA : ∀ (G : C) (_ : P G) (f : G ⟶ X), Subobject.Factors A f) :
+    A = ⊤ :=
+  hP.2 _ hA
+
+lemma isIso_of_mono ⦃X Y : C⦄ (i : X ⟶ Y) [Mono i]
+    (hi : ∀ (G : C) (_ : P G), Function.Surjective (fun (f : G ⟶ X) ↦ f ≫ i)) : IsIso i :=
+  (isStrongGenerator_iff.1 hP).2 i hi
+
+lemma exists_of_subobject_ne_top {X : C} {A : Subobject X} (hA : A ≠ ⊤) :
+    ∃ (G : C) (_ : P G) (f : G ⟶ X), ¬ Subobject.Factors A f := by
+  by_contra!
+  exact hA (hP.subobject_eq_top this)
+
+lemma exists_of_mono_not_isIso {X Y : C} (i : X ⟶ Y) [Mono i] (hi : ¬ IsIso i) :
+    ∃ (G : C) (_ : P G) (g : G ⟶ Y), ∀ (f : G ⟶ X), f ≫ i ≠ g := by
+  by_contra!
+  exact hi (hP.isIso_of_mono i this)
+
+end
+
+end IsStrongGenerator
+
+namespace IsStrongGenerator
+
+lemma mk_of_exists_extremalEpi
+    (hS : ∀ (X : C), ∃ (ι : Type w) (s : ι → C) (_ : ∀ i, P (s i)) (c : Cofan s) (_ : IsColimit c)
+      (p : c.pt ⟶ X), ExtremalEpi p) :
+    P.IsStrongGenerator := by
+  rw [isStrongGenerator_iff]
+  refine ⟨IsSeparating.mk_of_exists_epi.{w} (fun X ↦ ?_), fun X Y i _ hi ↦ ?_⟩
+  · obtain ⟨ι, s, hs, c, hc, p, _⟩ := hS X
+    exact ⟨ι, s, hs, c, hc, p, inferInstance⟩
+  · obtain ⟨ι, s, hs, c, hc, p, _⟩ := hS Y
+    replace hi (j : ι) := hi (s j) (hs j) (c.inj j ≫ p)
+    choose φ hφ using hi
+    exact ExtremalEpi.isIso p (Cofan.IsColimit.desc hc φ) _
+      (Cofan.IsColimit.hom_ext hc _ _ (by simp [hφ]))
+
+lemma extremalEpi_coproductFrom
+    (hP : IsStrongGenerator P) (X : C) [HasCoproduct (P.coproductFromFamily X)] :
+    ExtremalEpi (P.coproductFrom X) where
+  toEpi := hP.isSeparating.epi_coproductFrom X
+  isIso p i fac _ := hP.isIso_of_mono _ (fun G hG f ↦ ⟨P.ιCoproductFrom f hG ≫ p, by simp [fac]⟩)
+
+end IsStrongGenerator
+
+lemma isStrongGenerator_iff_exists_extremalEpi
+    [HasCoproducts.{w} C] [LocallySmall.{w} C] [ObjectProperty.Small.{w} P] :
+    P.IsStrongGenerator ↔
+      ∀ (X : C), ∃ (ι : Type w) (s : ι → C) (_ : ∀ i, P (s i)) (c : Cofan s) (_ : IsColimit c)
+        (p : c.pt ⟶ X), ExtremalEpi p := by
+  refine ⟨fun hP X ↦ ?_, fun hP ↦ .mk_of_exists_extremalEpi hP⟩
+  have := hasCoproductsOfShape_of_small.{w} C (CostructuredArrow P.ι X)
+  have := (coproductIsCoproduct (P.coproductFromFamily X)).whiskerEquivalence
+    (Discrete.equivalence (equivShrink.{w} _)).symm
+  refine ⟨_, fun j ↦ ((equivShrink.{w} (CostructuredArrow P.ι X)).symm j).left.1,
+    fun j ↦ ((equivShrink.{w} _).symm j).1.2, _,
+    (coproductIsCoproduct (P.coproductFromFamily X)).whiskerEquivalence
+    (Discrete.equivalence (equivShrink.{w} _)).symm, _, hP.extremalEpi_coproductFrom X⟩
+
+end ObjectProperty
+
+end CategoryTheory