module Order.Semilattice where
Semilatticesπ
A semilattice1 is a partially ordered set where every finite family of elements has a meet2. But semilattices-in-general admit an algebraic presentation, as well as an order-theoretic presentation: a semilattice is a commutative idempotent monoid.
As a concrete example of a semilattice before we get started, consider the subsets of a fixed type (like ), under the operation of subset intersection. If we donβt know about the βsubsetβ relation, can we derive it just from the behaviour of intersection?
Surprisingly, the answer is yes! is a subset of iff. the intersection of and is . Check this for yourself: The intersection of (e.g.) and is just again, so .
Generalising away from subsets and intersection, we can recover a partial ordering from any commutative monoid in which all elements are idempotent. That is precisely the definition of a semilattice:
record is-semilattice {β} {A : Type β} (β€ : A) (_β§_ : A β A β A) : Type β where no-eta-equality field has-is-monoid : is-monoid β€ _β§_ idempotent : β {x} β x β§ x β‘ x commutative : β {x y} β x β§ y β‘ y β§ x open is-monoid has-is-monoid public record Semilattice-on {β} (A : Type β) : Type β where no-eta-equality field top : A _β©_ : A β A β A has-is-semilattice : is-semilattice top _β©_ open is-semilattice has-is-semilattice public
to-monoid : Monoid-on A to-monoid = record { has-is-monoid = has-is-monoid } β : β {n} (f : Fin n β A) β A β {zero} f = top β {suc n} f = f fzero β© β (Ξ» i β f (fsuc i)) private unquoteDecl eqv = declare-record-iso eqv (quote is-semilattice) is-semilattice-is-prop : β {β} {A : Type β} (t : A) (m : A β A β A) β is-prop (is-semilattice t m) is-semilattice-is-prop {A = A} t m x = Isoβis-hlevel 1 eqv (hlevel 1) x where instance h-l-a : H-Level A 2 h-l-a = basic-instance 2 (is-semilattice.has-is-set x) instance H-Level-is-semilattice : β {β} {A : Type β} {top : A} {meet : A β A β A} {n} β H-Level (is-semilattice top meet) (suc n) H-Level-is-semilattice = prop-instance (is-semilattice-is-prop _ _)
Rather than going through the usual displayed structure dance, here we exhibit semilattices through an embedding into monoids: when is considered as a monoid, the information that it is a semilattice is a proposition. To be a bit more explicit, is a semilattice homomorphism when and .
Semilattice-structure : β β β Thin-structure {β = β} β Semilattice-on Semilattice-structure β = Full-substructure β _ _ SLatβͺMon (Monoid-structure β) where
SLatβͺMon : β x β Semilattice-on x β£ Monoid-on x SLatβͺMon x .fst = Semilattice-on.to-monoid SLatβͺMon x .snd a (S , p) (T , q) = Ξ£-pathp {A = Semilattice-on x} (Ξ» { i .Semilattice-on.top β (p β sym q) i .Monoid-on.identity ; i .Semilattice-on._β©_ β (p β sym q) i .Monoid-on._β_ ; i .Semilattice-on.has-is-semilattice β r i }) (Ξ» { i j .Monoid-on.identity β sq j i .Monoid-on.identity ; i j .Monoid-on._β_ β sq j i .Monoid-on._β_ ; i j .Monoid-on.has-is-monoid β is-propβsquarep (Ξ» i j β hlevel {T = is-monoid (sq j i .Monoid-on.identity) (sq j i .Monoid-on._β_)} 1) (Ξ» i β r i .is-semilattice.has-is-monoid) (Ξ» i β p i .Monoid-on.has-is-monoid) (Ξ» i β q i .Monoid-on.has-is-monoid) (Ξ» _ β a .Monoid-on.has-is-monoid) i j }) where r = is-propβpathp (Ξ» i β is-semilattice-is-prop ((p β sym q) i .Monoid-on.identity) ((p β sym q) i .Monoid-on._β_)) (S .Semilattice-on.has-is-semilattice) (T .Semilattice-on.has-is-semilattice) sq : Square p (p β sym q) refl q sq i j = hcomp (i β¨ β j) Ξ» where k (k = i0) β p j k (i = i1) β p (j β¨ k) k (j = i0) β p (i β§ k) k (j = i1) β q (i β¨ ~ k)
One might wonder about the soundness of this definition if we want to think of semilattices as order-theoretic objects: is a semilattice homomorphism in the above sense necessarily monotone? A little calculation tells us that yes: we can expand to mean , which by preservation of meets means β which is certainly the casae if , i.e., .
Semilattices : β β β Precategory (lsuc β) β Semilattices β = Structured-objects (Semilattice-structure β) Semilattice : β β β Type (lsuc β) Semilattice β = Precategory.Ob (Semilattices β)
record make-semilattice {β} (A : Type β) : Type β where no-eta-equality field has-is-set : is-set A top : A op : A β A β A idl : β {x} β op top x β‘ x associative : β {x y z} β op x (op y z) β‘ op (op x y) z commutative : β {x y} β op x y β‘ op y x idempotent : β {x} β op x x β‘ x module _ where open Semilattice-on open is-semilattice open make-semilattice to-semilattice-on : β {β} {A : Type β} β make-semilattice A β Semilattice-on A to-semilattice-on s .top = s .top to-semilattice-on s ._β©_ = s .op to-semilattice-on s .has-is-semilattice .has-is-monoid .has-is-semigroup .has-is-magma = record { has-is-set = s .has-is-set } to-semilattice-on s .has-is-semilattice .has-is-monoid .has-is-semigroup .associative = s .associative to-semilattice-on s .has-is-semilattice .has-is-monoid .idl = s .idl to-semilattice-on s .has-is-semilattice .has-is-monoid .idr = s .commutative β s .idl to-semilattice-on s .has-is-semilattice .idempotent = s .idempotent to-semilattice-on s .has-is-semilattice .commutative = s .commutative to-semilattice : β {β} {A : Type β} β make-semilattice A β Semilattice β β£ to-semilattice s .fst β£ = _ to-semilattice s .fst .is-tr = s .has-is-set to-semilattice s .snd = to-semilattice-on s open Functor
As ordersπ
Weβve already commented that a semilattice structure gives rise to a partial order on the underlying set β and, in some sense, this order is canonical β by setting to mean . To justify their inclusion in the same namespace as thin categories, though, we have to make this formal, by exhibiting a functor from semilattices to posets.
Meet-semi-lattice : β {β} β Functor (Semilattices β) (Posets β β) Meet-semi-lattice .Fβ X = X .fst , po where open Poset-on open is-partial-order module X = Semilattice-on (X .snd) po : Poset-on _ β X β po ._β€_ x y = x β‘ x X.β© y po .has-is-poset .β€-thin = hlevel 1 po .has-is-poset .β€-refl = sym X.idempotent
Proving that our now-familiar semilattice-induced order is a partial order reduces to a matter of algebra, which is presented without comment. Note that we do not need idempotence for transitivity or antisymmetry: it is only for reflexivity, where directly translates to .
po .has-is-poset .β€-trans {x} {y} {z} x=xβ§y y=yβ§z = x β‘β¨ x=xβ§y β©β‘ x X.β© β y β β‘β¨ ap! y=yβ§z β©β‘ x X.β© (y X.β© z) β‘β¨ X.associative β©β‘ β x X.β© y β X.β© z β‘Λβ¨ apΒ‘ x=xβ§y β©β‘Λ x X.β© z β po .has-is-poset .β€-antisym {x} {y} x=xβ§y y=yβ§x = x β‘β¨ x=xβ§y β©β‘ x X.β© y β‘β¨ X.commutative β©β‘ y X.β© x β‘Λβ¨ y=yβ§x β©β‘Λ y β
And, formalising our comments about monotonicity from before, any semilattice homomorphism is a monotone map under the induced ordering.
Meet-semi-lattice .Fβ f .hom = f .hom Meet-semi-lattice .Fβ f .preserves x y p = ap (f .hom) p β f .preserves .Monoid-hom.pres-β _ _ Meet-semi-lattice .F-id = Homomorphism-path Ξ» _ β refl Meet-semi-lattice .F-β f g = Homomorphism-path Ξ» _ β refl
The interfaceπ
This section is less about the mathematics per se, and more about how we formalise it. Semilattices (and lattices more generally) are an interesting structure, in that they are category-like in two different ways! In one direction, we have the the category structure by taking having a single Hom-set, and setting to be the composition operation β the delooping of the monoid. In the other direction, we have the poset structure, with the ordering induced by meets.
To effectively formalise mathematics to do with lattices, we need a convenient interface for both of these βcategoriesβ. We already have a fantastic module for working with morphisms in nontrivial categories: instantiating it with the delooping of the monoid means we get, for free, a bunch of combinators for handling big meet expressions.
module Semilattice {β} (A : Semilattice β) where po : Poset _ _ po = Meet-semi-lattice .Fβ A open Poset po public private module X = Semilattice-on (A .snd) renaming ( associative to β©-assoc ; idl to β©-idl ; idr to β©-idr ; commutative to β©-commutative ; idempotent to β©-idempotent ) open X using ( top ; _β©_ ; β©-assoc ; β©-idl ; β©-idr ; β©-commutative ; β©-idempotent ; β ) public open Cat.Reasoning (B (Semilattice-on.to-monoid (A .snd))) hiding ( Ob ; Hom ; id ; _β_ ; assoc ; idl ; idr ) public
As an example of reasoning about the lattice operator, let us prove that is indeed the meet of and in the induced ordering. Itβs reduced to a bit of algebra:
β©-is-meet : β {x y} β is-meet po x y (x β© y) β©-is-meet {x} {y} .is-meet.meetβ€l = x β© y β‘β¨ pushl (sym β©-idempotent) β©β‘ x β© (x β© y) β‘β¨ β©-commutative β©β‘ (x β© y) β© x β β©-is-meet {x} {y} .is-meet.meetβ€r = x β© y β‘Λβ¨ pullr β©-idempotent β©β‘Λ (x β© y) β© y β β©-is-meet {x} {y} .is-meet.greatest lb lb=lbβ§x lb=lbβ§y = lb β‘β¨ lb=lbβ§y β©β‘ lb β© y β‘β¨ pushl lb=lbβ§x β©β‘ lb β© (x β© y) β
private module Y {x} {y} = is-meet (β©-is-meet {x} {y}) renaming (meetβ€l to β©β€l ; meetβ€r to β©β€r ; greatest to β©-univ) open Y public β-is-glb : β {n} (f : Fin n β β A β) β is-glb po f (β f) β-is-glb {zero} f .is-glb.glbβ€fam () β-is-glb {zero} f .is-glb.greatest lbβ² x = sym β©-idr β-is-glb {suc n} f = go where those : is-glb po (Ξ» i β f (fsuc i)) _ those = β-is-glb _ go : is-glb po f (f fzero β© β (Ξ» i β f (fsuc i))) go .is-glb.glbβ€fam fzero = β©β€l go .is-glb.glbβ€fam (fsuc i) = f fzero β© β (Ξ» i β f (fsuc i)) β€β¨ β©β€r β©β€ β (Ξ» i β f (fsuc i)) β€β¨ those .is-glb.glbβ€fam i β©β€ f (fsuc i) β€β go .is-glb.greatest lbβ² fβ€lbβ² = β©-univ lbβ² (fβ€lbβ² fzero) (those .is-glb.greatest lbβ² (Ξ» i β fβ€lbβ² (fsuc i))) module _ {β ββ²} {A : Type β} {B : Type ββ²} (S : Semilattice-on A) (T : Semilattice-on B) (f : A β B) (fh : Monoid-hom (Semilattice-on.to-monoid S) (Semilattice-on.to-monoid T) f) where private module S = Semilattice-on S module T = Semilattice-on T open Monoid-hom slat-pres-β : β {n} (d : Fin n β A) β f (S.β d) β‘ T.β (Ξ» i β f (d i)) slat-pres-β {n = zero} d = fh .pres-id slat-pres-β {n = suc n} d = f (d fzero S.β© S.β (Ξ» i β d (fsuc i))) β‘β¨ fh .pres-β _ _ β©β‘ f (d fzero) T.β© f (S.β Ξ» i β d (fsuc i)) β‘β¨ apβ T._β©_ refl (slat-pres-β Ξ» i β d (fsuc i)) β©β‘ f (d fzero) T.β© T.β (Ξ» i β f (d (fsuc i))) β