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