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

open import Order.Diagram.Lub
open import Order.Semilattice
open import Order.Base

import Order.Reasoning as Pr

module Order.Lattice where


Latticesπ

A lattice is a poset which is a semilattice in two compatible, dual ways. We have a βmeetβ semilattice $(A, \cap, \top)$, and a βjoinβ semilattice $(A, \cup, \bot)$ β and we take the order on $A$ induced by, for definiteness, the $\cap$ semilattice. The question is then: how do we write, algebraically, a condition on $\cap$ and $\cup$ which guarantees that $\cup$ provides $(A, \le)$ with joins?

record
is-lattice
{β} {A : Type β}
(β€ : A) (_β©_ : A β A β A)
(β₯ : A) (_βͺ_ : A β A β A)
: Type β
where

no-eta-equality


The answer is yes! Of course, since if it were not, this page would not be being written. A lattice structure on $(A, \top, \bot, \cap, \cup)$ is a pair of semilattices $(A, \cap, \top)$ and $(A, \cup, \bot)$, such that the $\cap$ and $\cup$ operations satisfy the two absorption laws with respect to eachother:

  field
has-joins : is-semilattice β₯ _βͺ_

β©-absorbs-βͺ : β {x y} β x β© (x βͺ y) β‘ x
βͺ-absorbs-β© : β {x y} β x βͺ (x β© y) β‘ x

  open is-semilattice has-meets public
)
hiding ( has-is-magma ; has-is-semigroup )

open is-semilattice has-joins public
renaming ( associative to βͺ-associative
; commutative to βͺ-commutative
; idempotent  to βͺ-idempotent
; idl         to βͺ-idl
; idr         to βͺ-idr
)
hiding ( underlying-set ; has-is-magma ; has-is-set ; magma-hlevel )

private unquoteDecl eqv = declare-record-iso eqv (quote is-lattice)

instance
H-Level-is-lattice
: β {β} {A : Type β} {top bot : A} {meet join : A β A β A} {n}
β H-Level (is-lattice top meet bot join) (suc n)
H-Level-is-lattice = prop-instance Ξ» x β
let open is-lattice x in Isoβis-hlevel 1 eqv (hlevel 1) x


As usual, a lattice structure on a set is a record packaging together the operations and a proof that they are actually an instance of the algebraic structure weβre talking about.

record Lattice-on {β} (A : Type β) : Type β where
no-eta-equality
field
top : A
bot : A
_β©_ : A β A β A
_βͺ_ : A β A β A
has-is-lattice : is-lattice top _β©_ bot _βͺ_

open is-lattice has-is-lattice public

meets : Semilattice-on A
meets = record { has-is-semilattice = has-meets }

joins : Semilattice-on A
joins = record { has-is-semilattice = has-joins }

open Semilattice-on meets using (β) public
private module x = Semilattice-on joins renaming (β to β)
open x using (β) public

module _ {β} (L : Ξ£ (Set β) Ξ» A β Lattice-on β£ A β£) where
open Lattice-on (L .snd)

Latticeβposet : Poset β β
Latticeβposet =
Meet-semi-lattice .Functor.Fβ
(L .fst , record { has-is-semilattice = has-meets })

private module P = Pr Latticeβposet


The question then becomes: what is the point of the absorption laws? Iβll tell you! Since we have two semilattice structures on the set, we can imagine defining two orders on it: one is given by $x \le y$ iff $x = x \cap y$, and the other is given by $y = x \cup y$. As an exercise, try to work out that these are the same thing in the lattice of subsets of a fixed $A$.

Really, there are four orderings we could imagine defining on a semilattice: $x \le y$ iff. $x = x \cap y$, $y = x \cap y$, $x = x \cup y$, and $y = x \cup y$. The absorption laws serve to cut these possibilities in half, because using them we can show that $x = x \cap y$ is the same as $y = x \cup y$ (and, respectively, $y = x \cap y$ is the same as $x = x \cup y$).

  βͺ-orderββ©-order : β {x y} β y β‘ x βͺ y β x β‘ x β© y

β©-orderββͺ-order : β {x y} β x β‘ x β© y β y β‘ x βͺ y
y βͺ x         β‘β¨ βͺ-commutative β©β‘
x βͺ y         β


Using the βcup orderingβ, we can establish that cups provide a join of two elements. Since the cup ordering and the βcap orderingβ agree, we can prove that cups give a join in that case, too!

  βͺ-is-join : β {x y} β is-join Latticeβposet x y (x βͺ y)
βͺ-is-join {x} {y} .is-join.rβ€join =
y β© (x βͺ y)   β
βͺ-is-join {x} {y} .is-join.least ub' x=xβ©ub' y=yβ©ub' = βͺ-orderββ©-order $sym$
(x βͺ y) βͺ ub'   β‘Λβ¨ βͺ-associative β©β‘Λ
ub'             β

β₯-is-bottom : β {x} β bot P.β€ x


Category of latticesπ

A lattice homomorphism is a function which is, at the same time, a homomorphism for both of the semilattice monoid structures: A function sending bottom to bottom, top to top, joins to joins, and meets to meets. Put more concisely, a function which preserves finite meets and finite joins.

