open import Cat.Prelude

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

import Order.Reasoning

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, \le)$ such that any finite number of elements has a greatest lower bound, then $A$ 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