The κ-accessible category of κ-directed posets

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

The notion of κ-directed partially ordered type is implemented using the categorial notion IsCardinalFiltered: we may consider "κ-directed" and "κ-filtered" as synonyms.

If κ ≤ κ' where κ' is also a regular cardinal, we characterize the κ'-presentable objects of CardinalDirectedPoset κ as the objects J such that the underlying type J.obj has cardinality < κ'.

References

• Adámek, J. and Rosický, J., Locally presentable and accessible categories

@[reducible, inline]

abbrev PartOrdEmb.isCardinalFiltered (κ : Cardinal.{u}) [Fact κ.IsRegular] : CategoryTheory.ObjectProperty PartOrdEmb

The property of objects in PartOrdEmb that are satisfied by κ-directed partially ordered types. (Note: for partially ordered types, "κ-directed" and "κ-filtered" are synonyms. This is implemented using the categorical notion IsCardinalFiltered.)

Equations

• PartOrdEmb.isCardinalFiltered κ X = CategoryTheory.IsCardinalFiltered (↑X) κ

@[simp]

theorem PartOrdEmb.isCardinalFiltered_iff (κ : Cardinal.{u}) [Fact κ.IsRegular] (X : PartOrdEmb) : isCardinalFiltered κ X ↔ CategoryTheory.IsCardinalFiltered (↑X) κ

instance PartOrdEmb.instIsClosedUnderIsomorphismsIsCardinalFiltered (κ : Cardinal.{u}) [Fact κ.IsRegular] : (isCardinalFiltered κ).IsClosedUnderIsomorphisms

theorem PartOrdEmb.Limits.CoconePt.isCardinalFiltered_pt {κ : Cardinal.{u}} [Fact κ.IsRegular] {J : Type u} [CategoryTheory.SmallCategory J] [CategoryTheory.IsCardinalFiltered J κ] {F : CategoryTheory.Functor J PartOrdEmb} {c : CategoryTheory.Limits.Cocone (F.comp (CategoryTheory.forget PartOrdEmb))} (hc : CategoryTheory.Limits.IsColimit c) (hF : ∀ (j : J), CategoryTheory.IsCardinalFiltered (↑(F.obj j)) κ) : CategoryTheory.IsCardinalFiltered (CoconePt hc) κ

instance PartOrdEmb.instIsClosedUnderColimitsOfShapeIsCardinalFilteredOfIsCardinalFiltered (κ : Cardinal.{u}) [Fact κ.IsRegular] (J : Type u) [CategoryTheory.SmallCategory J] [CategoryTheory.IsCardinalFiltered J κ] : (isCardinalFiltered κ).IsClosedUnderColimitsOfShape J

@[reducible, inline]

abbrev CategoryTheory.CardinalDirectedPoset (κ : Cardinal.{u}) [Fact κ.IsRegular] : Type (u + 1)

The category of κ-filtered partially ordered types, with morphisms given by order embeddings.

Equations

• CategoryTheory.CardinalDirectedPoset κ = (PartOrdEmb.isCardinalFiltered κ).FullSubcategory

@[reducible, inline]

abbrev CategoryTheory.CardinalDirectedPoset.ι {κ : Cardinal.{u}} [Fact κ.IsRegular] : Functor (CardinalDirectedPoset κ) PartOrdEmb

The embedding of the category of κ-directed partially ordered types in the category of partially ordered types.

Equations

• CategoryTheory.CardinalDirectedPoset.ι = (PartOrdEmb.isCardinalFiltered κ).ι

@[reducible, inline]

abbrev CategoryTheory.CardinalDirectedPoset.of {κ : Cardinal.{u}} [Fact κ.IsRegular] (J : PartOrdEmb) [IsCardinalFiltered (↑J) κ] : CardinalDirectedPoset κ

Constructor for objects in CardinalFilteredPoset κ.

Equations

• CategoryTheory.CardinalDirectedPoset.of J = { obj := J, property := ⋯ }

theorem CategoryTheory.CardinalDirectedPoset.Hom.injective {κ : Cardinal.{u}} [Fact κ.IsRegular] {J₁ J₂ : CardinalDirectedPoset κ} (f : J₁ ⟶ J₂) : Function.Injective ⇑(ConcreteCategory.hom f)

theorem CategoryTheory.CardinalDirectedPoset.Hom.le_iff_le {κ : Cardinal.{u}} [Fact κ.IsRegular] {J₁ J₂ : CardinalDirectedPoset κ} (f : J₁ ⟶ J₂) (x₁ x₂ : ↑J₁.obj) : (ConcreteCategory.hom f) x₁ ≤ (ConcreteCategory.hom f) x₂ ↔ x₁ ≤ x₂

instance CategoryTheory.CardinalDirectedPoset.instIsCardinalFilteredCarrierObjPartOrdEmbIsCardinalFiltered {κ : Cardinal.{u}} [Fact κ.IsRegular] (J : CardinalDirectedPoset κ) : IsCardinalFiltered (↑J.obj) κ

instance CategoryTheory.CardinalDirectedPoset.instIsFilteredCarrierObjPartOrdEmbIsCardinalFiltered {κ : Cardinal.{u}} [Fact κ.IsRegular] (J : CardinalDirectedPoset κ) : IsFiltered ↑J.obj

