Principal upper sets of large posets

Content created by Egbert Rijke.

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

module order-theory.principal-upper-sets-large-posets where
Imports 
open import foundation.dependent-pair-types
open import foundation.identity-types
open import foundation.logical-equivalences
open import foundation.universe-levels

open import order-theory.large-posets
open import order-theory.large-subposets
open import order-theory.large-subpreorders
open import order-theory.similarity-of-elements-large-posets

Idea

The principal upper set ↑{x} of an element x of a large poset P is the large subposet consisting of all elements x ≤ y in P.

Two elements x and y in a large poset P are similar if and only if they have the same principal upper sets, and if x and y are of the same universe level, then x and y are equal if and only if they have the same principal upper sets. To see this, note that if ↑{x} = ↑{y}, then we have the implications (x ≤ x) → (x ≤ y) and (y ≤ y) → (y ≤ x).

Definitions

The predicate of being a principal upper set of an element

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

  is-principal-upper-set-Large-Subposet : UUω
  is-principal-upper-set-Large-Subposet =
    {l : Level} (y : type-Large-Poset P l) →
    leq-Large-Poset P y x ↔ is-in-Large-Subposet P S y

The principal upper set of an element

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

  large-subpreorder-principal-upper-set-element-Large-Poset :
    Large-Subpreorder (λ l → β l1 l) (large-preorder-Large-Poset P)
  large-subpreorder-principal-upper-set-element-Large-Poset y =
    leq-prop-Large-Poset P x y

  is-closed-under-sim-principal-upper-set-element-Large-Poset :
    is-closed-under-sim-Large-Subpreorder P
      ( large-subpreorder-principal-upper-set-element-Large-Poset)
  is-closed-under-sim-principal-upper-set-element-Large-Poset y z p q l =
    transitive-leq-Large-Poset P x y z p l

  principal-upper-set-element-Large-Poset : Large-Subposet (λ l → β l1 l) P
  large-subpreorder-Large-Subposet principal-upper-set-element-Large-Poset =
    large-subpreorder-principal-upper-set-element-Large-Poset
  is-closed-under-sim-Large-Subposet principal-upper-set-element-Large-Poset =
    is-closed-under-sim-principal-upper-set-element-Large-Poset

Properties

The principal upper sets ↑{x} and ↑{y} have the same elements if and only if x and y are similar

module _
  {α : Level → Level} {β : Level → Level → Level} (P : Large-Poset α β)
  {l1 l2 : Level} {x : type-Large-Poset P l1} {y : type-Large-Poset P l2}
  where

  sim-has-same-elements-principal-upper-set-element-Large-Poset :
    has-same-elements-Large-Subposet P
      ( principal-upper-set-element-Large-Poset P x)
      ( principal-upper-set-element-Large-Poset P y) →
    sim-Large-Poset P x y
  pr1 (sim-has-same-elements-principal-upper-set-element-Large-Poset H) =
    backward-implication (H y) (refl-leq-Large-Poset P y)
  pr2 (sim-has-same-elements-principal-upper-set-element-Large-Poset H) =
    forward-implication (H x) (refl-leq-Large-Poset P x)

  has-same-elements-principal-upper-set-element-sim-Large-Poset :
    sim-Large-Poset P x y →
    has-same-elements-Large-Subposet P
      ( principal-upper-set-element-Large-Poset P x)
      ( principal-upper-set-element-Large-Poset P y)
  pr1
    ( has-same-elements-principal-upper-set-element-sim-Large-Poset (H , K) z)
    ( p) =
    transitive-leq-Large-Poset P y x z p K
  pr2
    ( has-same-elements-principal-upper-set-element-sim-Large-Poset (H , K) z)
    ( q) =
    transitive-leq-Large-Poset P x y z q H

For two elements x and y of a large poset of the same universe level, if the principal upper sets ↑{x} and ↑{y} have the same elements, then x and y are equal

module _
  {α : Level → Level} {β : Level → Level → Level} (P : Large-Poset α β)
  {l1 : Level} (x y : type-Large-Poset P l1)
  where

  eq-has-same-elements-principal-upper-set-element-Large-Poset :
    has-same-elements-Large-Subposet P
      ( principal-upper-set-element-Large-Poset P x)
      ( principal-upper-set-element-Large-Poset P y) →
    x ＝ y
  eq-has-same-elements-principal-upper-set-element-Large-Poset H =
    antisymmetric-leq-Large-Poset P x y
      ( pr1 (sim-has-same-elements-principal-upper-set-element-Large-Poset P H))
      ( pr2 (sim-has-same-elements-principal-upper-set-element-Large-Poset P H))

Recent changes