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} {β„“}