feat(CategoryTheory/Presentable): the uniformization theorem

[joelriou]

The main result in this PR is IsCardinalAccessibleCategory.uniformization which says that if F : C ⥤ D is an accessible functor between accessible categories, there exists a regular cardinal κ such that C and D are κ-accessible categories, and F is a κ-accessible functor which preserves κ-presentable objects.

---

• depends on: feat(CategoryTheory/Presentable): lemmas about sharply smaller regular cardinals #42761
• depends on: [Merged by Bors] - feat(CategoryTheory/Presentable): equivalence between the various definitions of sharply smaller regular cardinals #41232
• depends on: [Merged by Bors] - feat(CategoryTheory/Presentable): sharply smaller regular cardinals #40937
• depends on: [Merged by Bors] - feat(CategoryTheory): the category of κ-directed posets #39669
• depends on: [Merged by Bors] - feat(CategoryTheory): the κ-accessible category of κ-directed posets #39655
• depends on: [Merged by Bors] - feat(CategoryTheory/Presentable): presentable objects in Type #30727
• depends on: [Merged by Bors] - feat(CategoryTheory): a category with a terminal object is κ-filtered #31767
• depends on: [Merged by Bors] - feat(CategoryTheory): strong generators #29519
• 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): dense functors #29565
• depends on: [Merged by Bors] - feat(CategoryTheory/ObjectProperty): closure of a property under certain limits #29854
• depends on: [Merged by Bors] - refactor(CategoryTheory/Presentable): cleaning up HasCardinalFilteredGenerator(s) #30459
• depends on: [Merged by Bors] - feat(CategoryTheory): for any filtered category, there exists a final functor from a directed poset #30605
• depends on: [Merged by Bors] - feat(CategoryTheory): DiagramWithUniqueTerminal #31426
• depends on: [Merged by Bors] - feat(CategoryTheory): HasCardinalLT for MorphismProperty and ObjectProperty #31421
• depends on: [Merged by Bors] - feat(SetTheory): more API for HasCardinalLT #30633
• depends on: [Merged by Bors] - feat(CategoryTheory): κ-filtered categories are stable under products #30634
• depends on: [Merged by Bors] - feat(Order/Category): partial orders with order embeddings as morphisms #30693
• depends on: [Merged by Bors] - feat(Order/Category): PartOrdEmb has filtered colimits #30696
• depends on: [Merged by Bors] - feat(CategoryTheory): characterization of κ-filtered categories #30781

[mathlib-merge-conflicts]

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

[mathlib-dependent-issues]

This PR/issue depends on:

• feat(CategoryTheory/Presentable): lemmas about sharply smaller regular cardinals #42761
• [Merged by Bors] - feat(CategoryTheory/Presentable): equivalence between the various definitions of sharply smaller regular cardinals #41232
• [Merged by Bors] - feat(CategoryTheory/Presentable): sharply smaller regular cardinals #40937
• [Merged by Bors] - feat(CategoryTheory): the category of κ-directed posets #39669
• [Merged by Bors] - feat(CategoryTheory): the κ-accessible category of κ-directed posets #39655
• [Merged by Bors] - feat(CategoryTheory/Presentable): presentable objects in Type #30727
• [Merged by Bors] - feat(CategoryTheory): a category with a terminal object is κ-filtered #31767
• [Merged by Bors] - feat(CategoryTheory): strong generators #29519
• [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
• [Merged by Bors] - feat(CategoryTheory): dense functors #29565
• [Merged by Bors] - feat(CategoryTheory/ObjectProperty): closure of a property under certain limits #29854
• [Merged by Bors] - refactor(CategoryTheory/Presentable): cleaning up HasCardinalFilteredGenerator(s) #30459
• [Merged by Bors] - feat(CategoryTheory): for any filtered category, there exists a final functor from a directed poset #30605
• [Merged by Bors] - feat(CategoryTheory): DiagramWithUniqueTerminal #31426
• [Merged by Bors] - feat(CategoryTheory): HasCardinalLT for MorphismProperty and ObjectProperty #31421
• [Merged by Bors] - feat(SetTheory): more API for HasCardinalLT #30633
• [Merged by Bors] - feat(CategoryTheory): κ-filtered categories are stable under products #30634
• [Merged by Bors] - feat(Order/Category): partial orders with order embeddings as morphisms #30693
• [Merged by Bors] - feat(Order/Category): PartOrdEmb has filtered colimits #30696
• [Merged by Bors] - feat(CategoryTheory): characterization of κ-filtered categories #30781
  By Dependent Issues (🤖). Happy coding!