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