refactor(CategoryTheory/Generator): use ObjectProperty instead of Set (#30269)

In certain applications (see #30247), it becomes unpractical to have certains notions like `IsSeparating` defined for `Set C`, while the API for the relatively new `ObjectProperty` is expanding. In this PR, we move the definition of `IsSeparating` to the `ObjectProperty` namespace.

Author: joelriou

Mathlib/Algebra/Category/ModuleCat/AB.lean

@@ -36,11 +36,11 @@ instance : AB4Star (ModuleCat.{u} R) where
 
 lemma ModuleCat.isSeparator [Small.{v} R] : IsSeparator (ModuleCat.of.{v} R (Shrink.{v} R)) :=
     fun X Y f g h ↦ by
-  simp only [Set.mem_singleton_iff, forall_eq, ModuleCat.hom_ext_iff, LinearMap.ext_iff] at h
+  simp only [ObjectProperty.singleton_iff, ModuleCat.hom_ext_iff, hom_comp,
+    LinearMap.ext_iff, LinearMap.coe_comp, Function.comp_apply, forall_eq'] at h
   ext x
-  simpa [Shrink.linearEquiv, Equiv.linearEquiv] using
-    h (ModuleCat.ofHom ((LinearMap.toSpanSingleton R X x).comp
-      (Shrink.linearEquiv R R : Shrink R →ₗ[R] R))) 1
+  simpa using h (ModuleCat.ofHom ((LinearMap.toSpanSingleton R X x).comp
+    (Shrink.linearEquiv R R : Shrink R →ₗ[R] R))) 1
 
 instance [Small.{v} R] : HasSeparator (ModuleCat.{v} R) where
   hasSeparator := ⟨ModuleCat.of R (Shrink.{v} R), ModuleCat.isSeparator R⟩

Mathlib/Algebra/Category/ModuleCat/Presheaf/Generator.lean

@@ -69,24 +69,23 @@ lemma freeYonedaEquiv_comp {M N : PresheafOfModules.{v} R} {X : C}
 variable (R) in
 /-- The set of `PresheafOfModules.{v} R` consisting of objects of the
 form `(free R).obj (yoneda.obj X)` for some `X`. -/
-def freeYoneda : Set (PresheafOfModules.{v} R) := Set.range (yoneda ⋙ free R).obj
+def freeYoneda : ObjectProperty (PresheafOfModules.{v} R) := .ofObj (yoneda ⋙ free R).obj
 
 namespace freeYoneda
 
-instance : Small.{u} (freeYoneda R) := by
-  let π : C → freeYoneda R := fun X ↦ ⟨_, ⟨X, rfl⟩⟩
-  have hπ : Function.Surjective π := by rintro ⟨_, ⟨X, rfl⟩⟩; exact ⟨X, rfl⟩
-  exact small_of_surjective hπ
+instance : ObjectProperty.Small.{u} (freeYoneda R) := by
+  dsimp [freeYoneda]
+  infer_instance
 
 variable (R)
 
-lemma isSeparating : IsSeparating (freeYoneda R) := by
+lemma isSeparating : ObjectProperty.IsSeparating (freeYoneda R) := by
   intro M N f₁ f₂ h
   ext ⟨X⟩ m
   obtain ⟨g, rfl⟩ := freeYonedaEquiv.surjective m
-  exact congr_arg freeYonedaEquiv (h _ ⟨X, rfl⟩ g)
+  exact congr_arg freeYonedaEquiv (h _ ⟨X⟩ g)
 
-lemma isDetecting : IsDetecting (freeYoneda R) :=
+lemma isDetecting : ObjectProperty.IsDetecting (freeYoneda R) :=
   (isSeparating R).isDetecting
 
 end freeYoneda

Mathlib/CategoryTheory/Abelian/GrothendieckCategory/EnoughInjectives.lean

@@ -111,8 +111,8 @@ lemma exists_pushouts
     ∃ (X' : C) (i : X ⟶ X') (p' : X' ⟶ Y) (_ : (generatingMonomorphisms G).pushouts i)
       (_ : ¬ IsIso i) (_ : Mono p'), i ≫ p' = p := by
   rw [hG.isDetector.isIso_iff_of_mono] at hp
-  simp only [coyoneda_obj_obj, coyoneda_obj_map, Set.mem_singleton_iff, forall_eq,
-    Function.Surjective, not_forall, not_exists] at hp
+  simp only [ObjectProperty.singleton_iff, Function.Surjective, coyoneda_obj_obj,
+    coyoneda_obj_map, forall_eq', not_forall, not_exists] at hp
   -- `f : G ⟶ Y` is a monomorphism the image of which is not contained in `X`
   obtain ⟨f, hf⟩ := hp
   -- we use the subobject `X'` of `Y` that is generated by the images of `p : X ⟶ Y`

Mathlib/CategoryTheory/Abelian/GrothendieckCategory/ModuleEmbedding/GabrielPopescu.lean

@@ -40,7 +40,7 @@ namespace CategoryTheory.IsGrothendieckAbelian
 variable {C : Type u} [Category.{v} C] [Abelian C] [IsGrothendieckAbelian.{v} C]
 
 instance {G : C} : (preadditiveCoyonedaObj G).IsRightAdjoint :=
-  isRightAdjoint_of_preservesLimits_of_isCoseparating (isCoseparator_coseparator _) _
+  isRightAdjoint_of_preservesLimits_of_isCoseparating.{v} (isCoseparator_coseparator _) _
 
 /-- The left adjoint of the functor `Hom(G, ·)`, which can be thought of as `· ⊗ G`. -/
 noncomputable def tensorObj (G : C) : ModuleCat (End G)ᵐᵒᵖ ⥤ C :=

Mathlib/CategoryTheory/Adjunction/AdjointFunctorTheorems.lean

@@ -101,20 +101,22 @@ variable {D : Type u'} [Category.{v} D]
 well-powered and has a small coseparating set, then `G` has a left adjoint.
 -/
 lemma isRightAdjoint_of_preservesLimits_of_isCoseparating [HasLimits D] [WellPowered.{v} D]
-    {𝒢 : Set D} [Small.{v} 𝒢] (h𝒢 : IsCoseparating 𝒢) (G : D ⥤ C) [PreservesLimits G] :
-    G.IsRightAdjoint :=
-  have : ∀ A, HasInitial (StructuredArrow A G) := fun A =>
-    hasInitial_of_isCoseparating (StructuredArrow.isCoseparating_proj_preimage A G h𝒢)
-  isRightAdjointOfStructuredArrowInitials _
+    {P : ObjectProperty D} [ObjectProperty.Small.{v} P]
+    (hP : P.IsCoseparating) (G : D ⥤ C) [PreservesLimits G] :
+    G.IsRightAdjoint := by
+  have : ∀ A, HasInitial (StructuredArrow A G) := fun A ↦
+    hasInitial_of_isCoseparating (StructuredArrow.isCoseparating_inverseImage_proj A G hP)
+  exact isRightAdjointOfStructuredArrowInitials _
 
 /-- The special adjoint functor theorem: if `F : C ⥤ D` preserves colimits and `C` is cocomplete,
 well-copowered and has a small separating set, then `F` has a right adjoint.
 -/
 lemma isLeftAdjoint_of_preservesColimits_of_isSeparating [HasColimits C] [WellPowered.{v} Cᵒᵖ]
-    {𝒢 : Set C} [Small.{v} 𝒢] (h𝒢 : IsSeparating 𝒢) (F : C ⥤ D) [PreservesColimits F] :
+    {P : ObjectProperty C} [ObjectProperty.Small.{v} P]
+    (h𝒢 : P.IsSeparating) (F : C ⥤ D) [PreservesColimits F] :
     F.IsLeftAdjoint :=
   have : ∀ A, HasTerminal (CostructuredArrow F A) := fun A =>
-    hasTerminal_of_isSeparating (CostructuredArrow.isSeparating_proj_preimage F A h𝒢)
+    hasTerminal_of_isSeparating (CostructuredArrow.isSeparating_inverseImage_proj F A h𝒢)
   isLeftAdjoint_of_costructuredArrowTerminals _
 
 end SpecialAdjointFunctorTheorem
@@ -123,19 +125,19 @@ namespace Limits
 
 /-- A consequence of the special adjoint functor theorem: if `C` is complete, well-powered and
     has a small coseparating set, then it is cocomplete. -/
-theorem hasColimits_of_hasLimits_of_isCoseparating [HasLimits C] [WellPowered.{v} C] {𝒢 : Set C}
-    [Small.{v} 𝒢] (h𝒢 : IsCoseparating 𝒢) : HasColimits C :=
+theorem hasColimits_of_hasLimits_of_isCoseparating [HasLimits C] [WellPowered.{v} C]
+    {P : ObjectProperty C} [ObjectProperty.Small.{v} P] (hP : P.IsCoseparating) : HasColimits C :=
   { has_colimits_of_shape := fun _ _ =>
       hasColimitsOfShape_iff_isRightAdjoint_const.2
-        (isRightAdjoint_of_preservesLimits_of_isCoseparating h𝒢 _) }
+        (isRightAdjoint_of_preservesLimits_of_isCoseparating hP _) }
 
 /-- A consequence of the special adjoint functor theorem: if `C` is cocomplete, well-copowered and
     has a small separating set, then it is complete. -/
-theorem hasLimits_of_hasColimits_of_isSeparating [HasColimits C] [WellPowered.{v} Cᵒᵖ] {𝒢 : Set C}
-    [Small.{v} 𝒢] (h𝒢 : IsSeparating 𝒢) : HasLimits C :=
+theorem hasLimits_of_hasColimits_of_isSeparating [HasColimits C] [WellPowered.{v} Cᵒᵖ]
+    {P : ObjectProperty C} [ObjectProperty.Small.{v} P] (hP : P.IsSeparating) : HasLimits C :=
   { has_limits_of_shape := fun _ _ =>
       hasLimitsOfShape_iff_isLeftAdjoint_const.2
-        (isLeftAdjoint_of_preservesColimits_of_isSeparating h𝒢 _) }
+        (isLeftAdjoint_of_preservesColimits_of_isSeparating hP _) }
 
 /-- A consequence of the special adjoint functor theorem: if `C` is complete, well-powered and
     has a separator, then it is complete. -/

Mathlib/CategoryTheory/Comma/StructuredArrow/Small.lean

@@ -5,7 +5,7 @@ Authors: Markus Himmel
 -/
 import Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
 import Mathlib.CategoryTheory.EssentiallySmall
-import Mathlib.Logic.Small.Set
+import Mathlib.CategoryTheory.ObjectProperty.Small
 
 /-!
 # Small sets in the category of structured arrows
@@ -25,26 +25,39 @@ namespace StructuredArrow
 
 variable {S : D} {T : C ⥤ D}
 
-instance small_proj_preimage_of_locallySmall {𝒢 : Set C} [Small.{v₁} 𝒢] [LocallySmall.{v₁} D] :
-    Small.{v₁} ((proj S T).obj ⁻¹' 𝒢) := by
-  suffices (proj S T).obj ⁻¹' 𝒢 = Set.range fun f : Σ G : 𝒢, S ⟶ T.obj G => mk f.2 by
+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
+  suffices P.inverseImage (proj S T) = .ofObj fun f : Σ (G : Subtype P), S ⟶ T.obj G => mk f.2 by
     rw [this]
     infer_instance
-  exact Set.ext fun X => ⟨fun h => ⟨⟨⟨_, h⟩, X.hom⟩, (eq_mk _).symm⟩, by cat_disch⟩
+  ext X
+  simp only [ObjectProperty.prop_inverseImage_iff, proj_obj, ObjectProperty.ofObj_iff,
+    Sigma.exists, Subtype.exists, exists_prop]
+  exact ⟨fun h ↦ ⟨_, h, _, rfl⟩, by rintro ⟨_, h, _, rfl⟩; exact h⟩
+
+@[deprecated (since := "2025-10-07")] alias small_proj_preimage_of_locallySmall :=
+  small_inverseImage_proj_of_locallySmall
 
 end StructuredArrow
 
 namespace CostructuredArrow
 
 variable {S : C ⥤ D} {T : D}
 
-instance small_proj_preimage_of_locallySmall {𝒢 : Set C} [Small.{v₁} 𝒢] [LocallySmall.{v₁} D] :
-    Small.{v₁} ((proj S T).obj ⁻¹' 𝒢) := by
-  suffices (proj S T).obj ⁻¹' 𝒢 = Set.range fun f : Σ G : 𝒢, S.obj G ⟶ T => mk f.2 by
+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
+  suffices P.inverseImage (proj S T) = .ofObj fun f : Σ (G : Subtype P), S.obj G ⟶ T => mk f.2 by
     rw [this]
     infer_instance
-  exact Set.ext fun X => ⟨fun h => ⟨⟨⟨_, h⟩, X.hom⟩, (eq_mk _).symm⟩, by cat_disch⟩
+  ext X
+  simp only [ObjectProperty.prop_inverseImage_iff, proj_obj, ObjectProperty.ofObj_iff,
+    Sigma.exists, Subtype.exists, exists_prop]
+  exact ⟨fun h ↦ ⟨_, h, _, rfl⟩, by rintro ⟨_, h, _, rfl⟩; exact h⟩
 
+@[deprecated (since := "2025-10-07")] alias small_proj_preimage_of_locallySmall :=
+  small_inverseImage_proj_of_locallySmall
 end CostructuredArrow
 
 end CategoryTheory