open import Algebra.Monoid.Category
open import Algebra.Semigroup
open import Algebra.Monoid

open import Cat.Displayed.Univalence.Thin
open import Cat.Instances.Delooping
open import Cat.Prelude

open import Data.Fin.Base hiding (_≤_)

open import Order.Diagram.Glb
open import Order.Base

import Cat.Reasoning

import Order.Reasoning as Poset

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 ${\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


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 = 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 \le x$ directly translates to $x = 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 \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 \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) ∎


1. Really, either a meet semilattice or a join semilattice, when considered ordered-theoretically↩︎

2. Or a join, depending↩︎