module Order.Frame.Free where

# Free cocompletionsđ

A frame is, in particular, a meet semilattice. Frame homomorphisms preserve finite meets, so they are also homomorphisms of the underlying meet semilattices. Since equality of homomorphisms is determined by equality of the underlying functions, these remarks assemble into a functor $FramesâSLat.$

FrameâȘSLat : â {o â} â Functor (Frames o â) (Meet-slats o â) FrameâȘSLat .Fâ (_ , A) = Frm.meets A FrameâȘSLat .Fâ f .hom = f .hom FrameâȘSLat .Fâ f .witness = has-meet-slat-hom (f .witness) FrameâȘSLat .F-id = trivial! FrameâȘSLat .F-â f g = trivial!

The question this module seeks to answer is: is there a way to freely turn a semilattice $A$ into a frame $D(A),$ such that the meets in $D(A)$ are preserved by the inclusion $AâD(A)?$ And if so, how?

Fortunately the answer is positive: otherwise this module would be
much longer (and probably rely on silly cardinality arguments). The free
frame on a semilattice is the free *cocompletion* of that
semilattice, its poset of lower
sets. The lower sets of *any* poset are a frame, because
meets and joins are computed pointwise in the poset of propositions,
$Î©.$

Lower-sets-frame : â {o â} â Meet-semilattice o â â Frame (o â â) o Lower-sets-frame (P , L) = Lower-sets P , Lâ-frame where module L = Meet-slat L module Lâ = Order.Reasoning (Lower-sets P) Lâ-frame : is-frame (Lower-sets P) Lâ-frame .is-frame._â©_ a b = Lower-sets-meets P a b .Meet.glb Lâ-frame .is-frame.â©-meets a b = Lower-sets-meets P a b .Meet.has-meet Lâ-frame .is-frame.has-top = Lower-sets-top P Lâ-frame .is-frame.â k = Lower-sets-cocomplete P k .Lub.lub Lâ-frame .is-frame.â-lubs k = Lower-sets-cocomplete P k .Lub.has-lub Lâ-frame .is-frame.â-distribl x f = ext Î» arg â Î©-ua (rec! Î» xâ€a i fiâ€a â inc (i , xâ€a , fiâ€a)) (rec! Î» i xâ€a fiâ€a â xâ€a , inc (i , fiâ€a))

The unit map
$AâD(A)$
sends an element of
$A$
to its down-set,
$âA.$
By a decategorification of the similar arguments about the Yoneda embedding,
the map
$AâŠâA$
preserves finite meets (really, it preserves *all* glbs that
exist in
$A);$
and for a complete lattice
$B,$
the left Kan
extension
$Lan_{â}(f):D(A)âB$
of a map
$f:AâB$
along
$â$
is always cocontinuous, and left exact whenever
$f$
is. Since weâre extending semilattice homomorphisms, this means that
$Lan_{â}(f)$
is a frame homomorphism.

Note the similarity between the construction of free frames outlined in the paragraph above and Diaconescuâs theorem: âA map of frames $D(A)âB$ corresponds to a lex monotone map $AâB$â is precisely the decategorification of âA geometric morphism $BâD(A)$ is a flat functor $AâB$â.

make-free-cocompletion : â {â} â (A : Meet-semilattice â â) â Free-object FrameâȘSLat A make-free-cocompletion {â} A = go where

Anwyay, that was a *very* dense explanation of the universal
property. Letâs go through it again, this time commenting on everything
as we encounter it. We start by packaging together the extension of a
semilattice homomorphism
$AâB$
to a frame homomorphism
$DAâB.$

module A = Meet-slat (A .snd) module Mk (B : Frame â â) (f : Meet-slats.Hom A (Frm.meets (B .snd))) where module Aâ = Frm (Lower-sets-frame A .snd) module B = Frm (B .snd) module f = is-meet-slat-hom (f .witness)

The easy part is an appeal to the existing machinery for free
cocompletions: Any monotone map
$AâB$
extends to a *cocontinuous* map
$DAâB,$
because
$B,$
being a frame, is cocomplete.

mkhom : Frames.Hom (Lower-sets-frame A) B mkhom .hom = Lanâ B.â-lubs (f .hom) mkhom .witness .â-â€ g = B.â€-refl' $ Lanâ-cocontinuous B.â-lubs (f .hom) g

The harder part is showing that the cocontinuous extension of a semilattice homomorphism is still a semilattice homomorphism. It preserves the top element, since the cocontinuous extension takes $â€_{A}$ to $â«_{B}â€_{A},$ which is readily calculated to equal $â€_{B}:$

mkhom .witness .top-â€ = B.top B.â€âš f.top-â€ â©B.â€ f # A.top B.â€âš B.â-inj (A.top , tt) â©B.â€ B.â (Î» i â f # fst i) B.â€â

Slightly harder, but still a bit of algebra, is computing that binary meets are preserved as well. The first step follows from the infinite distributive law in $B,$ and the second from the fact that $f$ preserves binary meets.

mkhom .witness .â©-â€ S T = B.â (Î» i â f # fst i) B.â© B.â (Î» i â f # fst i) B.=âš B.â-â©-product (Î» i â hom f # fst i) (Î» i â hom f # fst i) â©B.= B.â (Î» i â f # fst (fst i) B.â© f # fst (snd i)) B.â€âš B.ââ€â-over meet-section (Î» i â f.â©-â€ _ _) â©B.â€ B.â (Î» i â f # fst i) B.â€â where meet-section : â«â S Ă â«â T â â«â (Î» x â x â S Ă x â T) meet-section ((x , p) , (y , q)) = x A.â© y , S .pres-â€ A.â©â€l p , T .pres-â€ A.â©â€r q

Itâs also free from the definition of cocompletions that the extended map $fâ$ satisfies $fâ(âx)=f(x).$

mkcomm : â x â mkhom # (â (A .fst) x) âĄ f # x mkcomm x = (Lanâ-commutes B.â-lubs (f .hom) x)

Now we must define the unit map. Weâve already committed to defining
$Î·_{a}=âa,$
so we have to show that
$â$
preserves finite meets. This is true because
$â$
lands in *lower sets*, so it suffices to show an equivalence
between (e.g.) being *under
$a$
and under
$b$*
and being *under
$aâ§b$*.
But thatâs the definition of
$â§.$

the-unit : (S : Meet-semilattice â â) â Meet-slats.Hom S (Frm.meets (Lower-sets-frame S .snd)) the-unit S = go where module S = Meet-slat (S .snd) module Sâ = Frm (Lower-sets-frame S .snd) go : Meet-slats.Hom S Sâ.meets go .hom = ăâ (S .fst) go .witness .is-meet-slat-hom.â©-â€ x y z (p , q) = do zâ€x â p zâ€y â q pure $ S.â©-universal z zâ€x zâ€y go .witness .is-meet-slat-hom.top-â€ x _ = pure S.!

Weâre already 80% done with the adjunction. The final thing to do is to put it all together, bringing in the result about uniqueness of cocontinuous extensions to tie everything up:

go : Free-object FrameâȘSLat A go .free = Lower-sets-frame A go .unit = the-unit A go .fold {B} f = Mk.mkhom B f go .commute {B} {f} = ext (Mk.mkcomm B f) go .unique {B} {f} g wit = ext (p #â_) where open Mk B f gá” : Monotone (Lower-sets (A .fst)) (B .fst) gá” .hom x = g # x gá” .pres-â€ {x} {y} w = g .hom .pres-â€ w p = Lanâ-unique B.â-lubs (f .hom) gá” (is-frame-hom.pres-â (g .witness)) (wit #â_)