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

open import Data.Fin.Indexed
open import Data.Fin.Finite
open import Data.Fin.Base hiding (_β€_)

open import Order.Diagram.Bottom
open import Order.Diagram.Join
open import Order.Diagram.Lub
open import Order.Base

import Cat.Reasoning

import Order.Diagram.Join.Reasoning as Joins
import Order.Reasoning

module Order.Semilattice.Join where


# Join semilatticesπ

A join semilattice is a partially ordered set which has all finite joins. This means, in particular, that it has a bottom element, since that is the join of the empty family. Note that, even though join-semilattices are presented as being equipped with a binary operation this is not actual structure on the partially-ordered set: joins are uniquely determined, so βbeing a join-semilatticeβ is always a proposition.

record is-join-semilattice {o β} (P : Poset o β) : Type (o β β) where
field
_βͺ_     : β P β β β P β β β P β
βͺ-joins : β x y β is-join P x y (x βͺ y)
has-bottom : Bottom P

  infixr 24 _βͺ_

open Joins βͺ-joins public
open Bottom has-bottom using (bot; Β‘) public

abstract
is-join-semilattice-is-prop
: β {o β} {P : Poset o β}
β is-prop (is-join-semilattice P)
is-join-semilattice-is-prop {P = P} p q = path where
open Order.Diagram.Bottom P using (H-Level-Bottom)
open is-join-semilattice
module p = is-join-semilattice p
module q = is-join-semilattice q

joinp : β x y β x p.βͺ y β‘ x q.βͺ y
joinp x y = join-unique (p.βͺ-joins x y) (q.βͺ-joins x y)

path : p β‘ q
path i ._βͺ_ x y     = joinp x y i
path i .βͺ-joins x y = is-propβpathp (Ξ» i β hlevel {T = is-join P x y (joinp x y i)} 1) (p.βͺ-joins x y) (q.βͺ-joins x y) i
path i .has-bottom  = hlevel {T = Bottom P} 1 p.has-bottom q.has-bottom i

private variable
o β o' β' : Level
P Q R : Poset o β

instance
H-Level-is-join-semilattice : β {n} β H-Level (is-join-semilattice P) (suc n)
H-Level-is-join-semilattice = prop-instance is-join-semilattice-is-prop


Morphisms of join semilattices are monotone functions which additionally send joins to joins: we have and Note that, since was already assumed to be order-preserving, it suffices to have less than with an inequality. This is because we always have the reverse direction by the universal property.

record
is-join-slat-hom
{P : Poset o β} {Q : Poset o' β'} (f : Monotone P Q)
(P-slat : is-join-semilattice P)
(Q-slat : is-join-semilattice Q) : Type (o β β')
where

  no-eta-equality
private
module P = Poset P
module Pβ = is-join-semilattice P-slat
module Q = Order.Reasoning Q
module Qβ = is-join-semilattice Q-slat
open is-join

  field
βͺ-β€   : β x y β f # (x Pβ.βͺ y) Q.β€ (f # x) Qβ.βͺ (f # y)
bot-β€ : f # Pβ.bot Q.β€ Qβ.bot

  pres-βͺ : β x y β f # (x Pβ.βͺ y) β‘ (f # x) Qβ.βͺ (f # y)
pres-βͺ x y = Q.β€-antisym (βͺ-β€ x y) \$ Qβ.βͺ-universal (f # (x Pβ.βͺ y))
(f .pres-β€ Pβ.lβ€βͺ)
(f .pres-β€ Pβ.rβ€βͺ)

pres-bot : f # Pβ.bot β‘ Qβ.bot
pres-bot = Q.β€-antisym bot-β€ Qβ.Β‘

pres-joins
: β {x y m}
β is-join P x y m
β is-join Q (f # x) (f # y) (f # m)
pres-joins join .is-join.lβ€join = f .pres-β€ (join .lβ€join)
pres-joins join .is-join.rβ€join = f .pres-β€ (join .rβ€join)
pres-joins {x = x} {y = y} {m = m} join .is-join.least lb fxβ€lb fyβ€lb =
f # m            Q.β€β¨ f .pres-β€ (join .least (x Pβ.βͺ y) Pβ.lβ€βͺ Pβ.rβ€βͺ) β©Q.β€
f # (x Pβ.βͺ y)   Q.β€β¨ βͺ-β€ x y β©Q.β€
f # x Qβ.βͺ f # y Q.β€β¨ Qβ.βͺ-universal lb fxβ€lb fyβ€lb β©Q.β€
lb               Q.β€β

pres-bottoms
: β {b}
β is-bottom P b
β is-bottom Q (f # b)
pres-bottoms {b = b} b-bot x =
f # b      Q.β€β¨ f .pres-β€ (b-bot Pβ.bot) β©Q.β€
f # Pβ.bot Q.β€β¨ bot-β€ β©Q.β€
Qβ.bot     Q.β€β¨ Qβ.Β‘ β©Q.β€
x          Q.β€β

open is-join-slat-hom

unquoteDecl H-Level-is-join-slat-hom = declare-record-hlevel 1 H-Level-is-join-slat-hom (quote is-join-slat-hom)

open Poset


## The category of join-semilatticesπ

It is clear from the definition that join semilatice homomorphisms are closed under identity and composition: therefore, we can define the category of join-semilattices as a subcategory of that of posets. However, this subcategory is not full: there are monotone functions between semilattices that do not preserve joins.

id-join-slat-hom
: (Pβ : is-join-semilattice P)
β is-join-slat-hom idβ Pβ Pβ

β-join-slat-hom
: β {Pβ Qβ Rβ} {f : Monotone Q R} {g : Monotone P Q}
β is-join-slat-hom f Qβ Rβ
β is-join-slat-hom g Pβ Qβ
β is-join-slat-hom (f ββ g) Pβ Rβ

id-join-slat-hom {P = P} _ .βͺ-β€ _ _ = P .β€-refl
id-join-slat-hom {P = P} _ .bot-β€   = P .β€-refl

β-join-slat-hom {R = R} {f = f} {g = g} f-pres g-pres .βͺ-β€ x y =
R .β€-trans (f .pres-β€ (g-pres .βͺ-β€ x y)) (f-pres .βͺ-β€ (g # x) (g # y))
β-join-slat-hom {R = R} {f = f} {g = g} f-pres g-pres .bot-β€ =
R .β€-trans (f .pres-β€ (g-pres .bot-β€)) (f-pres .bot-β€)

Join-slats-subcat : β o β β Subcat (Posets o β) (o β β) (o β β)
Join-slats-subcat o β .Subcat.is-ob       = is-join-semilattice
Join-slats-subcat o β .Subcat.is-hom      = is-join-slat-hom
Join-slats-subcat o β .Subcat.is-hom-prop _ _ _ = hlevel 1
Join-slats-subcat o β .Subcat.is-hom-id   = id-join-slat-hom
Join-slats-subcat o β .Subcat.is-hom-β    = β-join-slat-hom

Join-slats : β o β β Precategory (lsuc o β lsuc β) (o β β)
Join-slats o β = Subcategory (Join-slats-subcat o β)

module Join-slats {o} {β} = Cat.Reasoning (Join-slats o β)

Join-slatsβPosets : β {o β} β Functor (Join-slats o β) (Posets o β)
Join-slatsβPosets = Forget-subcat

Join-slatsβͺSets : β {o β} β Functor (Join-slats o β) (Sets o)
Join-slatsβͺSets = PosetsβͺSets Fβ Join-slatsβPosets

Join-semilattice : β o β β Type _
Join-semilattice o β = Join-slats.Ob {o} {β}