module Order.Semilattice where

SemilatticesπŸ”—

A semilattice1 is a partially ordered set where every finite family of elements has a meet2. 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 N\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! XX is a subset of YY iff. the intersection of XX and YY is XX. Check this for yourself: The intersection of (e.g.) X={1,2,3}X = \{ 1, 2, 3 \} and Y={1,2,3,4,5}Y = \{ 1, 2, 3, 4, 5 \} is just {1,2,3}\{ 1, 2, 3 \} again, so XβŠ†YX \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

Rather than going through the usual displayed structure dance, here we exhibit semilattices through an embedding into monoids: when (A,⊀,∩)(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β†’Bf : A \to B is a semilattice homomorphism when f(⊀)=⊀f(\top) = \top and f(x∩y)=f(x)∩f(y)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)≀f(y)f(x) \le f(y) to mean f(x)=f(x)∩f(y)f(x) = f(x) \cap f(y), which by preservation of meets means f(x)=f(x∩y)f(x) = f(x \cap y) β€” which is certainly the casae if x=x∩yx = x \cap y, i.e., x≀yx \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≀yx \le y to mean x=x∩yx = 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 = X .fst , po where
  open Poset-on
  open is-partial-order
  module X = Semilattice-on (X .snd)
  po : Poset-on _ ⌞ X ⌟
  po ._≀_ x y = x ≑ x X.∩ y
  po .has-is-poset .≀-thin = hlevel 1
  po .has-is-poset .≀-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≀xx \le x directly translates to x=x∧xx = x \land x.

  po .has-is-poset .≀-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 .has-is-poset .≀-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 .preserves x y p = ap (f .hom) p βˆ™ f .preserves .Monoid-hom.pres-⋆ _ _
Meet-semi-lattice .F-id    = Homomorphism-path Ξ» _ β†’ refl
Meet-semi-lattice .F-∘ f g = Homomorphism-path Ξ» _ β†’ refl

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∩ba \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 Poset 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∩yx \cap y is indeed the meet of xx and yy 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) ∎
  private module Y {x} {y} = is-meet (∩-is-meet {x} {y}) renaming (meet≀l to βˆ©β‰€l ; meet≀r to βˆ©β‰€r ; greatest to ∩-univ)
  open Y public

  β‹‚-is-glb : βˆ€ {n} (f : Fin n β†’ ⌞ A ⌟) β†’ is-glb po f (β‹‚ f)
  β‹‚-is-glb {zero} f .is-glb.glb≀fam ()
  β‹‚-is-glb {zero} f .is-glb.greatest lbβ€² x = sym ∩-idr
  β‹‚-is-glb {suc n} f = go where
    those : is-glb po (Ξ» i β†’ f (fsuc i)) _
    those = β‹‚-is-glb _

    go : is-glb po f (f fzero ∩ β‹‚ (Ξ» i β†’ f (fsuc i)))
    go .is-glb.glb≀fam fzero = βˆ©β‰€l
    go .is-glb.glb≀fam (fsuc i) =
      f fzero ∩ β‹‚ (Ξ» i β†’ f (fsuc i))   β‰€βŸ¨ βˆ©β‰€r βŸ©β‰€
      β‹‚ (Ξ» i β†’ f (fsuc i))             β‰€βŸ¨ those .is-glb.glb≀fam i βŸ©β‰€
      f (fsuc i)                       β‰€βˆŽ
    go .is-glb.greatest lbβ€² f≀lbβ€² =
      ∩-univ lbβ€² (f≀lbβ€² fzero) (those .is-glb.greatest lbβ€² (Ξ» i β†’ f≀lbβ€² (fsuc i)))

module
  _ {β„“ β„“β€²} {A : Type β„“} {B : Type β„“β€²}
    (S : Semilattice-on A) (T : Semilattice-on B)
    (f : A β†’ B)
    (fh : Monoid-hom (Semilattice-on.to-monoid S) (Semilattice-on.to-monoid T) f)
  where
  private
    module S = Semilattice-on S
    module T = Semilattice-on T
    open Monoid-hom

  slat-pres-β‹‚ : βˆ€ {n} (d : Fin n β†’ A) β†’ f (S.β‹‚ d) ≑ T.β‹‚ (Ξ» i β†’ f (d i))
  slat-pres-β‹‚ {n = zero} d = fh .pres-id
  slat-pres-β‹‚ {n = suc n} d =
    f (d fzero S.∩ S.β‹‚ (Ξ» i β†’ d (fsuc i)))     β‰‘βŸ¨ fh .pres-⋆ _ _ βŸ©β‰‘
    f (d fzero) T.∩ f (S.β‹‚ Ξ» i β†’ d (fsuc i))   β‰‘βŸ¨ apβ‚‚ T._∩_ refl (slat-pres-β‹‚ Ξ» i β†’ d (fsuc i)) βŸ©β‰‘
    f (d fzero) T.∩ T.β‹‚ (Ξ» i β†’ f (d (fsuc i))) ∎

  1. Really, either a meet semilattice or a join semilattice, when considered ordered-theoreticallyβ†©οΈŽ

  2. Or a join, dependingβ†©οΈŽ