open import Cat.Diagram.Product
open import Cat.Prelude

open import Data.Bool

open import Order.Base
open import Order.Cat

import Order.Reasoning as Poset

module Order.Diagram.Glb where

Greatest lower bounds🔗

A glb gg (short for greatest lower bound) for a family of elements (ai)i:I(a_i)_{i : I} is, as the name implies, a greatest element among the lower bounds of the aia_i. Being a lower bound means that we have gaig \le a_i for all i:Ii : I; Being the greatest lower bound means that if we’re given some other mm satisfying maim \le a_i (for each ii), then we have mum \le u.

A more common word to use for “greatest lower bound” is “meet”. But since “meet” is a fairly uninformative name, and “glb” (pronounced “glib”) is just plain fun to say, we stick with the non-word for the indexed concept. However, if we’re talking about the glb of a binary family, then we use the word “meet”. The distinction here is entirely artificial, and it’s just because we can’t reuse the identifier is-glb for these two slightly different cases. Summing up: to us, a meet is a glb of two elements.

module _ { ℓ′} (P : Poset  ℓ′) where
  private module P = Poset P

  record is-glb {ℓᵢ} {I : Type ℓᵢ} (F : I  P.Ob) (glb : P.Ob)
          : Type (  ℓ′  ℓᵢ) where
    field
      glb≤fam  :  i  glb P.≤ F i
      greatest : (lb′ : P.Ob)  (∀ i  lb′ P.≤ F i)  lb′ P.≤ glb

As mentioned before, in the binary case, we refer to glbs as meets: The meet of aa and bb is, if it exists, the greatest element satisfying (ab)a(a \cap b) \le a and (ab)b(a \cap b) \le b.

  record is-meet (a b : P.Ob) (glb : P.Ob) : Type (  ℓ′) where
    field
      meet≤l   : glb P.≤ a
      meet≤r   : glb P.≤ b
      greatest : (lb′ : P.Ob)  lb′ P.≤ a  lb′ P.≤ b  lb′ P.≤ glb

  open is-meet

A shuffling of terms shows that being a meet is precisely being the greatest lower bound of a family of two elements.

  is-meet→is-glb :  {a b glb}  is-meet a b glb  is-glb (if_then a else b) glb
  is-meet→is-glb meet .glb≤fam true = meet .meet≤l
  is-meet→is-glb meet .glb≤fam false = meet .meet≤r
  is-meet→is-glb meet .greatest glb′ x = meet .greatest glb′ (x true) (x false)

  is-glb→is-meet :  {F : Bool  P.Ob} {glb}  is-glb F glb  is-meet (F true) (F false) glb
  is-glb→is-meet glb .meet≤l = glb .glb≤fam true
  is-glb→is-meet glb .meet≤r = glb .glb≤fam false
  is-glb→is-meet glb .greatest lb′ lb′<a lb′<b = glb .greatest lb′ λ where
    true   lb′<a
    false  lb′<b

An important lemma about meets is that, if xyx \le y, then the greatest lower bound of xx and yy is just xx:

  le→is-meet :  {a b}  a P.≤ b  is-meet a b a
  le→is-meet a≤b .meet≤l = P.≤-refl
  le→is-meet a≤b .meet≤r = a≤b
  le→is-meet a≤b .greatest lb′ lb′≤a _ = lb′≤a

  le-meet :  {a b l}  a P.≤ b  is-meet a b l  a  l
  le-meet a≤b l = ap fst $ meet-unique (_ , le→is-meet a≤b) (_ , l)

As products🔗

The categorification of meets is products: put another way, if our category has propositional homs, then being given a product diagram is the same as being given a meet.

  open is-product
  open Product

  is-meet→product :  {a b glb : P.Ob}  is-meet a b glb  Product (poset→category P) a b
  is-meet→product glb .apex = _
  is-meet→product glb .π₁ = glb .is-meet.meet≤l
  is-meet→product glb .π₂ = glb .is-meet.meet≤r
  is-meet→product glb .has-is-product .⟨_,_⟩ q<a q<b =
    glb .is-meet.greatest _ q<a q<b
  is-meet→product glb .has-is-product .π₁∘factor = prop!
  is-meet→product glb .has-is-product .π₂∘factor = prop!
  is-meet→product glb .has-is-product .unique _ _ _ = prop!