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 $a\cup b\text{,}$ 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 $f(\perp )=\perp \text{,}$ and $f(a\cup b)=f(a)\cup f(b)\text{.}$ Note that, since $f$ was already assumed to be order-preserving, it suffices to have $f(a\cup b)$ less than $f(a)\cup f(b)\text{,}$ 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

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ₗ