# Greatest lower bounds in posets

Content created by Fredrik Bakke, Egbert Rijke and Jonathan Prieto-Cubides.

Created on 2022-03-24.

module order-theory.greatest-lower-bounds-posets where

Imports
open import foundation.action-on-identifications-functions
open import foundation.dependent-pair-types
open import foundation.identity-types
open import foundation.logical-equivalences
open import foundation.propositions
open import foundation.subtypes
open import foundation.universe-levels

open import order-theory.lower-bounds-posets
open import order-theory.posets


## Idea

A greatest lower bound of a and b in a poset P is an element x such that the logical equivalence

  ((y ≤ a) ∧ (y ≤ b)) ⇔ (y ≤ x)


holds for every element y in P. Similarly, a greatest lower bound of a family a : I → P of elements of P is an element x of P such that the logical equivalence

  (∀ᵢ (y ≤ aᵢ)) ⇔ (y ≤ x)


holds for every element y in P.

## Definitions

### The predicate of being a greatest binary lower bound of two elements in a poset

module _
{l1 l2 : Level} (P : Poset l1 l2) (a b : type-Poset P)
where

is-greatest-binary-lower-bound-Poset-Prop : type-Poset P → Prop (l1 ⊔ l2)
is-greatest-binary-lower-bound-Poset-Prop x =
Π-Prop
( type-Poset P)
( λ y →
iff-Prop
( is-binary-lower-bound-Poset-Prop P a b y)
( leq-Poset-Prop P y x))

is-greatest-binary-lower-bound-Poset : type-Poset P → UU (l1 ⊔ l2)
is-greatest-binary-lower-bound-Poset x =
type-Prop (is-greatest-binary-lower-bound-Poset-Prop x)

is-prop-is-greatest-binary-lower-bound-Poset :
(x : type-Poset P) →
is-prop (is-greatest-binary-lower-bound-Poset x)
is-prop-is-greatest-binary-lower-bound-Poset x =
is-prop-type-Prop (is-greatest-binary-lower-bound-Poset-Prop x)

module _
{l1 l2 : Level} (P : Poset l1 l2) {a b : type-Poset P}
where

forward-implication-is-greatest-binary-lower-bound-Poset :
{x y : type-Poset P} →
is-greatest-binary-lower-bound-Poset P a b x →
is-binary-lower-bound-Poset P a b y → leq-Poset P y x
forward-implication-is-greatest-binary-lower-bound-Poset {x} {y} H =
forward-implication (H y)

backward-implication-is-greatest-binary-lower-bound-Poset :
{x y : type-Poset P} →
is-greatest-binary-lower-bound-Poset P a b x →
leq-Poset P y x → is-binary-lower-bound-Poset P a b y
backward-implication-is-greatest-binary-lower-bound-Poset {x} {y} H =
backward-implication (H y)

prove-is-greatest-binary-lower-bound-Poset :
{x : type-Poset P} →
is-binary-lower-bound-Poset P a b x →
( (y : type-Poset P) →
is-binary-lower-bound-Poset P a b y → leq-Poset P y x) →
is-greatest-binary-lower-bound-Poset P a b x
pr1 (prove-is-greatest-binary-lower-bound-Poset H K y) L = K y L
pr2 (prove-is-greatest-binary-lower-bound-Poset H K y) L =
is-binary-lower-bound-leq-Poset P H L

is-binary-lower-bound-is-greatest-binary-lower-bound-Poset :
{x : type-Poset P} →
is-greatest-binary-lower-bound-Poset P a b x →
is-binary-lower-bound-Poset P a b x
is-binary-lower-bound-is-greatest-binary-lower-bound-Poset {x} H =
backward-implication-is-greatest-binary-lower-bound-Poset H
( refl-leq-Poset P x)

leq-left-is-greatest-binary-lower-bound-Poset :
{x : type-Poset P} →
is-greatest-binary-lower-bound-Poset P a b x →
leq-Poset P x a
leq-left-is-greatest-binary-lower-bound-Poset H =
leq-left-is-binary-lower-bound-Poset P
( is-binary-lower-bound-is-greatest-binary-lower-bound-Poset H)

