module Order.Diagram.Lub where

Least upper bounds🔗

A lub $u$ (short for least upper bound) for a family of elements $(a_{i})_{i : I}$ is, as the name implies, a least elemnet among the upper boudns of the $a_{i} .$ Being an upper bound means that we have $a_{i} \leq u$ for all $i : I;$ Being the least upper bound means that if we’re given some other $l$ satisfying $a_{i} \leq l$ (for each $i),$ then we have $u \leq l .$

The same observation about the naming of glbs vs meets applies to lubs, with the binary name being join.

  record is-lub
    {ℓᵢ} {I : Type ℓᵢ} (F : I → Ob) (lub : Ob)
    : Type (o ⊔ ℓ ⊔ ℓᵢ)
    where
    no-eta-equality
    field
      fam≤lub : ∀ i → F i ≤ lub
      least   : (ub' : Ob) → (∀ i → F i ≤ ub') → lub ≤ ub'

  record Lub {ℓᵢ} {I : Type ℓᵢ} (F : I → Ob) : Type (o ⊔ ℓ ⊔ ℓᵢ) where
    no-eta-equality
    field
      lub : Ob
      has-lub : is-lub F lub
    open is-lub has-lub public

Let $f : I \to P$ be a family. If there is some $i$ such that for all $j,$ $f (j) < f (i),$ then $f (i)$ is the least upper bound of $f .$

  fam-bound→is-lub
    : ∀ {ℓᵢ} {I : Type ℓᵢ} {F : I → Ob}
    → (i : I) → (∀ j → F j ≤ F i)
    → is-lub P F (F i)
  fam-bound→is-lub i ge .fam≤lub = ge
  fam-bound→is-lub i ge .least y le = le i

If $x$ is the least upper bound of a constant family, then $x$ must be equal to every member of the family.

  lub-of-const-fam
    : ∀ {ℓᵢ} {I : Type ℓᵢ} {F : I → Ob} {x}
    → (∀ i j → F i ≡ F j)
    → is-lub P F x
    → ∀ i → F i ≡ x
  lub-of-const-fam {F = F} is-const x-lub i =
    ≤-antisym
      (fam≤lub x-lub i)
      (least x-lub (F i) λ j → ≤-refl' (sym (is-const i j)))

Furthermore, if $f : I \to A$ is a constant family and $I$ is merely inhabited, then $f$ has a least upper bound.

  const-inhabited-fam→is-lub
    : ∀ {ℓᵢ} {I : Type ℓᵢ} {F : I → Ob} {x}
    → (∀ i → F i ≡ x)
    → ∥ I ∥
    → is-lub P F x
  const-inhabited-fam→is-lub {I = I} {F = F} {x = x} is-const =
    rec! mk-is-lub where
      mk-is-lub : I → is-lub P F x
      mk-is-lub i .is-lub.fam≤lub j = ≤-refl' (is-const j)
      mk-is-lub i .is-lub.least y le =
        x   =˘⟨ is-const i ⟩
        F i ≤⟨ le i ⟩
        y ≤∎

  const-inhabited-fam→lub
    : ∀ {ℓᵢ} {I : Type ℓᵢ} {F : I → Ob}
    → (∀ i j → F i ≡ F j)
    → ∥ I ∥
    → Lub P F
  const-inhabited-fam→lub {I = I} {F = F} is-const =
    rec! mk-lub where
      mk-lub : I → Lub P F
      mk-lub i .Lub.lub = F i
      mk-lub i .Lub.has-lub =
        const-inhabited-fam→is-lub (λ j → is-const j i) (inc i)