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

[joelriou]

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.

---

• depends on: [Merged by Bors] - feat(CategoryTheory): the opposite of a property of objects #30294

[github-actions]

PR summary 0d837987e5

Import changes for modified files

Dependency changes

File	Base Count	Head Count	Change
Mathlib.CategoryTheory.Comma.StructuredArrow.Small	483	459	-24 (-4.97%)
Mathlib.CategoryTheory.Generator.Basic	758	759	+1 (+0.13%)
Mathlib.CategoryTheory.Generator.Presheaf	759	760	+1 (+0.13%)
Mathlib.CategoryTheory.Adjunction.AdjointFunctorTheorems	773	772	-1 (-0.13%)
Mathlib.CategoryTheory.Generator.HomologicalComplex	777	778	+1 (+0.13%)
Mathlib.CategoryTheory.Generator.Sheaf	791	792	+1 (+0.13%)
Mathlib.CategoryTheory.Generator.Preadditive	849	850	+1 (+0.12%)
Mathlib.CategoryTheory.Generator.Indization	970	971	+1 (+0.10%)
Mathlib.CategoryTheory.Abelian.GrothendieckCategory.EnoughInjectives	1147	1148	+1 (+0.09%)
Mathlib.Algebra.Category.ModuleCat.Presheaf.Generator	1352	1353	+1 (+0.07%)
Mathlib.Algebra.Category.ModuleCat.AB	1364	1365	+1 (+0.07%)
Mathlib.CategoryTheory.Abelian.GrothendieckCategory.ModuleEmbedding.GabrielPopescu	1465	1466	+1 (+0.07%)

Import changes for all files

Files	Import difference
Mathlib.CategoryTheory.Comma.StructuredArrow.Small	-24
Mathlib.CategoryTheory.Adjunction.AdjointFunctorTheorems	-1
22 files Mathlib.Algebra.Category.ModuleCat.AB Mathlib.Algebra.Category.ModuleCat.Presheaf.Generator Mathlib.Algebra.Category.ModuleCat.Presheaf.Pullback Mathlib.Algebra.Category.ModuleCat.Sheaf.PullbackContinuous Mathlib.CategoryTheory.Abelian.FreydMitchell Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Indization Mathlib.CategoryTheory.Abelian.GrothendieckCategory.ColimCoyoneda Mathlib.CategoryTheory.Abelian.GrothendieckCategory.Coseparator Mathlib.CategoryTheory.Abelian.GrothendieckCategory.EnoughInjectives Mathlib.CategoryTheory.Abelian.GrothendieckCategory.ModuleEmbedding.GabrielPopescu Mathlib.CategoryTheory.Abelian.GrothendieckCategory.ModuleEmbedding.Opposite Mathlib.CategoryTheory.Abelian.GrothendieckCategory.Subobject Mathlib.CategoryTheory.Abelian.Yoneda Mathlib.CategoryTheory.Generator.Abelian Mathlib.CategoryTheory.Generator.Basic Mathlib.CategoryTheory.Generator.HomologicalComplex Mathlib.CategoryTheory.Generator.Indization Mathlib.CategoryTheory.Generator.Preadditive Mathlib.CategoryTheory.Generator.Presheaf Mathlib.CategoryTheory.Generator.Sheaf Mathlib.Condensed.AB Mathlib.Condensed.Light.AB	1

---

Declarations diff

+ CostructuredArrow.isSeparating_proj_preimage
+ IsCodetecting.of_le
+ IsCoseparating.of_equivalence
+ IsCoseparating.of_le
+ IsDetecting.of_le
+ IsSeparating.of_equivalence
+ IsSeparating.of_le
+ ObjectProperty.IsSeparating.isSeparator_coproduct
+ StructuredArrow.isCoseparating_proj_preimage
+ instance : ObjectProperty.Small.{u} (freeYoneda R) := by
+ isCodetecting_bot_of_isGroupoid
+ isCoseparating_bot_of_isThin
+ isCoseparating_inverseImage_proj
+ isCoseparator_iff_of_isLimit_fan
+ isCoseparator_of_isLimit_fan
+ isDetecting_bot_of_isGroupoid
+ isGroupoid_of_isCodetecting_bot
+ isGroupoid_of_isDetecting_bot
+ isSeparating_bot_of_isThin
+ isSeparating_inverseImage_proj
+ isSeparator_iff_of_isColimit_cofan
+ isThin_of_isCoseparating_bot
+ isThin_of_isSeparating_bot
++ small_inverseImage_proj_of_locallySmall
++- IsCodetecting.isCoseparating
++- IsCodetecting.isIso_iff_of_epi
++- IsCoseparating.isCodetecting
++- IsDetecting.isIso_iff_of_mono
++- IsDetecting.isSeparating
++- IsSeparating.isDetecting
++- isCodetecting_iff_isCoseparating
++- isCodetecting_unop_iff
++- isCoseparating_unop_iff
++- isDetecting_unop_iff
++- isSeparating_unop_iff
++-- small_proj_preimage_of_locallySmall
+-+ IsCodetecting
+-+ IsCoseparating
+-+ IsDetecting
+-+ IsSeparating
+-+ isCodetecting_op_iff
+-+ isCoseparating_iff_mono
+-+ isCoseparating_op_iff
+-+ isDetecting_iff_isSeparating
+-+ isDetecting_op_iff
+-+ isSeparating_iff_epi
+-+ isSeparating_op_iff
- instance : Small.{u} (freeYoneda R) := by
- isCoseparating_proj_preimage
- isSeparating_proj_preimage
-+--++ isSeparating
--++ isSeparator

You can run this locally as follows

## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>

The doc-module for script/declarations_diff.sh contains some details about this script.

---

No changes to technical debt.

You can run this locally as

./scripts/technical-debt-metrics.sh pr_summary

• The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
• The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).

[mathlib4-dependent-issues-bot]

This PR/issue depends on:

• [Merged by Bors] - feat(CategoryTheory): the opposite of a property of objects #30294
  By Dependent Issues (🤖). Happy coding!