refactor(CategoryTheory/Presentable): cleaning up HasCardinalFilteredGenerator(s)

[joelriou]

We move IsCardinalFilteredGenerator(s) to the ObjectProperty namespace. Instead of using an index type in Type w for parametrising a family of objects, we use ObjectProperty and express the (essential) smallness using the typeclass ObjectProperty.(Essentially)Small.

---

• depends on: feat(CategoryTheory): dense functors #29565
• depends on: refactor(CategoryTheory/Generator): use ObjectProperty instead of Set #30269
• depends on: [Merged by Bors] - feat(CategoryTheory): functors that are dense at an object #29556
• depends on: feat(CategoryTheory): strong generators #29519
• depends on: feat(CategoryTheory): a property of objects is a strong generator if any object is a colimit of objects satisfying the property #29543
• depends on: feat(CategoryTheory/ObjectProperty): closure of a property under certain limits #29854
• depends on: refactor(CategoryTheory/ObjectProperty): IsClosedUnderLimitsOfShape #29881
• depends on: [Merged by Bors] - chore(CategoryTheory): split Limits.Presentation #29903

[github-actions]

PR summary 02905c8573

Import changes exceeding 2%

%	File
+2.37%	Mathlib.Algebra.Category.ModuleCat.Presheaf.Generator
+24.61%	Mathlib.CategoryTheory.Adjunction.AdjointFunctorTheorems
+26.02%	Mathlib.CategoryTheory.Generator.Basic
+25.39%	Mathlib.CategoryTheory.Generator.HomologicalComplex
+16.68%	Mathlib.CategoryTheory.Generator.Indization
+21.82%	Mathlib.CategoryTheory.Generator.Preadditive
+25.99%	Mathlib.CategoryTheory.Generator.Presheaf
+23.54%	Mathlib.CategoryTheory.Generator.Sheaf
+4.53%	Mathlib.CategoryTheory.ObjectProperty.Small
+7.28%	Mathlib.CategoryTheory.Presentable.CardinalFilteredPresentation
+7.27%	Mathlib.CategoryTheory.Presentable.LocallyPresentable

Import changes for modified files

Dependency changes

File	Base Count	Head Count	Change
Mathlib.CategoryTheory.Generator.Basic	757	954	+197 (+26.02%)
Mathlib.CategoryTheory.Generator.Presheaf	758	955	+197 (+25.99%)
Mathlib.CategoryTheory.Generator.HomologicalComplex	776	973	+197 (+25.39%)
Mathlib.CategoryTheory.Adjunction.AdjointFunctorTheorems	772	962	+190 (+24.61%)
Mathlib.CategoryTheory.Generator.Sheaf	790	976	+186 (+23.54%)
Mathlib.CategoryTheory.Generator.Preadditive	848	1033	+185 (+21.82%)
Mathlib.CategoryTheory.Generator.Indization	965	1126	+161 (+16.68%)
Mathlib.CategoryTheory.Presentable.CardinalFilteredPresentation	893	958	+65 (+7.28%)
Mathlib.CategoryTheory.Presentable.LocallyPresentable	894	959	+65 (+7.27%)
Mathlib.CategoryTheory.ObjectProperty.Small	397	415	+18 (+4.53%)
Mathlib.Algebra.Category.ModuleCat.Presheaf.Generator	1348	1380	+32 (+2.37%)
Mathlib.CategoryTheory.Comma.StructuredArrow.Small	483	472	-11 (-2.28%)
Mathlib.Algebra.Category.ModuleCat.AB	1357	1381	+24 (+1.77%)
Mathlib.CategoryTheory.Abelian.GrothendieckCategory.EnoughInjectives	1141	1149	+8 (+0.70%)
Mathlib.CategoryTheory.Abelian.GrothendieckCategory.ModuleEmbedding.GabrielPopescu	1458	1466	+8 (+0.55%)

Import changes for all files