instance CategoryTheory.CardinalDirectedPoset.instNonemptyCarrierObjPartOrdEmbIsCardinalFiltered {κ : Cardinal.{u}} [Fact κ.IsRegular] (J : CardinalDirectedPoset κ) : Nonempty ↑J.obj

instance CategoryTheory.CardinalDirectedPoset.instHasCardinalFilteredColimits {κ : Cardinal.{u}} [Fact κ.IsRegular] : HasCardinalFilteredColimits (CardinalDirectedPoset κ) κ

instance CategoryTheory.CardinalDirectedPoset.instPreservesColimitsOfShapeForgetOrderEmbeddingCarrierObjPartOrdEmbIsCardinalFilteredOfIsCardinalFiltered {κ : Cardinal.{u}} [Fact κ.IsRegular] (A : Type u) [SmallCategory A] [IsCardinalFiltered A κ] : Limits.PreservesColimitsOfShape A (forget (CardinalDirectedPoset κ))

instance CategoryTheory.CardinalDirectedPoset.instIsCardinalFilteredWithTopCarrierObjPartOrdEmbIsCardinalFiltered {κ : Cardinal.{u}} [Fact κ.IsRegular] (J : CardinalDirectedPoset κ) (κ' : Cardinal.{u}) [Fact κ'.IsRegular] : IsCardinalFiltered (WithTop ↑J.obj) κ'

@[reducible, inline]

abbrev CategoryTheory.CardinalDirectedPoset.withTop {κ : Cardinal.{u}} [Fact κ.IsRegular] (J : CardinalDirectedPoset κ) : CardinalDirectedPoset κ

The map CardinalDirectedPoset κ → CardinalDirectedPoset κ which sends a partially ordered κ-filtered type J to WithTop J.

Equations

• J.withTop = CategoryTheory.CardinalDirectedPoset.of { carrier := WithTop ↑J.obj, str := WithTop.instPartialOrder }

def CategoryTheory.CardinalDirectedPoset.functorOfPredicateSet {κ : Cardinal.{u}} [Fact κ.IsRegular] {J : CardinalDirectedPoset κ} (P : Set ↑J.obj → Prop) [∀ (S : Subtype P), IsCardinalFiltered (↑↑S) κ] : Functor (Subtype P) (CardinalDirectedPoset κ)

Given a predicate P : Set J.obj → Prop on the underlying type of J : CardinalDirectedPoset κ such that all the subsets satisfying P are κ-filtered, this is the functor Subtype P ⥤ CardinalDirectedPoset κ which sends a subset S of J satisfying P to the induced partially ordered type J, as an object in CardinalDirectedPoset κ.

Equations

• CategoryTheory.CardinalDirectedPoset.functorOfPredicateSet P = (PartOrdEmb.isCardinalFiltered κ).lift (PartOrdEmb.functorOfPredicateSet P) ⋯

@[simp]

theorem CategoryTheory.CardinalDirectedPoset.functorOfPredicateSet_obj_obj_coe {κ : Cardinal.{u}} [Fact κ.IsRegular] {J : CardinalDirectedPoset κ} (P : Set ↑J.obj → Prop) [∀ (S : Subtype P), IsCardinalFiltered (↑↑S) κ] (X : Subtype P) : ↑((functorOfPredicateSet P).obj X).obj = ↑↑X

@[simp]

theorem CategoryTheory.CardinalDirectedPoset.functorOfPredicateSet_map_hom_hom_apply_coe {κ : Cardinal.{u}} [Fact κ.IsRegular] {J : CardinalDirectedPoset κ} (P : Set ↑J.obj → Prop) [∀ (S : Subtype P), IsCardinalFiltered (↑↑S) κ] {X✝ Y✝ : Subtype P} (f : X✝ ⟶ Y✝) (x : ↑↑X✝) : ↑((PartOrdEmb.Hom.hom ((functorOfPredicateSet P).map f).hom) x) = ↑x

def CategoryTheory.CardinalDirectedPoset.coconeOfPredicateSet {κ : Cardinal.{u}} [Fact κ.IsRegular] {J : CardinalDirectedPoset κ} (P : Set ↑J.obj → Prop) [∀ (S : Subtype P), IsCardinalFiltered (↑↑S) κ] : Limits.Cocone (functorOfPredicateSet P)

Given a predicate P : Set J.obj → Prop on the underlying type of J : CardinalDirectedPoset κ such that all the subsets satisfying P are κ-filtered, this is the cocone with point J given by all the inclusions of the subsets satisfying P.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem CategoryTheory.CardinalDirectedPoset.coconeOfPredicateSet_ι_app {κ : Cardinal.{u}} [Fact κ.IsRegular] {J : CardinalDirectedPoset κ} (P : Set ↑J.obj → Prop) [∀ (S : Subtype P), IsCardinalFiltered (↑↑S) κ] (j : Subtype P) : (coconeOfPredicateSet P).ι.app j = ObjectProperty.homMk ((PartOrdEmb.coconeOfPredicateSet P).ι.app j)

@[simp]