leq-right-is-greatest-binary-lower-bound-Poset :
{x : type-Poset P} →
is-greatest-binary-lower-bound-Poset P a b x →
leq-Poset P x b
leq-right-is-greatest-binary-lower-bound-Poset H =
leq-right-is-binary-lower-bound-Poset P
( is-binary-lower-bound-is-greatest-binary-lower-bound-Poset H)


### The proposition that two elements have a greatest lower bound

module _
{l1 l2 : Level} (P : Poset l1 l2) (a b : type-Poset P)
where

has-greatest-binary-lower-bound-Poset : UU (l1 ⊔ l2)
has-greatest-binary-lower-bound-Poset =
Σ (type-Poset P) (is-greatest-binary-lower-bound-Poset P a b)

all-elements-equal-has-greatest-binary-lower-bound-Poset :
all-elements-equal has-greatest-binary-lower-bound-Poset
all-elements-equal-has-greatest-binary-lower-bound-Poset
(pair u H) (pair v K) =
eq-type-subtype
( is-greatest-binary-lower-bound-Poset-Prop P a b)
( antisymmetric-leq-Poset P u v
( forward-implication-is-greatest-binary-lower-bound-Poset P K
( is-binary-lower-bound-is-greatest-binary-lower-bound-Poset P H))
( forward-implication-is-greatest-binary-lower-bound-Poset P H
( is-binary-lower-bound-is-greatest-binary-lower-bound-Poset P K)))

is-prop-has-greatest-binary-lower-bound-Poset :
is-prop has-greatest-binary-lower-bound-Poset
is-prop-has-greatest-binary-lower-bound-Poset =
is-prop-all-elements-equal
all-elements-equal-has-greatest-binary-lower-bound-Poset

has-greatest-binary-lower-bound-Poset-Prop : Prop (l1 ⊔ l2)
pr1 has-greatest-binary-lower-bound-Poset-Prop =
has-greatest-binary-lower-bound-Poset
pr2 has-greatest-binary-lower-bound-Poset-Prop =
is-prop-has-greatest-binary-lower-bound-Poset

module _
{l1 l2 : Level} (P : Poset l1 l2) {a b : type-Poset P}
where

eq-is-greatest-binary-lower-bound-Poset :
{x y : type-Poset P} →
is-greatest-binary-lower-bound-Poset P a b x →
is-greatest-binary-lower-bound-Poset P a b y →
x ＝ y
eq-is-greatest-binary-lower-bound-Poset {x} {y} H K =
ap
( pr1)
( all-elements-equal-has-greatest-binary-lower-bound-Poset P a b
( x , H)
( y , K))


### Greatest lower bounds of families of elements

module _
{l1 l2 l3 : Level} (P : Poset l1 l2) {I : UU l3} (a : I → type-Poset P)
where

is-greatest-lower-bound-family-of-elements-Poset-Prop :
type-Poset P → Prop (l1 ⊔ l2 ⊔ l3)
is-greatest-lower-bound-family-of-elements-Poset-Prop x =
Π-Prop
( type-Poset P)
( λ y →
iff-Prop
( Π-Prop I (λ i → leq-Poset-Prop P y (a i)))
( leq-Poset-Prop P y x))

is-greatest-lower-bound-family-of-elements-Poset :
type-Poset P → UU (l1 ⊔ l2 ⊔ l3)
is-greatest-lower-bound-family-of-elements-Poset z =
type-Prop (is-greatest-lower-bound-family-of-elements-Poset-Prop z)

is-prop-is-greatest-lower-bound-family-of-elements-Poset :
(z : type-Poset P) →
is-prop (is-greatest-lower-bound-family-of-elements-Poset z)
is-prop-is-greatest-lower-bound-family-of-elements-Poset z =
is-prop-type-Prop (is-greatest-lower-bound-family-of-elements-Poset-Prop z)

