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

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)))
    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.β‰€βŸ¨≀ ⟩B.≀
      f #               B.β‰€βŸ¨ B.⋃-inj ( , 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.β‰€βˆŽ
        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

    : (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≀ 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