record
is-lattice-hom
{β β'} {A : Type β} {B : Type β'}
(f : A β B)
(S : Lattice-on A) (T : Lattice-on B)
: Type (β β β')
where

private
module S = Lattice-on S
module T = Lattice-on T

field
pres-β€ : f S.top β‘ T.top
pres-β₯ : f S.bot β‘ T.bot
pres-βͺ : β {x y} β f (x S.βͺ y) β‘ f x T.βͺ f y

private unquoteDecl eqv' = declare-record-iso eqv' (quote is-lattice-hom)

instance
H-Level-is-lattice-hom
: β {β β'} {A : Type β} {B : Type β'}
β {S : Lattice-on A} {T : Lattice-on B}
β β {f : A β B} {n}
β H-Level (is-lattice-hom f S T) (suc n)
H-Level-is-lattice-hom {T = T} = prop-instance \$
let open is-lattice (T .Lattice-on.has-is-lattice)
in Isoβis-hlevel 1 eqv' (hlevel 1)

open is-lattice-hom


Standard equational nonsense implies that (a) lattices and lattice homomorphisms form a precategory; and (b) this is a univalent category.

Lattice-structure : β β β Thin-structure β Lattice-on

Lattice-structure β .is-hom f S T .β£_β£   = is-lattice-hom f S T
Lattice-structure β .is-hom f S T .is-tr = hlevel!

Lattice-structure β .id-is-hom .pres-β€ = refl
Lattice-structure β .id-is-hom .pres-β₯ = refl
Lattice-structure β .id-is-hom .pres-β© = refl
Lattice-structure β .id-is-hom .pres-βͺ = refl

Lattice-structure β .β-is-hom f g Ξ± Ξ² .pres-β€ = ap f (Ξ² .pres-β€) β Ξ± .pres-β€
Lattice-structure β .β-is-hom f g Ξ± Ξ² .pres-β₯ = ap f (Ξ² .pres-β₯) β Ξ± .pres-β₯
Lattice-structure β .β-is-hom f g Ξ± Ξ² .pres-βͺ = ap f (Ξ² .pres-βͺ) β Ξ± .pres-βͺ


Univalence follows from the special case of considering the identity as a lattice homomorphism $(A, s) \to (A, t)$ β preservation of the operations guarantees that we get $\top_s = \top_t$ (for each operation; $\bot$, $\cap$ and $\cup$), which eventually gives $s = t$.

Lattice-structure β .id-hom-unique {s = s} {t = t} Ξ± _ = p where
open Lattice-on
p : s β‘ t
p i .top = Ξ± .pres-β€ i
p i .bot = Ξ± .pres-β₯ i
p i ._βͺ_ x y = Ξ± .pres-βͺ {x} {y} i
p i .has-is-lattice =
is-propβpathp
(Ξ» i β hlevel {T = is-lattice (Ξ± .pres-β€ i) (Ξ» x y β Ξ± .pres-β© i)
(Ξ± .pres-β₯ i) (Ξ» x y β Ξ± .pres-βͺ i)}
1)
(s .has-is-lattice) (t .has-is-lattice) i

Lattices : β β β Precategory (lsuc β) β
Lattices β = Structured-objects (Lattice-structure β)

Lattice : β β β Type (lsuc β)
Lattice β = Precategory.Ob (Lattices β)

record make-lattice {β} (A : Type β) : Type β where
no-eta-equality
field
has-is-set : is-set A
cup : A β A β A
cap : A β A β A
top : A
bot : A

cup-assoc      : β {x y z} β cup x (cup y z) β‘ cup (cup x y) z
cup-commutes   : β {x y} β cup x y β‘ cup y x
cup-idempotent : β {x} β cup x x β‘ x
cup-idl        : β {x} β cup bot x β‘ x

cap-assoc      : β {x y z} β cap x (cap y z) β‘ cap (cap x y) z
cap-commutes   : β {x y} β cap x y β‘ cap y x
cap-idempotent : β {x} β cap x x β‘ x
cap-idl        : β {x} β cap top x β‘ x

cap-absorbs : β {x y} β cap x (cup x y) β‘ x
cup-absorbs : β {x y} β cup x (cap x y) β‘ x

make-meets : make-semilattice A
make-meets .make-semilattice.has-is-set  = has-is-set
make-meets .make-semilattice.top         = top
make-meets .make-semilattice.op          = cap
make-meets .make-semilattice.idl         = cap-idl
make-meets .make-semilattice.associative = cap-assoc
make-meets .make-semilattice.commutative = cap-commutes
make-meets .make-semilattice.idempotent  = cap-idempotent

make-joins : make-semilattice A
make-joins .make-semilattice.has-is-set  = has-is-set
make-joins .make-semilattice.top         = bot
make-joins .make-semilattice.op          = cup
make-joins .make-semilattice.idl         = cup-idl
make-joins .make-semilattice.associative = cup-assoc
make-joins .make-semilattice.commutative = cup-commutes
make-joins .make-semilattice.idempotent  = cup-idempotent

open make-lattice
open Lattice-on
open is-lattice
open is-semilattice

to-lattice : β {β} (A : Type β) β make-lattice A β Lattice β
β£ to-lattice A x .fst β£ = A
to-lattice A x .fst .is-tr = x .has-is-set
to-lattice A x .snd .top = x .top
to-lattice A x .snd .bot = x .bot
to-lattice A x .snd ._β©_ = x .cap
to-lattice A x .snd ._βͺ_ = x .cup
to-lattice A x .snd .has-is-lattice .has-meets = to-semilattice-on (make-meets x) .Semilattice-on.has-is-semilattice
to-lattice A x .snd .has-is-lattice .has-joins = to-semilattice-on (make-joins x) .Semilattice-on.has-is-semilattice
to-lattice A x .snd .has-is-lattice .β©-absorbs-βͺ = x .cap-absorbs
to-lattice A x .snd .has-is-lattice .βͺ-absorbs-β© = x .cup-absorbs