Files	Import difference
Mathlib.CategoryTheory.Comma.StructuredArrow.Small	-11
Mathlib.CategoryTheory.ObjectProperty.ColimitsOfShape Mathlib.CategoryTheory.ObjectProperty.LimitsOfShape	1
Mathlib.CategoryTheory.Abelian.FreydMitchell	7
6 files 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	8
Mathlib.CategoryTheory.ObjectProperty.Small	18
3 files Mathlib.Algebra.Category.ModuleCat.AB Mathlib.Condensed.AB Mathlib.Condensed.Light.AB	24
Mathlib.Algebra.Category.ModuleCat.Sheaf.PullbackContinuous	26
Mathlib.Algebra.Category.ModuleCat.Presheaf.Generator Mathlib.Algebra.Category.ModuleCat.Presheaf.Pullback	32
Mathlib.CategoryTheory.Abelian.Yoneda	39
Mathlib.CategoryTheory.Presentable.CardinalFilteredPresentation Mathlib.CategoryTheory.Presentable.LocallyPresentable	65
Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Sheaf	102
Mathlib.CategoryTheory.Abelian.GrothendieckCategory.Monomorphisms	109
Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Indization	148
Mathlib.Algebra.Homology.GrothendieckAbelian Mathlib.CategoryTheory.Abelian.GrothendieckCategory.Basic	155
Mathlib.CategoryTheory.Generator.Indization	161
Mathlib.CategoryTheory.Generator.Abelian	178
Mathlib.CategoryTheory.Generator.Preadditive	185
Mathlib.CategoryTheory.Generator.Sheaf	186
Mathlib.CategoryTheory.Adjunction.AdjointFunctorTheorems	190
3 files Mathlib.CategoryTheory.Generator.Basic Mathlib.CategoryTheory.Generator.HomologicalComplex Mathlib.CategoryTheory.Generator.Presheaf	197
Mathlib.CategoryTheory.ObjectProperty.CompleteLattice (new file)	400
Mathlib.CategoryTheory.Functor.KanExtension.DenseAt (new file)	466
Mathlib.CategoryTheory.Generator.StrongGenerator (new file)	956
Mathlib.CategoryTheory.Functor.KanExtension.Dense (new file)	968

---

Declarations diff

