feat(CategoryTheory): presentable objects and adjunctions

[joelriou]

If adj : F ⊣ G and G is κ-accessible for a regular cardinal κ, then F preserves κ-presentable objects.

Moreover, if G : D ⥤ C is fully faithful, then D is locally κ-presentable (resp κ-accessible) if D is.

---

• depends on: feat(CategoryTheory): κ-presentable objects in a κ-accessible category is an essentially small category #30464
• depends on: refactor(CategoryTheory/Presentable): cleaning up HasCardinalFilteredGenerator(s) #30459
• 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

[github-actions]

PR summary 45dfe1bcb6

Import changes exceeding 2%

%	File
+2.51%	Mathlib.CategoryTheory.Generator.Basic
+2.45%	Mathlib.CategoryTheory.Generator.HomologicalComplex
+2.24%	Mathlib.CategoryTheory.Generator.Preadditive
+2.50%	Mathlib.CategoryTheory.Generator.Presheaf
+25.00%	Mathlib.CategoryTheory.ObjectProperty.Retract
+4.53%	Mathlib.CategoryTheory.ObjectProperty.Small
+7.75%	Mathlib.CategoryTheory.Presentable.CardinalFilteredPresentation
+7.74%	Mathlib.CategoryTheory.Presentable.LocallyPresentable

Import changes for modified files

Dependency changes

File	Base Count	Head Count	Change
Mathlib.CategoryTheory.ObjectProperty.Retract	368	460	+92 (+25.00%)
Mathlib.CategoryTheory.Presentable.CardinalFilteredPresentation	890	959	+69 (+7.75%)
Mathlib.CategoryTheory.Presentable.LocallyPresentable	891	960	+69 (+7.74%)
Mathlib.CategoryTheory.ObjectProperty.Small	397	415	+18 (+4.53%)
Mathlib.CategoryTheory.Generator.Basic	758	777	+19 (+2.51%)
Mathlib.CategoryTheory.Generator.Presheaf	759	778	+19 (+2.50%)
Mathlib.CategoryTheory.Generator.HomologicalComplex	777	796	+19 (+2.45%)
Mathlib.CategoryTheory.Comma.StructuredArrow.Small	483	472	-11 (-2.28%)
Mathlib.CategoryTheory.Generator.Preadditive	849	868	+19 (+2.24%)
Mathlib.CategoryTheory.Adjunction.AdjointFunctorTheorems	773	786	+13 (+1.68%)
Mathlib.CategoryTheory.Generator.Sheaf	791	804	+13 (+1.64%)
Mathlib.Algebra.Category.ModuleCat.Presheaf.Generator	1350	1362	+12 (+0.89%)

Import changes for all files

Files	Import difference
Mathlib.CategoryTheory.Comma.StructuredArrow.Small	-11
Mathlib.CategoryTheory.Presentable.Basic	1
Mathlib.CategoryTheory.Preadditive.Projective.Internal	3
Mathlib.CategoryTheory.Abelian.GrothendieckCategory.Monomorphisms	4
10 files Mathlib.Algebra.Homology.GrothendieckAbelian Mathlib.CategoryTheory.Abelian.FreydMitchell Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Sheaf Mathlib.CategoryTheory.Abelian.GrothendieckCategory.Basic 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	5
4 files Mathlib.Algebra.Category.ModuleCat.AB Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Indization Mathlib.Condensed.AB Mathlib.Condensed.Light.AB	6
Mathlib.Algebra.Category.ModuleCat.Sheaf.PullbackContinuous Mathlib.CategoryTheory.Generator.Indization	7
Mathlib.CategoryTheory.ObjectProperty.ColimitsOfShape Mathlib.CategoryTheory.ObjectProperty.LimitsOfShape	10
Mathlib.Algebra.Category.ModuleCat.Presheaf.Generator Mathlib.Algebra.Category.ModuleCat.Presheaf.Pullback	12
Mathlib.CategoryTheory.Adjunction.AdjointFunctorTheorems Mathlib.CategoryTheory.Generator.Sheaf	13
Mathlib.CategoryTheory.ObjectProperty.Small	18
6 files Mathlib.CategoryTheory.Abelian.Yoneda Mathlib.CategoryTheory.Generator.Abelian Mathlib.CategoryTheory.Generator.Basic Mathlib.CategoryTheory.Generator.HomologicalComplex Mathlib.CategoryTheory.Generator.Preadditive Mathlib.CategoryTheory.Generator.Presheaf	19
Mathlib.CategoryTheory.Presentable.CardinalFilteredPresentation Mathlib.CategoryTheory.Presentable.LocallyPresentable	69
Mathlib.CategoryTheory.ObjectProperty.Retract	92
Mathlib.CategoryTheory.ObjectProperty.CompleteLattice (new file)	400
Mathlib.CategoryTheory.Functor.KanExtension.DenseAt (new file)	466
Mathlib.CategoryTheory.Adjunction.ReflectiveLimits (new file)	481
Mathlib.CategoryTheory.Generator.StrongGenerator (new file)	779
Mathlib.CategoryTheory.Functor.KanExtension.Dense (new file)	791
Mathlib.CategoryTheory.Presentable.Retracts (new file)	870
Mathlib.CategoryTheory.Presentable.Adjunction (new file)	962

