feat(CategoryTheory/Presentable): the representation theorem

[joelriou]

If C is an essentially w-small category, then the category of κ-continuous functors Cᵒᵖ ⥤ Type w is locally κ-presentable, and any locally κ-presentable category is equivalent to such a category. In particular, we show that a locally κ-presentable category has limits.

This is a draft...

---

• depends on: refactor(CategoryTheory): colimits of representable presheaves #42816
• depends on: feat(CategoryTheory): StructuredArrow.congr #42645
• depends on: feat(CategoryTheory): κ-continuous presheaves #30817
• depends on: [Merged by Bors] - feat(CategoryTheory): presheaves of types which preserve a limit #32725
• depends on: [Merged by Bors] - feat(CategoryTheory/ObjectProperty): preservation of limits is closed under isomorphisms #41036
• depends on: [Merged by Bors] - feat(CategoryTheory): more preservation properties of functors #32423
• depends on: [Merged by Bors] - feat(CategoryTheory): the Yoneda embedding for a locally small category #32424
• depends on: [Merged by Bors] - feat(CategoryTheory): prerequisites for the characterization of locally presentable categories using strong generators #32034
• depends on: [Merged by Bors] - feat(CategoryTheory): an accessible category is essentially large #31137
• depends on: [Merged by Bors] - feat(CategoryTheory): final functors from a κ-filtered category #30795
• depends on: [Merged by Bors] - feat(CategoryTheory): presentable objects form a dense subcategory #30755
• depends on: [Merged by Bors] - feat(CategoryTheory/Presentable): transport via an equivalence #30731
• depends on: [Merged by Bors] - feat(CategoryTheory): localization of locally presentable categories #30554
• depends on: [Merged by Bors] - feat(CategoryTheory): presentable objects and adjunctions #30533
• depends on: [Merged by Bors] - feat(CategoryTheory): prerequisites for the existence of the left adjoint in the orthogonal reflection construction #30513
• depends on: [Merged by Bors] - feat(CategoryTheory): LeftBousfield.W is stable under transfinite compositions #30509
• depends on: [Merged by Bors] - feat(CategoryTheory): MorphismProperty.isLocal is closed under κ-filtered colimits #30507
• depends on: [Merged by Bors] - feat(CategoryTheory): the orthogonal-reflection construction #30492
• depends on: [Merged by Bors] - feat(CategoryTheory): κ-presentable objects in a κ-accessible category is an essentially small category #30464
• depends on: [Merged by Bors] - refactor(CategoryTheory/Presentable): cleaning up HasCardinalFilteredGenerator(s) #30459
• depends on: [Merged by Bors] - refactor(CategoryTheory/Generator): use ObjectProperty instead of Set #30269
• depends on: [Merged by Bors] - feat(CategoryTheory): categories of presheaves are locally presentable #30247
• depends on: [Merged by Bors] - feat(CategoryTheory): locally presentable categories and strong generators #30241
• depends on: [Merged by Bors] - feat(CategoryTheory): closure under bounded colimits #30168
• depends on: [Merged by Bors] - feat(CategoryTheory/ObjectProperty): closure of a property under certain colimits #30160
• depends on: [Merged by Bors] - refactor(CategoryTheory/ObjectProperty): IsClosedUnderLimitsOfShape #29881
• depends on: [Merged by Bors] - feat(CategoryTheory/ObjectProperty): closure of a property under certain limits #29854
• depends on: [Merged by Bors] - feat(CategoryTheory): dense functors #29565
• depends on: [Merged by Bors] - feat(CategoryTheory): a property of objects is a strong generator if any object is a colimit of objects satisfying the property #29543
• depends on: [Merged by Bors] - feat(CategoryTheory): strong generators #29519

[github-actions]

PR summary 50fd6b3413

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference
Mathlib.CategoryTheory.Presentable.Continuous (new file)	1192
Mathlib.CategoryTheory.Presentable.Representation (new file)	1197

---

Declarations diff (regex)

