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

[joelriou]

Given a regular cardinal κ : Cardinal.{u}, we show that the category CardinalFilteredPoset κ of κ-directed partially ordered types (with order embeddings as morphisms) is a κ-accessible category.

---

• depends on: feat(CategoryTheory): the category of κ-directed posets #39669

[github-actions]

PR summary bde3f62a80

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.ι
+ Hom.injective
+ Hom.le_iff_le
+ cocone
+ coconeWithTop
+ hasCardinalLTWithTerminal
+ 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 (S : indexSet J) : HasTerminal S := S.prop.2
+ instance (S : indexSet J) : IsCardinalFiltered S κ := isCardinalFiltered_of_hasTerminal _ _
+ instance : (forget PartOrdEmb.{u}).ReflectsIsomorphisms
+ instance : (isCardinalFiltered κ).IsClosedUnderIsomorphisms
+ instance : HasCardinalFilteredColimits (CardinalFilteredPoset κ) κ
+ instance : IsCardinalAccessibleCategory (CardinalFilteredPoset κ) κ
+ instance : IsCardinalFiltered (indexSet J h) κ'
+ instance : IsCardinalFiltered (indexSet J) κ
+ instance : IsFiltered (indexSet J h) := isFiltered_of_isCardinalFiltered _ κ'
+ instance : IsFiltered (indexSet J) := isFiltered_of_isCardinalFiltered _ κ
+ instance : ObjectProperty.EssentiallySmall.{u} (hasCardinalLTWithTerminal κ)
+ instance : ReflectsColimitsOfShape J (forget PartOrdEmb.{u})
+ isCardinalFiltered
+ isCardinalFilteredGenerator_hasCardinalLTWithTerminal
+ isCardinalFiltered_iff
+ isCardinalFiltered_pt
+ isCardinalPresentable_iff
+ isCardinalPresentable_iff'
+ isCardinalPresentable_of_hasCardinalLT_of_le
+ isColimitCocone
+ isColimitCoconeWithTop
+ of
+ orderIsoOfIso
+ pair_mem_indexSet
+ singleton_mem_indexSet
+ withTop
++ functor
++ indexSet

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.

[mathlib-dependent-issues]

This PR/issue depends on:

• feat(CategoryTheory): the category of κ-directed posets #39669
  By Dependent Issues (🤖). Happy coding!