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

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

abstract
  is-join-slat-hom-is-prop
    : βˆ€ {P : Poset o β„“} {Q : Poset o' β„“'} {f : Monotone P Q} {P-slat Q-slat}
    β†’ is-prop (is-join-slat-hom f P-slat Q-slat)
  is-join-slat-hom-is-prop =
    Iso→is-hlevel 1 eqv hlevel!
    where unquoteDecl eqv = declare-record-iso eqv (quote is-join-slat-hom)

instance
  H-Level-is-join-slat-hom
    : βˆ€ {f : Monotone P Q} {P-slat Q-slat n}
    β†’ H-Level (is-join-slat-hom f P-slat Q-slat) (suc n)
  H-Level-is-join-slat-hom = prop-instance is-join-slat-hom-is-prop

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β‚—