feat(CategoryTheory): κ-continuous presheaves

[joelriou]

Given categories C, D and a regular cardinal κ : Cardinal.{w}, we define isCardinalContinuous C D κ : ObjectProperty (C ⥤ D) as the property of functors which preserves limits indexed by categories J such that HasCardinalLT (Arrow J) κ.

When C : Type w is a small category, we show that κ-continuous functors Cᵒᵖ ⥤ Type w are exactly the objects that are local with respect to a suitable w-small family of morphisms.

DRAFT

---

• depends on: feat(CategoryTheory): presheaves of types which preserve a limit #32725
• 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): 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

[mathlib4-merge-conflict-bot]

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

[mathlib4-merge-conflict-bot]

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

[mathlib4-dependent-issues-bot]

This PR/issue depends on:

• feat(CategoryTheory): presheaves of types which preserve a limit #32725
• [Merged by Bors] - feat(CategoryTheory): more preservation properties of functors #32423
• [Merged by Bors] - feat(CategoryTheory): the Yoneda embedding for a locally small category #32424
• [Merged by Bors] - feat(CategoryTheory): closure under bounded colimits #30168
• [Merged by Bors] - feat(CategoryTheory/ObjectProperty): closure of a property under certain colimits #30160
• [Merged by Bors] - refactor(CategoryTheory/ObjectProperty): IsClosedUnderLimitsOfShape #29881
• [Merged by Bors] - feat(CategoryTheory/ObjectProperty): closure of a property under certain limits #29854
  By Dependent Issues (🤖). Happy coding!

[mathlib-merge-conflicts]

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