open import 1Lab.Function.Surjection

open import Algebra.Monoid

open import Cat.Functor.Subcategory
open import Cat.Functor.Adjoint
open import Cat.Prelude

open import Data.Fin.Indexed
open import Data.Fin.Base
open import Data.Sum.Base
open import Data.Power

open import Order.Semilattice.Join.Subsemilattice
open import Order.Instances.Pointwise.Diagrams
open import Order.Semilattice.Join.NAry
open import Order.Instances.Pointwise
open import Order.Semilattice.Join
open import Order.Diagram.Lub
open import Order.Subposet
open import Order.Base

import Order.Semilattice.Join.Reasoning

module Order.Semilattice.Free where

Free (semi)lattices🔗

This module provides an impredicative construction of the free join semilattice on a set $A\text{,}$ as the semilattice of Kuratowski-finite subsets $K(A)\text{,}$ 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\text{,}$ 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\text{.}$ 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\to K(A)$ as $\eta \text{,}$ since it will play the role of our adjunction unit when we establish the universal property of $K(A)\text{.}$

  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\subseteq 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\to B$ and a semilattice structure on $B\text{,}$ we can extend this to a semilattice homomorphism¹ $f^{\prime }:K(A)\to B$ by first expressing $S:K(A)$ as ${\bigcup }_{i:[n]}\eta (a_i)$ for some $n\text{,}$ $a_i\text{,}$ then computing ${\bigcup }_{i:[n]}f(a_i)\text{.}$

  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\hookrightarrow A$ by first computing a join for the composite $[n]\twoheadrightarrow P\hookrightarrow A\text{,}$ then “forgetting” about the fact we used the epi from $[n]\text{.}$

      ε : 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\to 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

    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\}\text{,}$ and the universal extension of $f:A\to B$ is as defined above.

open Free-object
open Subcat-hom
open is-join-slat-hom

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)\to B$ such that $f=g\circ \{-\}\text{,}$ and let $P:K(A)\text{.}$ To see that the $g(P)=f^{\prime }(P)\text{,}$ note that $f^{\prime }$ 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\text{.}$ Furthermore, $g$ preserves all finitely-indexed joins, so $g$ must be computed as a join over the elements of $P\text{,}$ which is the same join used to compute the extension of $f\text{.}$

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