module Order.Semilattice.Order where

Semilattices from posetsπŸ”—

We have already established that semilattices, which we define algebraically, have an underlying poset. The aim of this module is to prove the converse: If you have a poset (A,≀)(A, \le) such that any finite number of elements has a greatest lower bound, then AA is a semilattice. As usual, by induction, it suffices to have nullary and binary greatest lower bounds: A top element, and meets.

To this end, we define a type of finitely complete posets: Posets possessing meets and a top element.

record Finitely-complete-poset β„“β‚’ β„“α΅£ : Type (lsuc (β„“β‚’ βŠ” β„“α΅£)) where
  no-eta-equality
  field
    poset : Poset β„“β‚’ β„“α΅£
    _∩_         : ⌞ poset ⌟ β†’ ⌞ poset ⌟ β†’ ⌞ poset ⌟
    has-is-meet : βˆ€ {x y} β†’ is-meet poset x y (x ∩ y)

    top        : ⌞ poset ⌟
    has-is-top : βˆ€ {x} β†’ Poset._≀_ poset x top

  open Poset poset public
  private module meet {x} {y} = is-meet (has-is-meet {x} {y})
  open meet renaming (meet≀l to βˆ©β‰€l ; meet≀r to βˆ©β‰€r ; greatest to ∩-univ) public

  leβ†’meet : βˆ€ {x y} β†’ x ≀ y β†’ x ≑ x ∩ y
  leβ†’meet x≀y = le-meet poset x≀y has-is-meet

  meetβ†’le : βˆ€ {x y} β†’ x ≑ x ∩ y β†’ x ≀ y
  meetβ†’le {y = y} x=x∩y = subst (_≀ y) (sym x=x∩y) βˆ©β‰€r

From a finitely complete poset, we can define a semilattice: from the universal property of meets, we can conclude that they are associative, idempotent, commutative, and have the top element as a unit.

fc-posetβ†’semilattice : βˆ€ {o β„“} (P : Finitely-complete-poset o β„“) β†’ Semilattice o
fc-poset→semilattice P = to-semilattice make-p where
  module ml = make-semilattice
  open Finitely-complete-poset P

  make-p : make-semilattice ⌞ poset ⌟
  make-p .ml.has-is-set = hlevel!
  make-p .ml.top = top
  make-p .ml.op = _∩_
  make-p .ml.idl = ≀-antisym βˆ©β‰€r (∩-univ _ has-is-top ≀-refl)
  make-p .ml.associative = ≀-antisym
    (∩-univ _
      (∩-univ _ βˆ©β‰€l (≀-trans βˆ©β‰€r βˆ©β‰€l))
      (≀-trans βˆ©β‰€r βˆ©β‰€r))
    (∩-univ _ (≀-trans βˆ©β‰€l βˆ©β‰€l) (∩-univ _ (≀-trans βˆ©β‰€l βˆ©β‰€r) βˆ©β‰€r))
  make-p .ml.commutative = ≀-antisym
    (∩-univ _ βˆ©β‰€r βˆ©β‰€l)
    (∩-univ _ βˆ©β‰€r βˆ©β‰€l)
  make-p .ml.idempotent = ≀-antisym βˆ©β‰€l (∩-univ _ ≀-refl ≀-refl)

It’s a general fact about meets that the semilattice ordering defined with the meets from a finitely complete poset agrees with our original ordering, which we link below:

_ = le-meet