module Order.Semilattice.Free where

# Free (semi)latticesπ

This module provides an *impredicative* construction of the
free join
semilattice on a set
$A,$
as the semilattice of Kuratowski-finite
subsets
$K(A),$
ordered by inclusion, under the operation of union. While this
construction might feel like it comes out of left field, finite subsets
are actually a very natural model for join semilattices, since *every
subset is a join of singletons*.

While this Coyoneda-like theorem about
$K(A)$
provides an abstract justification for the construction, itβs important
to keep in mind that a Kuratowski-finite subset of
$A$
can be equivalently presented as a list with elements drawn from
$A,$
but considered modulo order and repetition. Therefore, a concrete
intuition for this construction can also be drawn from the connection
between semilattices and monoids: a semilattice is a *commutative,
idempotent* monoid.

module _ {β} (A : Set β) where K-finite-subset : Type β K-finite-subset = Ξ£[ P β (β£ A β£ β Ξ©) ] (is-K-finite P) _βͺα΅_ : K-finite-subset β K-finite-subset β K-finite-subset (P , pf) βͺα΅ (Q , qf) = P βͺ Q , union-is-K-finite {P = P} {Q = Q} pf qf minimalα΅ : K-finite-subset minimalα΅ = minimal , minimal-is-K-finite

Since $K(A)$ is closed under unions (and contains the least element), it follows that itβs a semilattice, being a sub-semilattice of the power set of $A.$ In fact, a different characterisation of $K(A)$ is as the smallest sub-semilattice of $K(A)$ containing the singletons and closed under union.

K[_] : Join-semilattice β β K[_] .fst = Subposet (Subsets β£ A β£) Ξ» P β el! (is-K-finite P) K[_] .snd = Subposet-is-join-semilattice Subsets-is-join-slat (Ξ» {P} {Q} pf qf β union-is-K-finite {P = P} {Q = Q} pf qf) minimal-is-K-finite private module KA = Order.Semilattice.Join.Reasoning (K[_] .snd)

We shall refer to the singleton-assigning map $AβK(A)$ as $Ξ·,$ since it will play the role of our adjunction unit when we establish the universal property of $K(A).$

singletonα΅ : β£ A β£ β K-finite-subset singletonα΅ x = singleton x , singleton-is-K-finite (A .is-tr) x

We can then establish the aforementioned Coyoneda-like statement: a K-finite subset $PβA$ is the join of the singleton subsets it contains.

K-singleton-lub : (P : K-finite-subset) β is-lub (K[_] .fst) {I = β«β (P .fst)} (singletonα΅ β fst) P K-singleton-lub P = subposet-has-lub _ (P .snd) (subset-singleton-lub _)

In a similar vein, given a map
$f:AβB$
and a semilattice structure on
$B,$
we can extend this to a semilattice homomorphism^{1}
$f_{β²}:K(A)βB$
by first expressing
$S:K(A)$
as
$β_{i:[n]}Ξ·(a_{i})$
for some
$n,$
$a_{i},$
then computing
$β_{i:[n]}f(a_{i}).$

module _ {o β'} (B : Join-semilattice o β') where private module B = Order.Semilattice.Join.Reasoning (B .snd) fold-K : (β£ A β£ β β B β) β K-finite-subset β β B β fold-K f (P , P-fin) = Lub.lub Ξ΅' module fold-K where fam : (Ξ£ β£ A β£ Ξ» x β β£ P x β£) β β B β fam (x , _) = f x

Since precomposition with a surjection both
*preserves and reflect* the property of being a least upper bound,
we can compute a join for our family
$PβͺA$
by first computing a join for the composite
$[n]βPβͺA,$
then βforgettingβ about the fact we used the epi from
$[n].$

Ξ΅ : Finite-cover (β«β P) β Lub (B .fst) fam Ξ΅ (covering {card} g surj) = cover-reflects-lub surj (Finite-lubs (B .snd) (fam β g)) Ξ΅' : Lub (B .fst) fam Ξ΅' = rec! Ξ΅ P-fin module Ξ΅' = Lub Ξ΅'

This extension of $f:AβB$ is monotonic, since itβs computed as a join.

fold-K-pres-β€ : β (f : β A β β β B β) β (P Q : K-finite-subset) β P .fst β Q .fst β fold-K f P B.β€ fold-K f Q fold-K-pres-β€ f (P , Pf) Qqf@(Q , Qf) PβQ = fold-K.Ξ΅'.least f P Pf (fold-K f Qqf) Ξ» (x , xβP) β fold-K.Ξ΅'.famβ€lub f Q Qf (x , PβQ x xβP)

