{-# OPTIONS --lossy-unification #-}
open import Cat.Functor.Subcategory
open import Cat.Functor.Adjoint
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 $\mathbf{Frames}\to \mathbf{SLat}\text{.}$

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 $A$ into a frame $D(A)\text{,}$ such that the meets in $D(A)$ are preserved by the inclusion $A\to D(A)\text{?}$ 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, $\Omega \text{.}$

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 → biimp
    (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\to D(A)$ sends an element of $A$ to its down-set, $\downarrow A\text{.}$ By a decategorification of the similar arguments about the Yoneda embedding, the map $A\mapsto \downarrow A$ preserves finite meets (really, it preserves all glbs that exist in $A\text{);}$ and for a complete lattice $B\text{,}$ the left Kan extension ${\mathrm{Lan}}_{\downarrow }(f):D(A)\to B$ of a map $f:A\to B$ along $\downarrow$ is always cocontinuous, and left exact whenever $f$ is. Since we’re extending semilattice homomorphisms, this means that ${\mathrm{Lan}}_{\downarrow }(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)\to B$ corresponds to a lex monotone map $A\to B$” is precisely the decategorification of “A geometric morphism $B\to D(A)$ is a flat functor $A\to 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\to B$ to a frame homomorphism $DA\to B\text{.}$

  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\to B$ extends to a cocontinuous map $DA\to B\text{,}$ because $B\text{,}$ 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 ${\top }_A$ to ${\int }_B{\top }_A\text{,}$ which is readily calculated to equal ${\top }_B\text{:}$

    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\text{,}$ 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 $\hat{f}$ satisfies $\hat{f}(\downarrow x)=f(x)\text{.}$

    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 ${\eta }_a=\downarrow a\text{,}$ so we have to show that $\downarrow$ preserves finite meets. This is true because $\downarrow$ lands in lower sets, so it suffices to show an equivalence between (e.g.) being under $a$ and under $b$ and being under $a\wedge b$. But that’s the definition of $\wedge \text{.}$

  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:

  open Free-object

  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 #ₚ_)