{-# OPTIONS --lossy-unification -vtc.decl:5 -vtactic.hlevel:30 #-}
open import Cat.Functor.Subcategory
open import Cat.Prelude

open import Data.Bool

open import Order.Instances.Lower.Cocompletion
open import Order.Instances.Pointwise
open import Order.Semilattice.Meet
open import Order.Instances.Lower
open import Order.Diagram.Meet
open import Order.Diagram.Glb
open import Order.Diagram.Lub
open import Order.Frame
open import Order.Base

import Order.Semilattice.Meet.Reasoning as Meet-slat
import Order.Frame.Reasoning as Frm
import Order.Reasoning

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

open Functor
open Subcat-hom
open is-frame-hom

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 into a frame such that the meets in are preserved by the inclusion 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 (Ξ» { (x , box) β β‘-map (Ξ» { (i , argβfi) β i , x , argβfi }) box })
(β‘-rec! Ξ» { (i , x , argβfi) β x , inc (i , argβfi) })


The unit map sends an element of to its down-set, By a decategorification of the similar arguments about the Yoneda embedding, the map preserves finite meets (really, it preserves all glbs that exist in and for a complete lattice the left Kan extension of a map along is always cocontinuous, and left exact whenever is. Since weβre extending semilattice homomorphisms, this means that 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 corresponds to a lex monotone map β is precisely the decategorification of βA geometric morphism is a flat functor β.

make-free-cocompletion : β {β} β make-left-adjoint (FrameβͺSLat {β} {β})
make-free-cocompletion {β} = 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 to a frame homomorphism

  module Mk (A : Meet-semilattice β β) (B : Frame β β)
(f : Meet-slats β β .Precategory.Hom A (Frm.meets (B .snd)))
where
module A  = Meet-slat (A .snd)
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 extends to a cocontinuous map because 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 to which is readily calculated to equal  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 and the second from the fact that 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 satisfies  mkcomm : β x β f # x β‘ mkhom # (β (A .fst) x) mkcomm x = sym (Lanβ-commutes B.β-lubs (f .hom) x)  Now we must define the unit map. Weβve already committed to defining 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 and under and being under . 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 : make-left-adjoint (FrameβͺSLat {β})
go .free = Lower-sets-frame
go .unit = the-unit
go .universal {A} {B} f = Mk.mkhom A B f
go .commutes {A} {B} f = ext (Mk.mkcomm A B f)
go .unique {A} {B} {f = f} {g} wit = ext q where
open Mk A 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))
Ξ» x β ap (_# x) (sym wit)

q : β x β Lanβ B.β-lubs (f .hom) # x β‘ g # x
q x = sym p #β x