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 , 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?
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
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
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
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 β)