Lower sets in large posets

Content created by Egbert Rijke.

Created on 2023-11-24.
Last modified on 2023-11-24.

module order-theory.lower-sets-large-posets where
Imports 
open import foundation.universe-levels

open import order-theory.large-posets
open import order-theory.large-subposets

Idea

A lower set or downwards closed set in a large poset is a large subposet that is downwards closed, i.e., that satisfies the condition that

  ∀ (x y : P), (y ≤ x) → x ∈ S → y ∈ S.

Definitions

The predicate of being a lower set

module _
  {α γ : Level → Level} {β : Level → Level → Level}
  (P : Large-Poset α β) (S : Large-Subposet γ P)
  where

  is-lower-set-Large-Subposet : UUω
  is-lower-set-Large-Subposet =
    {l1 l2 : Level} (x : type-Large-Poset P l1) (y : type-Large-Poset P l2) →
    leq-Large-Poset P y x →
    is-in-Large-Subposet P S x → is-in-Large-Subposet P S y

Lower sets of a large poset

module _
  {α : Level → Level} {β : Level → Level → Level} (γ : Level → Level)
  (P : Large-Poset α β)
  where

  record
    lower-set-Large-Poset : UUω
    where
    field
      large-subposet-lower-set-Large-Poset :
        Large-Subposet γ P
      is-lower-set-lower-set-Large-Poset :
        is-lower-set-Large-Subposet P large-subposet-lower-set-Large-Poset

  open lower-set-Large-Poset public

module _
  {α γ : Level → Level} {β : Level → Level → Level}
  (P : Large-Poset α β) (L : lower-set-Large-Poset γ P)
  where

  is-in-lower-set-Large-Poset :
    {l : Level} (x : type-Large-Poset P l) → UU (γ l)
  is-in-lower-set-Large-Poset =
    is-in-Large-Subposet P (large-subposet-lower-set-Large-Poset L)

See also

Recent changes