Upper bounds in posets

module order-theory.upper-bounds-posets where
Imports
open import foundation.dependent-pair-types
open import foundation.propositions
open import foundation.universe-levels

open import order-theory.posets

Idea

An upper bound of two elements x and y in a poset P is an element z such that both x ≤ z and y ≤ z hold. Similaryly, an upper bound of a family x : I → P of elements in P is an element z such that x i ≤ z holds for every i : I.

Definitions

Binary upper bounds

module _
  {l1 l2 : Level} (P : Poset l1 l2)
  where

  is-binary-upper-bound-Poset-Prop :
    (x y z : type-Poset P)  Prop l2
  is-binary-upper-bound-Poset-Prop x y z =
    prod-Prop (leq-Poset-Prop P x z) (leq-Poset-Prop P y z)

  is-binary-upper-bound-Poset :
    (x y z : type-Poset P)  UU l2
  is-binary-upper-bound-Poset x y z =
    type-Prop (is-binary-upper-bound-Poset-Prop x y z)

  is-prop-is-binary-upper-bound-Poset :
    (x y z : type-Poset P)  is-prop (is-binary-upper-bound-Poset x y z)
  is-prop-is-binary-upper-bound-Poset x y z =
    is-prop-type-Prop (is-binary-upper-bound-Poset-Prop x y z)

module _
  {l1 l2 : Level} (P : Poset l1 l2) {a b x : type-Poset P}
  (H : is-binary-upper-bound-Poset P a b x)
  where

  leq-left-is-binary-upper-bound-Poset : leq-Poset P a x
  leq-left-is-binary-upper-bound-Poset = pr1 H

  leq-right-is-binary-upper-bound-Poset : leq-Poset P b x
  leq-right-is-binary-upper-bound-Poset = pr2 H

Upper bounds of families of elements

module _
  {l1 l2 : Level} (P : Poset l1 l2)
  where

  is-upper-bound-family-of-elements-Poset-Prop :
    {l : Level} {I : UU l}  (I  type-Poset P)  type-Poset P 
    Prop (l2  l)
  is-upper-bound-family-of-elements-Poset-Prop {l} {I} f z =
    Π-Prop I  i  leq-Poset-Prop P (f i) z)

  is-upper-bound-family-of-elements-Poset :
    {l : Level} {I : UU l}  (I  type-Poset P)  type-Poset P 
    UU (l2  l)
  is-upper-bound-family-of-elements-Poset f z =
    type-Prop (is-upper-bound-family-of-elements-Poset-Prop f z)

  is-prop-is-upper-bound-family-of-elements-Poset :
    {l : Level} {I : UU l} (f : I  type-Poset P) (z : type-Poset P) 
    is-prop (is-upper-bound-family-of-elements-Poset f z)
  is-prop-is-upper-bound-family-of-elements-Poset f z =
    is-prop-type-Prop (is-upper-bound-family-of-elements-Poset-Prop f z)

Properties

Any element greater than an upper bound of a and b is an upper bound of a and b

module _
  {l1 l2 : Level} (P : Poset l1 l2) {a b x : type-Poset P}
  (H : is-binary-upper-bound-Poset P a b x)
  where

  is-binary-upper-bound-leq-Poset :
    {y : type-Poset P} 
    leq-Poset P x y  is-binary-upper-bound-Poset P a b y
  pr1 (is-binary-upper-bound-leq-Poset K) =
    transitive-leq-Poset P a x _
      ( K)
      ( leq-left-is-binary-upper-bound-Poset P H)
  pr2 (is-binary-upper-bound-leq-Poset K) =
    transitive-leq-Poset P b x _
      ( K)
      ( leq-right-is-binary-upper-bound-Poset P H)

Any element greater than an upper bound of a family of elements a is an upper bound of a

module _
  {l1 l2 l3 : Level} (P : Poset l1 l2) {I : UU l3} {a : I  type-Poset P}
  {x : type-Poset P} (H : is-upper-bound-family-of-elements-Poset P a x)
  where

  is-upper-bound-family-of-elements-leq-Poset :
    {y : type-Poset P}  leq-Poset P x y 
    is-upper-bound-family-of-elements-Poset P a y
  is-upper-bound-family-of-elements-leq-Poset K i =
    transitive-leq-Poset P (a i) x _ K (H i)