Commit 2026-05-28 18:39 937da144
View on Github →feat(CategoryTheory): the category of κ-directed posets (#39669)
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 < κ'.