theorem CategoryTheory.CardinalDirectedPoset.coconeOfPredicateSet_pt {κ : Cardinal.{u}} [Fact κ.IsRegular] {J : CardinalDirectedPoset κ} (P : Set ↑J.obj → Prop) [∀ (S : Subtype P), IsCardinalFiltered (↑↑S) κ] : (coconeOfPredicateSet P).pt = J

noncomputable def CategoryTheory.CardinalDirectedPoset.isColimitCoconeOfPredicateSet {κ : Cardinal.{u}} [Fact κ.IsRegular] {J : CardinalDirectedPoset κ} (P : Set ↑J.obj → Prop) [IsDirectedOrder (Subtype P)] [Nonempty (Subtype P)] [∀ (S : Subtype P), IsCardinalFiltered (↑↑S) κ] (hP : ∀ (a : ↑J.obj), ∃ (S : Set ↑J.obj), P S ∧ a ∈ S) : Limits.IsColimit (coconeOfPredicateSet P)

Let P be a predicate on Set J.obj where J : CardinalDirectedPoset κ. We assume that Subtype P is directed and nonempty, and that any a : J.obj belongs to some S : Set J.obj satisfying P. Then, J is the colimit in the category CardinalDirectedPoset κ of these subsets.

Equations

• One or more equations did not get rendered due to their size.

def CategoryTheory.CardinalDirectedPoset.hasCardinalLTWithTerminal (κ : Cardinal.{u}) [Fact κ.IsRegular] : ObjectProperty (CardinalDirectedPoset κ)

The property of posets in CardinalDirectedPoset κ that are of cardinality < κ and have terminal object.

Equations

• CategoryTheory.CardinalDirectedPoset.hasCardinalLTWithTerminal κ J = (HasCardinalLT (↑J.obj) κ ∧ CategoryTheory.Limits.HasTerminal ↑J.obj)

instance CategoryTheory.CardinalDirectedPoset.instEssentiallySmallHasCardinalLTWithTerminal {κ : Cardinal.{u}} [Fact κ.IsRegular] : ObjectProperty.EssentiallySmall.{u, u, u + 1} (hasCardinalLTWithTerminal κ)

theorem CategoryTheory.CardinalDirectedPoset.isCardinalPresentable_of_hasCardinalLT_of_le {κ : Cardinal.{u}} [Fact κ.IsRegular] (J : CardinalDirectedPoset κ) {κ' : Cardinal.{u}} [Fact κ'.IsRegular] (hJ : HasCardinalLT (↑J.obj) κ') (h : κ ≤ κ') : IsCardinalPresentable J κ'

def CategoryTheory.CardinalDirectedPoset.PropSetWithTop {κ : Cardinal.{u}} [Fact κ.IsRegular] (J : CardinalDirectedPoset κ) (κ' : Cardinal.{u}) [Fact κ'.IsRegular] (S : Set ↑J.withTop.obj) : Prop

Given J : CardinalFilteredPoset κ and a regular cardinal κ', this is the predicate on Set J.withTop.obj that is satisfied by subsets that are of cardinality < κ' and contain ⊤.

Equations

• J.PropSetWithTop κ' S = (HasCardinalLT (↑S) κ' ∧ ⊤ ∈ S)

