open import Cat.Prelude

open import Order.Diagram.Glb
open import Order.Semilattice
open import Order.Base

import Order.Reasoning as Poset

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