module Order.Semilattice where

Semilattices🔗

A semilattice¹ is a partially ordered set where every finite family of elements has a meet². But semilattices-in-general admit an algebraic presentation, as well as an order-theoretic presentation: a semilattice is a commutative idempotent monoid.

As a concrete example of a semilattice before we get started, consider the subsets of a fixed type (like $\mathbb{N}$), under the operation of subset intersection. If we don’t know about the “subset” relation, can we derive it just from the behaviour of intersection?

Surprisingly, the answer is yes! $X$ is a subset of $Y$ iff. the intersection of $X$ and $Y$ is $X$. Check this for yourself: The intersection of (e.g.) $X = \{ 1, 2, 3 \}$ and $Y = \{ 1, 2, 3, 4, 5 \}$ is just $\{ 1, 2, 3 \}$ again, so $X \sube Y$.

Generalising away from subsets and intersection, we can recover a partial ordering from any commutative monoid in which all elements are idempotent. That is precisely the definition of a semilattice:

record is-semilattice {ℓ} {A : Type ℓ} (⊤ : A) (_∧_ : A → A → A) : Type ℓ where
  no-eta-equality
  field
    has-is-monoid : is-monoid ⊤ _∧_
    idempotent    : ∀ {x}   → x ∧ x ≡ x
    commutative   : ∀ {x y} → x ∧ y ≡ y ∧ x
  open is-monoid has-is-monoid public

record Semilattice-on {ℓ} (A : Type ℓ) : Type ℓ where
  no-eta-equality
  field
    top : A
    _∩_ : A → A → A
    has-is-semilattice : is-semilattice top _∩_
  open is-semilattice has-is-semilattice public
  infixr 25 _∩_

Rather than going through the usual displayed structure dance, here we exhibit semilattices through an embedding into monoids: when $(A, \top, \cap)$ is considered as a monoid, the information that it is a semilattice is a proposition. To be a bit more explicit, $f : A \to B$ is a semilattice homomorphism when $f(\top) = \top$ and $f(x \cap y) = f(x) \cap f(y)$.

Semilattice-structure : ∀ ℓ → Thin-structure {ℓ = ℓ} ℓ Semilattice-on
Semilattice-structure ℓ =
  Full-substructure ℓ _ _ SLat↪Mon (Monoid-structure ℓ) where

One might wonder about the soundness of this definition if we want to think of semilattices as order-theoretic objects: is a semilattice homomorphism in the above sense necessarily monotone? A little calculation tells us that yes: we can expand $f(x) \le f(y)$ to mean $f(x) = f(x) \cap f(y)$, which by preservation of meets means $f(x) = f(x \cap y)$ — which is certainly the casae if $x = x \cap y$, i.e., $x \le y$.

Semilattices : ∀ ℓ → Precategory (lsuc ℓ) ℓ
Semilattices ℓ = Structured-objects (Semilattice-structure ℓ)

Semilattice : ∀ ℓ → Type (lsuc ℓ)
Semilattice ℓ = Precategory.Ob (Semilattices ℓ)

As orders🔗

We’ve already commented that a semilattice structure gives rise to a partial order on the underlying set — and, in some sense, this order is canonical — by setting $x \le y$ to mean $x = x \cap y$. To justify their inclusion in the same namespace as thin categories, though, we have to make this formal, by exhibiting a functor from semilattices to posets.

Meet-semi-lattice : ∀ {ℓ} → Functor (Semilattices ℓ) (Posets ℓ ℓ)
Meet-semi-lattice .F₀ X = po where
  open Poset
  module X = Semilattice-on (X .snd)
  po : Poset _ _
  po .Ob = ⌞ X ⌟
  po ._≤_ x y = x ≡ x X.∩ y
  po .≤-thin = hlevel 1
  po .≤-refl = sym X.idempotent

Proving that our now-familiar semilattice-induced order is a partial order reduces to a matter of algebra, which is presented without comment. Note that we do not need idempotence for transitivity or antisymmetry: it is only for reflexivity, where $x \le x$ directly translates to $x = x \land x$.

  po .≤-trans {x} {y} {z} x=x∧y y=y∧z =
    x                 ≡⟨ x=x∧y ⟩
    x X.∩ ⌜ y ⌝       ≡⟨ ap! y=y∧z ⟩
    x X.∩ (y X.∩ z)   ≡⟨ X.associative ⟩
    ⌜ x X.∩ y ⌝ X.∩ z ≡˘⟨ ap¡ x=x∧y ⟩
    x X.∩ z           ∎
  po .≤-antisym {x} {y} x=x∧y y=y∧x =
    x       ≡⟨ x=x∧y ⟩
    x X.∩ y ≡⟨ X.commutative ⟩
    y X.∩ x ≡˘⟨ y=y∧x ⟩
    y       ∎

And, formalising our comments about monotonicity from before, any semilattice homomorphism is a monotone map under the induced ordering.

Meet-semi-lattice .F₁ f .hom = f .hom
Meet-semi-lattice .F₁ f .pres-≤ p = ap (f .hom) p ∙ f .preserves .Monoid-hom.pres-⋆ _ _
Meet-semi-lattice .F-id    = trivial!
Meet-semi-lattice .F-∘ f g = trivial!

The interface🔗

This section is less about the mathematics per se, and more about how we formalise it. Semilattices (and lattices more generally) are an interesting structure, in that they are category-like in two different ways! In one direction, we have the the category structure by taking having a single Hom-set, and setting $a \cap b$ to be the composition operation — the delooping of the $\cap$ monoid. In the other direction, we have the poset structure, with the ordering induced by meets.

To effectively formalise mathematics to do with lattices, we need a convenient interface for both of these “categories”. We already have a fantastic module for working with morphisms in nontrivial categories: instantiating it with the delooping of the $\cap$ monoid means we get, for free, a bunch of combinators for handling big meet expressions.

module Semilattice {ℓ} (A : Semilattice ℓ) where
  po : Poset _ _
  po = Meet-semi-lattice .F₀ A
  open Order.Reasoning po public

  private module X = Semilattice-on (A .snd) renaming
            ( associative to ∩-assoc
            ; idl         to ∩-idl
            ; idr         to ∩-idr
            ; commutative to ∩-commutative
            ; idempotent  to ∩-idempotent
            )
  open X using ( top ; _∩_ ; ∩-assoc ; ∩-idl ; ∩-idr ; ∩-commutative ; ∩-idempotent ; ⋂ )
    public

  open Cat.Reasoning (B (Semilattice-on.to-monoid (A .snd)))
    hiding ( Ob ; Hom ; id ; _∘_ ; assoc ; idl ; idr ) public

As an example of reasoning about the lattice operator, let us prove that $x \cap y$ is indeed the meet of $x$ and $y$ in the induced ordering. It’s reduced to a bit of algebra:

  ∩-is-meet : ∀ {x y} → is-meet po x y (x ∩ y)
  ∩-is-meet {x} {y} .is-meet.meet≤l =
    x ∩ y       ≡⟨ pushl (sym ∩-idempotent) ⟩
    x ∩ (x ∩ y) ≡⟨ ∩-commutative ⟩
    (x ∩ y) ∩ x ∎
  ∩-is-meet {x} {y} .is-meet.meet≤r =
    x ∩ y       ≡˘⟨ pullr ∩-idempotent ⟩
    (x ∩ y) ∩ y ∎
  ∩-is-meet {x} {y} .is-meet.greatest lb lb=lb∧x lb=lb∧y =
    lb           ≡⟨ lb=lb∧y ⟩
    lb ∩ y       ≡⟨ pushl lb=lb∧x ⟩
    lb ∩ (x ∩ y) ∎