The κ-accessible category of κ-directed posets

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

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 partially ordered types of cardinality < κ.

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.CardinalFilteredPoset (κ : Cardinal.{u}) [Fact κ.IsRegular] : Type (u + 1)

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

Equations

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

@[reducible, inline]

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

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

Equations

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

@[reducible, inline]

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

Constructor for objects in CardinalFilteredPoset κ.

Equations

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

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

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

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

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

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

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

@[reducible, inline]

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

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

Equations

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

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

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

Equations

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

@[simp]

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

@[simp]

theorem CategoryTheory.CardinalFilteredPoset.functorOfPredicateSet_map_hom_hom_apply_coe {κ : Cardinal.{u}} [Fact κ.IsRegular] {J : CardinalFilteredPoset κ} (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.CardinalFilteredPoset.coconeOfPredicateSet {κ : Cardinal.{u}} [Fact κ.IsRegular] {J : CardinalFilteredPoset κ} (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 : CardinalFilteredPoset κ 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.CardinalFilteredPoset.coconeOfPredicateSet_ι_app {κ : Cardinal.{u}} [Fact κ.IsRegular] {J : CardinalFilteredPoset κ} (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.CardinalFilteredPoset.coconeOfPredicateSet_pt {κ : Cardinal.{u}} [Fact κ.IsRegular] {J : CardinalFilteredPoset κ} (P : Set ↑J.obj → Prop) [∀ (S : Subtype P), IsCardinalFiltered (↑↑S) κ] : (coconeOfPredicateSet P).pt = J

noncomputable def CategoryTheory.CardinalFilteredPoset.isColimitCoconeOfPredicateSet {κ : Cardinal.{u}} [Fact κ.IsRegular] {J : CardinalFilteredPoset κ} (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 : CardinalFilteredPoset κ. 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 CardinalFilteredPoset κ of these subsets.

Equations

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

def CategoryTheory.CardinalFilteredPoset.PropSetWithTop {κ : Cardinal.{u}} [Fact κ.IsRegular] (J : CardinalFilteredPoset κ) (κ' : 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.CardinalFilteredPoset.instHasTerminalElemCarrierObjPartOrdEmbIsCardinalFilteredWithTopValSetPropSetWithTop {κ : Cardinal.{u}} [Fact κ.IsRegular] (J : CardinalFilteredPoset κ) (κ' : Cardinal.{u}) [Fact κ'.IsRegular] (S : Subtype (J.PropSetWithTop κ')) : Limits.HasTerminal ↑↑S

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

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

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

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

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

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

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

@[reducible, inline]

abbrev CategoryTheory.CardinalFilteredPoset.coconeWithTop {κ : Cardinal.{u}} [Fact κ.IsRegular] (J : CardinalFilteredPoset κ) (κ' : 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.CardinalFilteredPoset.coconeOfPredicateSet (J.PropSetWithTop κ')

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

If J : CardinalFilteredPoset κ 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.CardinalFilteredPoset.isColimitCoconeOfPredicateSet (J.PropSetWithTop κ') ⋯