feat(CategoryTheory): the category of κ-directed posets

[joelriou]

Given a regular cardinal κ : Cardinal.{u}, we define the category CardinalFilteredPoset κ of κ-directed partially ordered types (with order embeddings as morphisms). In a future PR #39655, we shall show that it is a κ-accessible category.
In this PR, we also show that if J : CardinalFilteredPoset κ, the object J.withTop obtained by adding a top element is a κ'-filtered colimit of objects of cardinality < κ' (when κ' is a regular cardinal such that κ ≤ κ'). This shall be used in #39655 in order to characterize κ'-presentable objects in CardinalFilteredPoset κ as the objects that are of cardinality < κ'.

---

[github-actions]

PR summary 8702bdc64b

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference
Mathlib.CategoryTheory.Presentable.CardinalDirectedPoset (new file)	1008

---

Declarations diff

+ CardinalFilteredPoset
+ CardinalFilteredPoset.ι
+ coconeWithTop
+ functor
+ indexSet
+ instance (A : Type u) [SmallCategory A] [IsCardinalFiltered A κ] :
+ instance (J : CardinalFilteredPoset κ) (κ' : Cardinal.{u}) [Fact κ'.IsRegular] :
+ instance (J : CardinalFilteredPoset κ) : IsCardinalFiltered J.obj κ := J.property
+ instance (J : CardinalFilteredPoset κ) : IsFiltered J.obj
+ instance (J : CardinalFilteredPoset κ) : Nonempty J.obj := IsFiltered.nonempty
+ instance (J : Type u) [SmallCategory J] [IsCardinalFiltered J κ] :
+ instance (S : indexSet J h) : HasTerminal S
+ instance (S : indexSet J h) : IsCardinalFiltered S κ := isCardinalFiltered_of_hasTerminal _ _
+ instance : (forget PartOrdEmb.{u}).ReflectsIsomorphisms
+ instance : (isCardinalFiltered κ).IsClosedUnderIsomorphisms
+ instance : HasCardinalFilteredColimits (CardinalFilteredPoset κ) κ
+ instance : IsCardinalFiltered (indexSet J h) κ'
+ instance : IsFiltered (indexSet J h) := isFiltered_of_isCardinalFiltered _ κ'
+ instance : ReflectsColimitsOfShape J (forget PartOrdEmb.{u})
+ isCardinalFiltered
+ isCardinalFiltered_iff
+ isCardinalFiltered_pt
+ isColimitCoconeWithTop
+ of
+ orderIsoOfIso
+ pair_mem_indexSet
+ withTop

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.

---

No changes to strong technical debt.

No changes to weak technical debt.

[dagurtomas]

Thanks!

maintainer delegate

[dagurtomas]

Maybe add a small comment explaining the nolint: isColimitCoconeWithTop wouldn't work without the unused arguments

[dagurtomas]

Can you put together Iso.mk and orderIsoOfIso into an equivalence (α ≃o β) ≃ (α ≅ β)?

[github-actions]

🚀 Pull request has been placed on the maintainer queue by dagurtomas.