instance CategoryTheory.CardinalDirectedPoset.instHasTerminalElemCarrierObjPartOrdEmbIsCardinalFilteredWithTopValSetPropSetWithTop {κ : Cardinal.{u}} [Fact κ.IsRegular] (J : CardinalDirectedPoset κ) (κ' : Cardinal.{u}) [Fact κ'.IsRegular] (S : Subtype (J.PropSetWithTop κ')) : Limits.HasTerminal ↑↑S

instance CategoryTheory.CardinalDirectedPoset.instIsCardinalFilteredElemCarrierObjPartOrdEmbIsCardinalFilteredWithTopValSetPropSetWithTop {κ : Cardinal.{u}} [Fact κ.IsRegular] (J : CardinalDirectedPoset κ) (κ' : Cardinal.{u}) [Fact κ'.IsRegular] (S : Subtype (J.PropSetWithTop κ')) : IsCardinalFiltered (↑↑S) κ

instance CategoryTheory.CardinalDirectedPoset.instIsCardinalFilteredSubtypeSetCarrierObjPartOrdEmbIsCardinalFilteredWithTopPropSetWithTop {κ : Cardinal.{u}} [Fact κ.IsRegular] (J : CardinalDirectedPoset κ) (κ' : Cardinal.{u}) [Fact κ'.IsRegular] : IsCardinalFiltered (Subtype (J.PropSetWithTop κ')) κ'

instance CategoryTheory.CardinalDirectedPoset.instIsFilteredSubtypeSetCarrierObjPartOrdEmbIsCardinalFilteredWithTopPropSetWithTop {κ : Cardinal.{u}} [Fact κ.IsRegular] (J : CardinalDirectedPoset κ) (κ' : Cardinal.{u}) [Fact κ'.IsRegular] : IsFiltered (Subtype (J.PropSetWithTop κ'))

instance CategoryTheory.CardinalDirectedPoset.instIsDirectedOrderSubtypeSetCarrierObjPartOrdEmbIsCardinalFilteredWithTopPropSetWithTop {κ : Cardinal.{u}} [Fact κ.IsRegular] (J : CardinalDirectedPoset κ) (κ' : Cardinal.{u}) [Fact κ'.IsRegular] : IsDirectedOrder (Subtype (J.PropSetWithTop κ'))

instance CategoryTheory.CardinalDirectedPoset.instNonemptySubtypeSetCarrierObjPartOrdEmbIsCardinalFilteredWithTopPropSetWithTop {κ : Cardinal.{u}} [Fact κ.IsRegular] (J : CardinalDirectedPoset κ) (κ' : Cardinal.{u}) [Fact κ'.IsRegular] : Nonempty (Subtype (J.PropSetWithTop κ'))

theorem CategoryTheory.CardinalDirectedPoset.propSetWithTop_pair {κ : Cardinal.{u}} [Fact κ.IsRegular] {J : CardinalDirectedPoset κ} (κ' : Cardinal.{u}) [Fact κ'.IsRegular] (j : ↑J.obj) : J.PropSetWithTop κ' {↑j, ⊤}

theorem CategoryTheory.CardinalDirectedPoset.exists_mem_propSetWithTop {κ : Cardinal.{u}} [Fact κ.IsRegular] (J : CardinalDirectedPoset κ) (κ' : Cardinal.{u}) [Fact κ'.IsRegular] (a : ↑J.withTop.obj) : ∃ (S : Set ↑J.withTop.obj), J.PropSetWithTop κ' S ∧ a ∈ S

@[reducible, inline]

abbrev CategoryTheory.CardinalDirectedPoset.coconeWithTop {κ : Cardinal.{u}} [Fact κ.IsRegular] (J : CardinalDirectedPoset κ) (κ' : Cardinal.{u}) [Fact κ'.IsRegular] : Limits.Cocone (functorOfPredicateSet (J.PropSetWithTop κ'))

If J : CardinalFilteredPoset κ and κ' is any regular cardinal, this is a colimit cocone which exhibits J.withTop as the κ'-filtered colimit of its subsets that are of cardinality < κ' and contain ⊤.

Equations

• J.coconeWithTop κ' = CategoryTheory.CardinalDirectedPoset.coconeOfPredicateSet (J.PropSetWithTop κ')

noncomputable def CategoryTheory.CardinalDirectedPoset.isColimitCoconeWithTop {κ : Cardinal.{u}} [Fact κ.IsRegular] (J : CardinalDirectedPoset κ) (κ' : Cardinal.{u}) [Fact κ'.IsRegular] : Limits.IsColimit (J.coconeWithTop κ')

If J : CardinalDirectedPoset κ and κ' is any regular cardinal, then J.withTop is the κ'-filtered colimit of its subsets that are of cardinality < κ' and contain ⊤.

Equations

• J.isColimitCoconeWithTop κ' = CategoryTheory.CardinalDirectedPoset.isColimitCoconeOfPredicateSet (J.PropSetWithTop κ') ⋯

theorem CategoryTheory.CardinalDirectedPoset.isCardinalPresentable_iff {κ : Cardinal.{u}} [Fact κ.IsRegular] (J : CardinalDirectedPoset κ) {κ' : Cardinal.{u}} [Fact κ'.IsRegular] (h : κ ≤ κ') : IsCardinalPresentable J κ' ↔ HasCardinalLT (↑J.obj) κ'

theorem CategoryTheory.CardinalDirectedPoset.isCardinalPresentable_iff' {κ : Cardinal.{u}} [Fact κ.IsRegular] (J : CardinalDirectedPoset κ) : IsCardinalPresentable J κ ↔ HasCardinalLT (↑J.obj) κ

def CategoryTheory.CardinalDirectedPoset.PropSet {κ : Cardinal.{u}} [Fact κ.IsRegular] (J : CardinalDirectedPoset κ) (S : Set ↑J.obj) : Prop

Given J : CardinalDirectedPoset κ, this is the predicate on Set J.obj that is satisfied by subsets that are of cardinality < κ and have a terminal object.

Equations

• J.PropSet S = (HasCardinalLT (↑S) κ ∧ CategoryTheory.Limits.HasTerminal ↑S)

instance CategoryTheory.CardinalDirectedPoset.instHasTerminalElemCarrierObjPartOrdEmbIsCardinalFilteredValSetPropSet {κ : Cardinal.{u}} [Fact κ.IsRegular] (J : CardinalDirectedPoset κ) (S : Subtype J.PropSet) : Limits.HasTerminal ↑↑S

instance CategoryTheory.CardinalDirectedPoset.instIsCardinalFilteredElemCarrierObjPartOrdEmbIsCardinalFilteredValSetPropSet {κ : Cardinal.{u}} [Fact κ.IsRegular] (J : CardinalDirectedPoset κ) (S : Subtype J.PropSet) : IsCardinalFiltered (↑↑S) κ

theorem CategoryTheory.CardinalDirectedPoset.propSet_singleton {κ : Cardinal.{u}} [Fact κ.IsRegular] {J : CardinalDirectedPoset κ} (j : ↑J.obj) : J.PropSet {j}

instance CategoryTheory.CardinalDirectedPoset.instIsCardinalFilteredSubtypeSetCarrierObjPartOrdEmbIsCardinalFilteredPropSet {κ : Cardinal.{u}} [Fact κ.IsRegular] (J : CardinalDirectedPoset κ) : IsCardinalFiltered (Subtype J.PropSet) κ

instance CategoryTheory.CardinalDirectedPoset.instIsFilteredSubtypeSetCarrierObjPartOrdEmbIsCardinalFilteredPropSet {κ : Cardinal.{u}} [Fact κ.IsRegular] (J : CardinalDirectedPoset κ) : IsFiltered (Subtype J.PropSet)

instance CategoryTheory.CardinalDirectedPoset.instIsDirectedOrderSubtypeSetCarrierObjPartOrdEmbIsCardinalFilteredPropSet {κ : Cardinal.{u}} [Fact κ.IsRegular] (J : CardinalDirectedPoset κ) : IsDirectedOrder (Subtype J.PropSet)

instance CategoryTheory.CardinalDirectedPoset.instNonemptySubtypeSetCarrierObjPartOrdEmbIsCardinalFilteredPropSet {κ : Cardinal.{u}} [Fact κ.IsRegular] (J : CardinalDirectedPoset κ) : Nonempty (Subtype J.PropSet)

@[reducible, inline]

abbrev CategoryTheory.CardinalDirectedPoset.cocone {κ : Cardinal.{u}} [Fact κ.IsRegular] (J : CardinalDirectedPoset κ) : Limits.Cocone (functorOfPredicateSet J.PropSet)

For any object J : CardinalDirectedPoset κ, this is a colimit cocone exhibiting J as the colimit of its subsets that are of cardinality < κ and have a terminal object.

Equations

• J.cocone = CategoryTheory.CardinalDirectedPoset.coconeOfPredicateSet J.PropSet

noncomputable def CategoryTheory.CardinalDirectedPoset.isColimitCocone {κ : Cardinal.{u}} [Fact κ.IsRegular] (J : CardinalDirectedPoset κ) : Limits.IsColimit J.cocone

Any object J : CardinalDirectedPoset κ is a colimit of its subsets that are of cardinality < κ and have a terminal object.

Equations

• J.isColimitCocone = CategoryTheory.CardinalDirectedPoset.isColimitCoconeOfPredicateSet J.PropSet ⋯

theorem CategoryTheory.CardinalDirectedPoset.isCardinalFilteredGenerator_hasCardinalLTWithTerminal (κ : Cardinal.{u}) [Fact κ.IsRegular] : (hasCardinalLTWithTerminal κ).IsCardinalFilteredGenerator κ

instance CategoryTheory.CardinalDirectedPoset.instIsCardinalAccessibleCategory {κ : Cardinal.{u}} [Fact κ.IsRegular] : IsCardinalAccessibleCategory (CardinalDirectedPoset κ) κ

@[reducible, inline]

abbrev CategoryTheory.CardinalDirectedPoset.SetCardinalLT (κ : Cardinal.{u}) (X : Type u) : Type u

Given a cardinal κ and a type X, this is the subtype of Set X consisting of subsets of X of cardinality < κ.

Equations

• CategoryTheory.CardinalDirectedPoset.SetCardinalLT κ X = { S : Set X // HasCardinalLT (↑S) κ }

@[reducible, inline]

abbrev CategoryTheory.CardinalDirectedPoset.SetCardinalLT.singleton (κ : Cardinal.{u}) [Fact κ.IsRegular] {X : Type u} (x : X) : SetCardinalLT κ X

Given a regular cardinal κ and x : X, this is the singleton {x}, considered as a subset of X of cardinality < κ.

Equations

• CategoryTheory.CardinalDirectedPoset.SetCardinalLT.singleton κ x = ⟨{x}, ⋯⟩

instance CategoryTheory.CardinalDirectedPoset.instIsCardinalFilteredSetCardinalLT (κ : Cardinal.{u}) [Fact κ.IsRegular] (X : Type u) : IsCardinalFiltered (SetCardinalLT κ X) κ

@[reducible, inline]

abbrev CategoryTheory.CardinalDirectedPoset.setCardinalLT (κ : Cardinal.{u}) [Fact κ.IsRegular] (X : Type u) : CardinalDirectedPoset κ

Given a regular cardinal κ and a type X, this is the κ-filtered partially ordered type of subsets of X of cardinality < κ, as an object of the category CardinalDirectedPoset κ.

Equations

• One or more equations did not get rendered due to their size.

@[deprecated CategoryTheory.CardinalDirectedPoset (since := "2026-06-24")]

def CategoryTheory.CardinalFilteredPoset (κ : Cardinal.{u}) [Fact κ.IsRegular] : Type (u + 1)

Alias of CategoryTheory.CardinalDirectedPoset.

---

The category of κ-filtered partially ordered types, with morphisms given by order embeddings.

Equations

• CategoryTheory.CardinalFilteredPoset = CategoryTheory.CardinalDirectedPoset

@[deprecated CategoryTheory.CardinalDirectedPoset.ι (since := "2026-06-24")]

def CategoryTheory.CardinalFilteredPoset.ι {κ : Cardinal.{u}} [Fact κ.IsRegular] : Functor (CardinalDirectedPoset κ) PartOrdEmb

Alias of CategoryTheory.CardinalDirectedPoset.ι.

---

The embedding of the category of κ-directed partially ordered types in the category of partially ordered types.

Equations

• @CategoryTheory.CardinalFilteredPoset.ι = @CategoryTheory.CardinalDirectedPoset.ι

@[deprecated CategoryTheory.CardinalDirectedPoset.of (since := "2026-06-24")]

def CategoryTheory.CardinalFilteredPoset.of {κ : Cardinal.{u}} [Fact κ.IsRegular] (J : PartOrdEmb) [IsCardinalFiltered (↑J) κ] : CardinalDirectedPoset κ

Alias of CategoryTheory.CardinalDirectedPoset.of.

---

Constructor for objects in CardinalFilteredPoset κ.

Equations

• @CategoryTheory.CardinalFilteredPoset.of = @CategoryTheory.CardinalDirectedPoset.of

@[deprecated CategoryTheory.CardinalDirectedPoset.Hom.injective (since := "2026-06-24")]

theorem CategoryTheory.CardinalFilteredPoset.Hom.injective {κ : Cardinal.{u}} [Fact κ.IsRegular] {J₁ J₂ : CardinalDirectedPoset κ} (f : J₁ ⟶ J₂) : Function.Injective ⇑(ConcreteCategory.hom f)

Alias of CategoryTheory.CardinalDirectedPoset.Hom.injective.

@[deprecated CategoryTheory.CardinalDirectedPoset.Hom.le_iff_le (since := "2026-06-24")]

theorem CategoryTheory.CardinalFilteredPoset.Hom.le_iff_le {κ : Cardinal.{u}} [Fact κ.IsRegular] {J₁ J₂ : CardinalDirectedPoset κ} (f : J₁ ⟶ J₂) (x₁ x₂ : ↑J₁.obj) : (ConcreteCategory.hom f) x₁ ≤ (ConcreteCategory.hom f) x₂ ↔ x₁ ≤ x₂

Alias of CategoryTheory.CardinalDirectedPoset.Hom.le_iff_le.

@[deprecated CategoryTheory.CardinalDirectedPoset.withTop (since := "2026-06-24")]

def CategoryTheory.CardinalFilteredPoset.withTop {κ : Cardinal.{u}} [Fact κ.IsRegular] (J : CardinalDirectedPoset κ) : CardinalDirectedPoset κ

Alias of CategoryTheory.CardinalDirectedPoset.withTop.

---

The map CardinalDirectedPoset κ → CardinalDirectedPoset κ which sends a partially ordered κ-filtered type J to WithTop J.

Equations

• @CategoryTheory.CardinalFilteredPoset.withTop = @CategoryTheory.CardinalDirectedPoset.withTop

@[deprecated CategoryTheory.CardinalDirectedPoset.functorOfPredicateSet (since := "2026-06-24")]

def CategoryTheory.CardinalFilteredPoset.functorOfPredicateSet {κ : Cardinal.{u}} [Fact κ.IsRegular] {J : CardinalDirectedPoset κ} (P : Set ↑J.obj → Prop) [∀ (S : Subtype P), IsCardinalFiltered (↑↑S) κ] : Functor (Subtype P) (CardinalDirectedPoset κ)

Alias of CategoryTheory.CardinalDirectedPoset.functorOfPredicateSet.

---

Given a predicate P : Set J.obj → Prop on the underlying type of J : CardinalDirectedPoset κ such that all the subsets satisfying P are κ-filtered, this is the functor Subtype P ⥤ CardinalDirectedPoset κ which sends a subset S of J satisfying P to the induced partially ordered type J, as an object in CardinalDirectedPoset κ.

Equations

• @CategoryTheory.CardinalFilteredPoset.functorOfPredicateSet = @CategoryTheory.CardinalDirectedPoset.functorOfPredicateSet

@[deprecated CategoryTheory.CardinalDirectedPoset.coconeOfPredicateSet (since := "2026-06-24")]

def CategoryTheory.CardinalFilteredPoset.coconeOfPredicateSet {κ : Cardinal.{u}} [Fact κ.IsRegular] {J : CardinalDirectedPoset κ} (P : Set ↑J.obj → Prop) [∀ (S : Subtype P), IsCardinalFiltered (↑↑S) κ] : Limits.Cocone (CardinalDirectedPoset.functorOfPredicateSet P)

Alias of CategoryTheory.CardinalDirectedPoset.coconeOfPredicateSet.

---

Given a predicate P : Set J.obj → Prop on the underlying type of J : CardinalDirectedPoset κ such that all the subsets satisfying P are κ-filtered, this is the cocone with point J given by all the inclusions of the subsets satisfying P.

Equations

• @CategoryTheory.CardinalFilteredPoset.coconeOfPredicateSet = @CategoryTheory.CardinalDirectedPoset.coconeOfPredicateSet

@[deprecated CategoryTheory.CardinalDirectedPoset.isColimitCoconeOfPredicateSet (since := "2026-06-24")]

def CategoryTheory.CardinalFilteredPoset.isColimitCoconeOfPredicateSet {κ : Cardinal.{u}} [Fact κ.IsRegular] {J : CardinalDirectedPoset κ} (P : Set ↑J.obj → Prop) [IsDirectedOrder (Subtype P)] [Nonempty (Subtype P)] [∀ (S : Subtype P), IsCardinalFiltered (↑↑S) κ] (hP : ∀ (a : ↑J.obj), ∃ (S : Set ↑J.obj), P S ∧ a ∈ S) : Limits.IsColimit (CardinalDirectedPoset.coconeOfPredicateSet P)

Alias of CategoryTheory.CardinalDirectedPoset.isColimitCoconeOfPredicateSet.

---

Let P be a predicate on Set J.obj where J : CardinalDirectedPoset κ. We assume that Subtype P is directed and nonempty, and that any a : J.obj belongs to some S : Set J.obj satisfying P. Then, J is the colimit in the category CardinalDirectedPoset κ of these subsets.

Equations

• @CategoryTheory.CardinalFilteredPoset.isColimitCoconeOfPredicateSet = @CategoryTheory.CardinalDirectedPoset.isColimitCoconeOfPredicateSet

@[deprecated CategoryTheory.CardinalDirectedPoset.hasCardinalLTWithTerminal (since := "2026-06-24")]

def CategoryTheory.CardinalFilteredPoset.hasCardinalLTWithTerminal (κ : Cardinal.{u}) [Fact κ.IsRegular] : ObjectProperty (CardinalDirectedPoset κ)

Alias of CategoryTheory.CardinalDirectedPoset.hasCardinalLTWithTerminal.

---

The property of posets in CardinalDirectedPoset κ that are of cardinality < κ and have terminal object.

Equations

• CategoryTheory.CardinalFilteredPoset.hasCardinalLTWithTerminal = CategoryTheory.CardinalDirectedPoset.hasCardinalLTWithTerminal

@[deprecated CategoryTheory.CardinalDirectedPoset.isCardinalPresentable_of_hasCardinalLT_of_le (since := "2026-06-24")]

theorem CategoryTheory.CardinalFilteredPoset.isCardinalPresentable_of_hasCardinalLT_of_le {κ : Cardinal.{u}} [Fact κ.IsRegular] (J : CardinalDirectedPoset κ) {κ' : Cardinal.{u}} [Fact κ'.IsRegular] (hJ : HasCardinalLT (↑J.obj) κ') (h : κ ≤ κ') : IsCardinalPresentable J κ'

Alias of CategoryTheory.CardinalDirectedPoset.isCardinalPresentable_of_hasCardinalLT_of_le.

@[deprecated CategoryTheory.CardinalDirectedPoset.PropSetWithTop (since := "2026-06-24")]

def CategoryTheory.CardinalFilteredPoset.PropSetWithTop {κ : Cardinal.{u}} [Fact κ.IsRegular] (J : CardinalDirectedPoset κ) (κ' : Cardinal.{u}) [Fact κ'.IsRegular] (S : Set ↑J.withTop.obj) : Prop

Alias of CategoryTheory.CardinalDirectedPoset.PropSetWithTop.

---

Given J : CardinalFilteredPoset κ and a regular cardinal κ', this is the predicate on Set J.withTop.obj that is satisfied by subsets that are of cardinality < κ' and contain ⊤.

Equations

• @CategoryTheory.CardinalFilteredPoset.PropSetWithTop = @CategoryTheory.CardinalDirectedPoset.PropSetWithTop

@[deprecated CategoryTheory.CardinalDirectedPoset.propSetWithTop_pair (since := "2026-06-24")]

theorem CategoryTheory.CardinalFilteredPoset.propSetWithTop_pair {κ : Cardinal.{u}} [Fact κ.IsRegular] {J : CardinalDirectedPoset κ} (κ' : Cardinal.{u}) [Fact κ'.IsRegular] (j : ↑J.obj) : J.PropSetWithTop κ' {↑j, ⊤}

Alias of CategoryTheory.CardinalDirectedPoset.propSetWithTop_pair.

@[deprecated CategoryTheory.CardinalDirectedPoset.exists_mem_propSetWithTop (since := "2026-06-24")]

theorem CategoryTheory.CardinalFilteredPoset.exists_mem_propSetWithTop {κ : Cardinal.{u}} [Fact κ.IsRegular] (J : CardinalDirectedPoset κ) (κ' : Cardinal.{u}) [Fact κ'.IsRegular] (a : ↑J.withTop.obj) : ∃ (S : Set ↑J.withTop.obj), J.PropSetWithTop κ' S ∧ a ∈ S

Alias of CategoryTheory.CardinalDirectedPoset.exists_mem_propSetWithTop.

@[deprecated CategoryTheory.CardinalDirectedPoset.coconeWithTop (since := "2026-06-24")]

def CategoryTheory.CardinalFilteredPoset.coconeWithTop {κ : Cardinal.{u}} [Fact κ.IsRegular] (J : CardinalDirectedPoset κ) (κ' : Cardinal.{u}) [Fact κ'.IsRegular] : Limits.Cocone (CardinalDirectedPoset.functorOfPredicateSet (J.PropSetWithTop κ'))

Alias of CategoryTheory.CardinalDirectedPoset.coconeWithTop.

---

If J : CardinalFilteredPoset κ and κ' is any regular cardinal, this is a colimit cocone which exhibits J.withTop as the κ'-filtered colimit of its subsets that are of cardinality < κ' and contain ⊤.

Equations

• @CategoryTheory.CardinalFilteredPoset.coconeWithTop = @CategoryTheory.CardinalDirectedPoset.coconeWithTop

@[deprecated CategoryTheory.CardinalDirectedPoset.isColimitCoconeWithTop (since := "2026-06-24")]

def CategoryTheory.CardinalFilteredPoset.isColimitCoconeWithTop {κ : Cardinal.{u}} [Fact κ.IsRegular] (J : CardinalDirectedPoset κ) (κ' : Cardinal.{u}) [Fact κ'.IsRegular] : Limits.IsColimit (J.coconeWithTop κ')

Alias of CategoryTheory.CardinalDirectedPoset.isColimitCoconeWithTop.

---

If J : CardinalDirectedPoset κ and κ' is any regular cardinal, then J.withTop is the κ'-filtered colimit of its subsets that are of cardinality < κ' and contain ⊤.

Equations

• @CategoryTheory.CardinalFilteredPoset.isColimitCoconeWithTop = @CategoryTheory.CardinalDirectedPoset.isColimitCoconeWithTop

@[deprecated CategoryTheory.CardinalDirectedPoset.isCardinalPresentable_iff (since := "2026-06-24")]

theorem CategoryTheory.CardinalFilteredPoset.isCardinalPresentable_iff {κ : Cardinal.{u}} [Fact κ.IsRegular] (J : CardinalDirectedPoset κ) {κ' : Cardinal.{u}} [Fact κ'.IsRegular] (h : κ ≤ κ') : IsCardinalPresentable J κ' ↔ HasCardinalLT (↑J.obj) κ'

Alias of CategoryTheory.CardinalDirectedPoset.isCardinalPresentable_iff.

@[deprecated CategoryTheory.CardinalDirectedPoset.isCardinalPresentable_iff' (since := "2026-06-24")]

theorem CategoryTheory.CardinalFilteredPoset.isCardinalPresentable_iff' {κ : Cardinal.{u}} [Fact κ.IsRegular] (J : CardinalDirectedPoset κ) : IsCardinalPresentable J κ ↔ HasCardinalLT (↑J.obj) κ

Alias of CategoryTheory.CardinalDirectedPoset.isCardinalPresentable_iff'.

@[deprecated CategoryTheory.CardinalDirectedPoset.PropSet (since := "2026-06-24")]

def CategoryTheory.CardinalFilteredPoset.PropSet {κ : Cardinal.{u}} [Fact κ.IsRegular] (J : CardinalDirectedPoset κ) (S : Set ↑J.obj) : Prop

Alias of CategoryTheory.CardinalDirectedPoset.PropSet.

---

Given J : CardinalDirectedPoset κ, this is the predicate on Set J.obj that is satisfied by subsets that are of cardinality < κ and have a terminal object.

Equations

• @CategoryTheory.CardinalFilteredPoset.PropSet = @CategoryTheory.CardinalDirectedPoset.PropSet

@[deprecated CategoryTheory.CardinalDirectedPoset.propSet_singleton (since := "2026-06-24")]

theorem CategoryTheory.CardinalFilteredPoset.propSet_singleton {κ : Cardinal.{u}} [Fact κ.IsRegular] {J : CardinalDirectedPoset κ} (j : ↑J.obj) : J.PropSet {j}

Alias of CategoryTheory.CardinalDirectedPoset.propSet_singleton.

@[deprecated CategoryTheory.CardinalDirectedPoset.cocone (since := "2026-06-24")]

def CategoryTheory.CardinalFilteredPoset.cocone {κ : Cardinal.{u}} [Fact κ.IsRegular] (J : CardinalDirectedPoset κ) : Limits.Cocone (CardinalDirectedPoset.functorOfPredicateSet J.PropSet)

Alias of CategoryTheory.CardinalDirectedPoset.cocone.

---

For any object J : CardinalDirectedPoset κ, this is a colimit cocone exhibiting J as the colimit of its subsets that are of cardinality < κ and have a terminal object.

Equations

• @CategoryTheory.CardinalFilteredPoset.cocone = @CategoryTheory.CardinalDirectedPoset.cocone

@[deprecated CategoryTheory.CardinalDirectedPoset.isColimitCocone (since := "2026-06-24")]

def CategoryTheory.CardinalFilteredPoset.isColimitCocone {κ : Cardinal.{u}} [Fact κ.IsRegular] (J : CardinalDirectedPoset κ) : Limits.IsColimit J.cocone

Alias of CategoryTheory.CardinalDirectedPoset.isColimitCocone.

---

Any object J : CardinalDirectedPoset κ is a colimit of its subsets that are of cardinality < κ and have a terminal object.

Equations

• @CategoryTheory.CardinalFilteredPoset.isColimitCocone = @CategoryTheory.CardinalDirectedPoset.isColimitCocone