---

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
+ IsCardinalPresentable.exists_eq_of_isColimit
+ IsCardinalPresentable.exists_eq_of_isColimit'
+ IsCardinalPresentable.exists_hom_of_isColimit
+ 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
+ Retract.isCardinalPresentable
+ StructuredArrow.isCoseparating_proj_preimage
+ compUliftCoyonedaIso
+ congr_isDenseAt
+ coproductFrom
+ coproductFromFamily
+ denseAt
+ essentiallySmall_isPresentable
+ exists_of_mono_not_isIso
+ exists_of_subobject_ne_top
+ extremalEpi_coproductFrom
+ hasCardinalFilteredGenerator
+ hasColimitsOfShape
+ hasLimitsOfShape
+ instance (C : Type u) [Category.{v} C]
+ instance (P : ObjectProperty C) [ObjectProperty.EssentiallySmall.{w} P] (F : C ⥤ D) :
+ instance (P : ObjectProperty C) [ObjectProperty.EssentiallySmall.{w} P] :
+ instance (P : ObjectProperty C) [ObjectProperty.Small.{w} P] (F : C ⥤ D) :
+ instance (P : ObjectProperty C) [ObjectProperty.Small.{w} P] :
+ instance (κ : Cardinal.{w}) [Fact κ.IsRegular] :
+ instance : (isCardinalPresentable C κ).IsClosedUnderIsomorphisms
+ instance : E.isPointwiseLeftKanExtensionAt.IsClosedUnderIsomorphisms
+ instance : E.isPointwiseRightKanExtensionAt.IsClosedUnderIsomorphisms
+ instance : F.isDenseAt.IsClosedUnderIsomorphisms := by
+ instance : IsCardinalAccessible (𝟭 C) κ
+ instance : ObjectProperty.Small.{u} (freeYoneda R) := by
+ instance [F.IsDense] : (restrictedULiftYoneda.{w} F).Faithful
+ instance [F.IsDense] : (restrictedULiftYoneda.{w} F).Full
+ instance [IsCardinalPresentable X κ] :
+ instance [ObjectProperty.EssentiallySmall.{w} P] [LocallySmall.{w} C] :
+ instance [P.IsClosedUnderIsomorphisms] [Q.IsClosedUnderIsomorphisms] :
+ instance [PreservesColimitsOfSize.{w, w} F] : F.IsCardinalAccessible κ
+ 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 {E : Type u₃} [Category.{v₃} E] (F : C ⥤ D) (G : D ⥤ E)
+ 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] :
+ isCardinalAccessible
+ isCardinalFilteredGenerator
+ isCardinalLocallyPresentable
+ isCardinalPresentable
+ isCardinalPresentable_iff
+ isCardinalPresentable_iff_isCardinalAccessible_coyoneda_obj
+ isCardinalPresentable_iff_isCardinalAccessible_uliftCoyoneda_obj
+ 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
+ isPresentable_eq_retractClosure
+ isPresentable_leftAdjoint_obj
+ 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
+ retractClosure_isoClosure
+ subobject_eq_top
+ uliftCoyoneda
+ ι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): κ-presentable objects in a κ-accessible category is an essentially small category #30464
• refactor(CategoryTheory/Presentable): cleaning up HasCardinalFilteredGenerator(s) #30459
• 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
  By Dependent Issues (🤖). Happy coding!

[mathlib4-merge-conflict-bot]

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