+ ColimitOfShape.isCardinalPresentable
+ CostructuredArrow.isSeparating_proj_preimage
+ DenseAt
+ DenseAt.ofIso
+ DenseAt.ofNatIso
+ DenseAt.postcompEquivalence
+ DenseAt.precompEquivalence
+ EssentiallySmall
+ EssentiallySmall.exists_small
+ EssentiallySmall.exists_small_le
+ EssentiallySmall.of_le
+ HasCardinalFilteredGenerator
+ HasCardinalFilteredGenerator.exists_small_generator
+ IsCardinalFilteredGenerator
+ IsCodetecting.of_le
+ IsCoseparating.mk_of_exists_limitsOfShape
+ IsCoseparating.mk_of_exists_mono
+ IsCoseparating.mono_productTo
+ IsCoseparating.of_equivalence
+ IsCoseparating.of_le
+ IsDense
+ IsDense.of_fullyFaithful_restrictedULiftYoneda
+ IsDetecting.of_le
+ IsSeparating.epi_coproductFrom
+ IsSeparating.mk_of_exists_colimitsOfShape
+ IsSeparating.mk_of_exists_epi
+ IsSeparating.of_equivalence
+ IsSeparating.of_le
+ IsStrongGenerator
+ IsStrongGenerator.mk_of_exists_colimitsOfShape
+ ObjectProperty.IsCardinalFilteredGenerator.hasCardinalFilteredGenerator
+ ObjectProperty.IsSeparating.isSeparator_coproduct
+ StructuredArrow.isCoseparating_proj_preimage
+ congr_isDenseAt
+ coproductFrom
+ coproductFromFamily
+ denseAt
+ exists_of_mono_not_isIso
+ exists_of_subobject_ne_top
+ extremalEpi_coproductFrom
+ instance (P : ObjectProperty C) [ObjectProperty.EssentiallySmall.{w} P] :
+ instance (P : ObjectProperty C) [ObjectProperty.Small.{w} P] :
+ instance : (isCardinalPresentable C κ).IsClosedUnderIsomorphisms
+ instance : E.isPointwiseLeftKanExtensionAt.IsClosedUnderIsomorphisms
+ instance : E.isPointwiseRightKanExtensionAt.IsClosedUnderIsomorphisms
+ instance : F.isDenseAt.IsClosedUnderIsomorphisms := by
+ instance : ObjectProperty.Small.{u} (freeYoneda R) := by
+ instance [F.IsDense] : (restrictedULiftYoneda.{w} F).Faithful
+ instance [F.IsDense] : (restrictedULiftYoneda.{w} F).Full
+ instance [P.IsClosedUnderIsomorphisms] [Q.IsClosedUnderIsomorphisms] :
+ instance [Small.{w} C] [LocallySmall.{w} D] : Small.{w} (CostructuredArrow S T)
+ instance [Small.{w} C] [LocallySmall.{w} D] : Small.{w} (StructuredArrow S T)
+ instance [∀ a, (P a).IsClosedUnderIsomorphisms] :
+ instance {P Q : ObjectProperty C}
+ instance {P Q : ObjectProperty C} [ObjectProperty.Small.{w} P] :
+ instance {P Q : ObjectProperty C} [ObjectProperty.Small.{w} P] [ObjectProperty.Small.{w} Q] :
+ instance {P Q : ObjectProperty C} [ObjectProperty.Small.{w} Q] :
+ isCardinalPresentable
+ isCardinalPresentable_iff
+ isCardinalPresentable_monotone
+ isClosedUnderIsomorphisms_iff_isoClosure_eq_self
+ isCodetecting_bot_of_isGroupoid
+ isCoseparating_bot_of_isThin
+ isCoseparating_inverseImage_proj
+ isCoseparator_iff_of_isLimit_fan
+ isCoseparator_of_isLimit_fan
+ isDenseAt
+ isDenseAt_eq_isPointwiseLeftKanExtensionAt
+ isDense_iff_fullyFaithful_restrictedULiftYoneda
+ isDense_iff_nonempty_isPointwiseLeftKanExtension
+ isDetecting_bot_of_isGroupoid
+ isGroupoid_of_isCodetecting_bot
+ isGroupoid_of_isDetecting_bot
+ isIso_of_mono
+ isPointwiseLeftKanExtensionAt
+ isPointwiseRightKanExtensionAt
+ isSeparating_bot_of_isThin
+ isSeparating_inverseImage_proj
+ isSeparator_iff_of_isColimit_cofan
+ isStrongGenerator
+ isStrongGenerator_iff
+ isStrongGenerator_iff_exists_extremalEpi
+ isStrongGenerator_of_isDense
+ isThin_of_isCoseparating_bot
+ isThin_of_isSeparating_bot
+ isoClosure
+ isoClosure_iSup
+ isoClosure_iff
+ isoClosure_sup
+ mk_of_exists_extremalEpi
+ of_le_isoClosure
+ productTo
+ productToFamily
+ prop_iSup_iff
+ prop_inf_iff
+ prop_sup_iff
+ subobject_eq_top
+ ιCoproductFrom
+ πProductTo
++ hom_ext'
++ instance {α : Type*} (P : α → ObjectProperty C)
++ 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
- J
- colimitPresentation
- exists_colimitPresentation_diag_obj_iso
- instance (j : h.J X) :
- instance (j : h.J X) : IsPresentable.{w} ((h.colimitPresentation X).diag.obj j)
- instance : IsCardinalFiltered (h.J X) κ
- instance : Small.{u} (freeYoneda R) := by
- instance : SmallCategory (h.J X)
- isCoseparating_proj_preimage
- isPresentable
- 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:

• feat(CategoryTheory): dense functors #29565
• refactor(CategoryTheory/Generator): use ObjectProperty instead of Set #30269
• [Merged by Bors] - feat(CategoryTheory): functors that are dense at an object #29556
• feat(CategoryTheory): strong generators #29519
• feat(CategoryTheory): a property of objects is a strong generator if any object is a colimit of objects satisfying the property #29543
• feat(CategoryTheory/ObjectProperty): closure of a property under certain limits #29854
• refactor(CategoryTheory/ObjectProperty): IsClosedUnderLimitsOfShape #29881
• [Merged by Bors] - chore(CategoryTheory): split Limits.Presentation #29903
  By Dependent Issues (🤖). Happy coding!

[mathlib4-merge-conflict-bot]

This pull request has conflicts, please merge master and resolve them.