module Order.Lattice where
Latticesπ
A lattice is a poset which is a semilattice in two compatible, dual ways. We have a βmeetβ semilattice , and a βjoinβ semilattice β and we take the order on induced by, for definiteness, the semilattice. The question is then: how do we write, algebraically, a condition on and which guarantees that provides 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 is a pair of semilattices and , such that the and operations satisfy the two absorption laws with respect to eachother:
field has-meets : is-semilattice β€ _β©_ has-joins : is-semilattice β₯ _βͺ_ β©-absorbs-βͺ : β {x y} β x β© (x βͺ y) β‘ x βͺ-absorbs-β© : β {x y} β x βͺ (x β© y) β‘ x
open is-semilattice has-meets public renaming ( associative to β©-associative ; commutative to β©-commutative ; idempotent to β©-idempotent ; idl to β©-idl ; idr to β©-idr ) 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 iff , and the other is given by . As an exercise, try to work out that these are the same thing in the lattice of subsets of a fixed .
Really, there are four orderings we could imagine defining on a semilattice: iff. , , , and . The absorption laws serve to cut these possibilities in half, because using them we can show that is the same as (and, respectively, is the same as ).
βͺ-orderββ©-order : β {x y} β y β‘ x βͺ y β x β‘ x β© y βͺ-orderββ©-order {x} {y} y=xβͺy = x β‘Λβ¨ β©-absorbs-βͺ β©β‘Λ x β© β x βͺ y β β‘Λβ¨ apΒ‘ y=xβͺy β©β‘Λ x β© y β β©-orderββͺ-order : β {x y} β x β‘ x β© y β y β‘ x βͺ y β©-orderββͺ-order {x} {y} p = y β‘β¨ sym βͺ-absorbs-β© β©β‘ y βͺ β y β© x β β‘β¨ ap! β©-commutative β©β‘ y βͺ β x β© y β β‘Λβ¨ apΒ‘ p β©β‘Λ 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 .is-join.lβ€join = sym β©-absorbs-βͺ βͺ-is-join {x} {y} .is-join.rβ€join = y β‘Λβ¨ β©-absorbs-βͺ β©β‘Λ y β© β y βͺ x β β‘β¨ ap! βͺ-commutative β©β‘ y β© (x βͺ y) β βͺ-is-join {x} {y} .is-join.least ubβ² x=xβ©ubβ² y=yβ©ubβ² = βͺ-orderββ©-order $ sym $ (x βͺ y) βͺ ubβ² β‘Λβ¨ βͺ-associative β©β‘Λ x βͺ β y βͺ ubβ² β β‘Λβ¨ apΒ‘ (β©-orderββͺ-order y=yβ©ubβ²) β©β‘Λ x βͺ ubβ² β‘Λβ¨ β©-orderββͺ-order x=xβ©ubβ² β©β‘Λ ubβ² β β₯-is-bottom : β {x} β bot P.β€ x β₯-is-bottom = βͺ-orderββ©-order (sym βͺ-idl)
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 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-β© 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 β preservation of the operations guarantees that we get (for each operation; , and ), which eventually gives .
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 ._βͺ_ 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