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 a4c0062efe

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
+ PropSet
+ PropSetWithTop
+ cocone
+ coconeWithTop
+ exists_mem_propSetWithTop
+ 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 : Subtype (J.PropSetWithTop κ')) : HasTerminal S
+ instance (S : Subtype (J.PropSetWithTop κ')) : IsCardinalFiltered S κ
+ instance (S : Subtype J.PropSet) : HasTerminal S := S.prop.2
+ instance (S : Subtype J.PropSet) : IsCardinalFiltered S κ
+ instance : (forget PartOrdEmb.{u}).ReflectsIsomorphisms
+ instance : (isCardinalFiltered κ).IsClosedUnderIsomorphisms
+ instance : HasCardinalFilteredColimits (CardinalFilteredPoset κ) κ
+ instance : IsCardinalAccessibleCategory (CardinalFilteredPoset κ) κ
+ instance : IsCardinalFiltered (Subtype (J.PropSetWithTop κ')) κ'
+ instance : IsCardinalFiltered (Subtype J.PropSet) κ
+ instance : IsDirectedOrder (Subtype (J.PropSetWithTop κ'))
+ instance : IsDirectedOrder (Subtype J.PropSet)
+ instance : IsFiltered (Subtype (J.PropSetWithTop κ'))
+ instance : IsFiltered (Subtype J.PropSet) := isFiltered_of_isCardinalFiltered _ κ
+ instance : Nonempty (Subtype (J.PropSetWithTop κ'))
+ instance : Nonempty (Subtype J.PropSet)
+ 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
+ isColimitCoconeOfPredicateSet
+ isColimitCoconeWithTop
+ isColimitOfPredicateSet
+ of
+ orderIsoEquivIso
+ orderIsoOfIso
+ propSetWithTop_pair
+ propSetWithTop_singleton
+ withTop
++ coconeOfPredicateSet
++ functorOfPredicateSet

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!