+ _root_.CategoryTheory.Equivalence.shrinkYonedaIsoConjugateYoneda
+ costructuredArrowUliftYonedaEquiv
+ costructuredArrowYonedaEquiv
+ essentiallySmall'
+ exists_presentation_of_isCardinalContinuous
+ hasFiniteLimits
+ hasLimitsOfSize
+ instance (F : Cᵒᵖ ⥤ Type w) :
+ instance (J : Type w) [SmallCategory J] :
+ instance (X : C) :
+ instance (X : C) [IsCardinalPresentable X κ] :
+ instance (κ : Cardinal.{w}) :
+ instance :
+ instance : (isCardinalContinuous C (Type w) κ).ι.IsRightAdjoint := by
+ instance : (isCardinalContinuous Cᵒᵖ (Type w) κ).ι.IsRightAdjoint := by
+ instance : (restrictedShrinkYoneda.{w} F).Faithful := by
+ instance : (restrictedShrinkYoneda.{w} F).Full := by
+ instance : (toCardinalContinuous C κ).EssSurj
+ instance : (toCardinalContinuous C κ).Faithful := by
+ instance : (toCardinalContinuous C κ).Full := by
+ instance : (toCardinalContinuous C κ).IsEquivalence
+ instance : HasLimitsOfSize.{w, w} (isCardinalContinuous Cᵒᵖ (Type w) κ).FullSubcategory := by
+ instance : IsCardinalLocallyPresentable
+ instance : IsCardinalLocallyPresentable (isCardinalContinuous C (Type w) κ).FullSubcategory κ
+ instance : IsLocallyPresentable.{w} (isCardinalContinuous C (Type w) κ).FullSubcategory
+ instance [IsLocallyPresentable.{w} C] : HasColimitsOfSize.{w, w} C := by
+ instance {X : C} {P : Cᵒᵖ ⥤ Type w} :
+ isCardinalContinuous
+ isCardinalContinuous.preservesColimitsOfShape
+ isCardinalContinuousCongrLeft
+ isCardinalContinuousMorphismProperty
+ isCardinalContinuous_eq_isLocal
+ isCardinalContinuous_iff
+ isCardinalContinuous_precomp_iff
+ isCardinalFiltered_costructuredArrow_shrinkYoneda
+ isCardinalFiltered_costructuredArrow_yoneda
+ isCardinalPresentable_isCardinalContinuousMorphismProperty_src_tgt
+ isColimitTautologicalCoconeShrink
+ isColimitTautologicalCoconeShrinkEvaluation
+ restrictedShrinkYoneda
+ restrictedShrinkYonedaCompULiftIso
+ shrinkYonedaCompWhiskeringRightUliftFunctorIso
+ shrinkYonedaEquiv_symm_comp
+ shrinkYonedaFlipObjCompUliftFunctorIso
+ shrinkYonedaIso
+ shrinkYonedaIso_hom
+ shrinkYonedaMap
+ tautologicalCoconeShrink
+ toCardinalContinuous
+ toCardinalContinuousCompIso
+ toCardinalContinuousEquivalence
+ whiskeringLeftObjCompWhiskeringRightObj
++ congr
++ instance (C : Type u) [Category.{v} C] [IsLocallyPresentable.{w} C] :
++ instance (J : SmallCategoryCardinalLT κ)
++ ι

You can run this locally as follows

## from your `mathlib4` directory:
git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci

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

## more verbose report:
../mathlib-ci/scripts/pr_summary/declarations_diff.sh long <optional_commit>

The doc-module for scripts/pr_summary/declarations_diff.sh in the mathlib-ci repository contains some details about this script.

Declarations diff (Lean -- pending)

Computed after the build finishes.

---

Decrease in strong tech debt: (relative, absolute) = (2.95, 0.02)

Current number	Change	Type (strong)
backward.defeqAttrib.useBackward	4252	-46
backward.isDefEq.respectTransparency	4868	13
backward.isDefEq.respectTransparency.types	2493	-12
erw	498	1
adaptation notes	376	-2

Increase in weak tech debt: (relative, absolute) = (2.00, 0.00)

Current number	Change	Type (weak)
exposed public sections	5032	2

Current commit 50fd6b3413
Reference commit 58e016c6f6

This script lives in the mathlib-ci repository. To run it locally, from your mathlib4 directory:

git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci
../mathlib-ci/scripts/reporting/technical-debt-metrics.py 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).

[mathlib-merge-conflicts]

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

[mathlib-merge-conflicts]

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

[mathlib-merge-conflicts]

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

[mathlib-merge-conflicts]

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

[mathlib-bors]

This pull request is now in draft mode. No active bors state needed cleanup.

While this PR remains draft, bors will ignore commands on this PR. Mark it ready for review before using commands like bors r+ or bors try.