module _
{l1 l2 l3 : Level} (P : Poset l1 l2) {I : UU l3} {a : I → type-Poset P}
where

forward-implication-is-greatest-lower-bound-family-of-elements-Poset :
{x y : type-Poset P} →
is-greatest-lower-bound-family-of-elements-Poset P a x →
((i : I) → leq-Poset P y (a i)) → leq-Poset P y x
forward-implication-is-greatest-lower-bound-family-of-elements-Poset
{ x} {y} H =
forward-implication (H y)

backward-implication-is-greatest-lower-bound-family-of-elements-Poset :
{x y : type-Poset P} →
is-greatest-lower-bound-family-of-elements-Poset P a x →
leq-Poset P y x → (i : I) → leq-Poset P y (a i)
backward-implication-is-greatest-lower-bound-family-of-elements-Poset
{x} {y} H =
backward-implication (H y)

is-lower-bound-is-greatest-lower-bound-family-of-elements-Poset :
{x : type-Poset P} →
is-greatest-lower-bound-family-of-elements-Poset P a x →
is-lower-bound-family-of-elements-Poset P a x
is-lower-bound-is-greatest-lower-bound-family-of-elements-Poset {x} H =
backward-implication-is-greatest-lower-bound-family-of-elements-Poset H
( refl-leq-Poset P x)


### The proposition that a family of elements has a greatest lower bound

module _
{l1 l2 l3 : Level} (P : Poset l1 l2) {I : UU l3} (a : I → type-Poset P)
where

has-greatest-lower-bound-family-of-elements-Poset : UU (l1 ⊔ l2 ⊔ l3)
has-greatest-lower-bound-family-of-elements-Poset =
Σ (type-Poset P) (is-greatest-lower-bound-family-of-elements-Poset P a)

all-elements-equal-has-greatest-lower-bound-family-of-elements-Poset :
all-elements-equal has-greatest-lower-bound-family-of-elements-Poset
all-elements-equal-has-greatest-lower-bound-family-of-elements-Poset
( x , H) (y , K) =
eq-type-subtype
( is-greatest-lower-bound-family-of-elements-Poset-Prop P a)
( antisymmetric-leq-Poset P x y
( forward-implication-is-greatest-lower-bound-family-of-elements-Poset
( P)
( K)
( is-lower-bound-is-greatest-lower-bound-family-of-elements-Poset
( P)
( H)))
( forward-implication-is-greatest-lower-bound-family-of-elements-Poset
( P)
( H)
( is-lower-bound-is-greatest-lower-bound-family-of-elements-Poset
( P)
( K))))

is-prop-has-greatest-lower-bound-family-of-elements-Poset :
is-prop has-greatest-lower-bound-family-of-elements-Poset
is-prop-has-greatest-lower-bound-family-of-elements-Poset =
is-prop-all-elements-equal
all-elements-equal-has-greatest-lower-bound-family-of-elements-Poset

has-greatest-lower-bound-family-of-elements-Poset-Prop : Prop (l1 ⊔ l2 ⊔ l3)
pr1 has-greatest-lower-bound-family-of-elements-Poset-Prop =
has-greatest-lower-bound-family-of-elements-Poset
pr2 has-greatest-lower-bound-family-of-elements-Poset-Prop =
is-prop-has-greatest-lower-bound-family-of-elements-Poset

module _
{l1 l2 l3 : Level} (P : Poset l1 l2) {I : UU l3} {a : I → type-Poset P}
where

eq-is-greatest-lower-bound-family-of-elements-Poset :
{x y : type-Poset P} →
is-greatest-lower-bound-family-of-elements-Poset P a x →
is-greatest-lower-bound-family-of-elements-Poset P a y →
x ＝ y
eq-is-greatest-lower-bound-family-of-elements-Poset {x} {y} H K =
ap
( pr1)
( all-elements-equal-has-greatest-lower-bound-family-of-elements-Poset
( P)
( a)
( x , H)
( y , K))