open import Algebra.Monoid.Category
open import Algebra.Semigroup
open import Algebra.Monoid

open import Cat.Displayed.Univalence.Thin
open import Cat.Instances.Delooping
open import Cat.Prelude

open import Data.Fin.Base hiding (_β€_)

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

import Cat.Reasoning

import Order.Reasoning as Poset

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 $\mathbb{N}$), 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! $X$ is a subset of $Y$ iff. the intersection of $X$ and $Y$ is $X$. Check this for yourself: The intersection of (e.g.) $X = \{ 1, 2, 3 \}$ and $Y = \{ 1, 2, 3, 4, 5 \}$ is just $\{ 1, 2, 3 \}$ again, so $X \sube Y$.

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 $(A, \top, \cap)$ is considered as a monoid, the information that it is a semilattice is a proposition. To be a bit more explicit, $f : A \to B$ is a semilattice homomorphism when $f(\top) = \top$ and $f(x \cap y) = f(x) \cap f(y)$.

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 $f(x) \le f(y)$ to mean $f(x) = f(x) \cap f(y)$, which by preservation of meets means $f(x) = f(x \cap y)$ β which is certainly the casae if $x = x \cap y$, i.e., $x \le y$.

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 $x \le y$ to mean $x = x \cap y$. 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 $x \le x$ directly translates to $x = x \land x$.

  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 $a \cap b$ to be the composition operation β the delooping of the $\cap$ 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 $\cap$ 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 $x \cap y$ is indeed the meet of $x$ and $y$ 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))) β


1. Really, either a meet semilattice or a join semilattice, when considered ordered-theoreticallyβ©οΈ

2. Or a join, dependingβ©οΈ