Likewise, it can be shown to preserve binary joins, and the bottom element.

fold-K-βͺ-β€ : (f : β A β β β B β) (P Q : K-finite-subset) β fold-K f (P βͺα΅ Q) B.β€ (fold-K f P B.βͺ fold-K f Q) fold-K-bot-β€ : (f : β A β β β B β) β fold-K f minimalα΅ B.β€ B.bot

## The proofs follow the same pattern as the proof of monotonicity, so we omit them.

fold-K-βͺ-β€ f Ppf@(P , Pf) Qqf@(Q , Qf) = fold-K.Ξ΅'.least f (P βͺ Q) (union-is-K-finite Pf Qf) _ go where go : (i : β«β (P βͺ Q)) β f (i .fst) B.β€ fold-K f Ppf B.βͺ fold-K f Qqf go (x , inc (inl p)) = B.β€-trans (fold-K.Ξ΅'.famβ€lub f P Pf (x , p)) B.lβ€βͺ go (x , inc (inr p)) = B.β€-trans (fold-K.Ξ΅'.famβ€lub f Q Qf (x , p)) B.rβ€βͺ go (x , squash p q i) = B.β€-thin (go (x , p)) (go (x , q)) i fold-K-bot-β€ f = fold-K.Ξ΅'.least f minimal minimal-is-K-finite B.bot Ξ» ()

Crucially for the universal property, when applied to a singleton subset, this extension agrees with our original function. Intuitively, this is because weβre taking the join of a single thing, but we still have to show this!

fold-K-singleton : (f : β A β β β B β) (x : β A β) β fold-K f (singletonα΅ x) β‘ f x fold-K-singleton f x = B.β€-antisym (Ξ΅'.least (f x) Ξ» (y , β‘x=y) β case β‘x=y of Ξ» x=y β subst (Ξ» Ο β f Ο B.β€ f x) x=y B.β€-refl) (Ξ΅'.famβ€lub (x , inc refl)) where open fold-K f (singleton x) (singleton-is-K-finite (A .is-tr) x)

We now have all the ingredients to show that $K$ is a left adjoint. The unit of the adjunction takes an element $x:A$ to the singleton set ${x},$ and the universal extension of $f:AβB$ is as defined above.

make-free-join-slat : β {β} β (A : Set β) β Free-object (Join-slatsβͺSets {β = β}) A make-free-join-slat A .free = K[ A ] make-free-join-slat A .unit = singletonα΅ A make-free-join-slat A .fold {B} f .hom .hom = fold-K A B f make-free-join-slat A .fold {B} f .hom .pres-β€ {P} {Q} = fold-K-pres-β€ A B f P Q make-free-join-slat A .fold {B} f .witness .βͺ-β€ = fold-K-βͺ-β€ A B f make-free-join-slat A .fold {B} f .witness .bot-β€ = fold-K-bot-β€ A B f

As noted earlier, the extension of $f$ agrees with $f$ on singleton sets, so the universal extension commutes with the unit of the adjunction.

make-free-join-slat A .commute {B} {f} = ext (fold-K-singleton A B f)

Finally, we shall show that the universal extension of
$f$
is unique. Let
$g:K(A)βB$
such that
$f=gβ{β},$
and let
$P:K(A).$
To see that the
$g(P)=f_{β²}(P),$
note that
$f_{β²}$
is computed via taking a join, so it suffices to show that
$g$
is *also* computed via a join over the same family.

By our assumptions,
$g$
agrees with
$f$
on singleton sets. However, every K-finite subset
$P$
can be described as a (finitely-indexed) join over the elements of
$P.$
Furthermore,
$g$
preserves all finitely-indexed joins, so
$g$
*must* be computed as a join over the elements of
$P,$
which is the same join used to compute the extension of
$f.$

make-free-join-slat A .unique {B} {f} g p = ext Ξ» P pfin β sym $ lub-unique (fold-K.Ξ΅'.has-lub A B f P pfin) (cast-is-lubαΆ (Ξ» Q β (p #β Q .fst)) $ pres-finitely-indexed-lub (g .witness) pfin _ _ $ K-singleton-lub A _)

Here we construct the underlying map first, the proof that itβs a semilattice homomorphism follows.β©οΈ