module Order.Lattice where
Latticesπ
A lattice is a poset which is simultaneously a meet semilattice and a join semilattice.
record is-lattice {o β} (P : Poset o β) : Type (o β β) where
no-eta-equality
field
_β©_ : β P β β β P β β β P β
: β x y β is-meet P x y (x β© y)
β©-meets
_βͺ_ : β P β β β P β β β P β
: β x y β is-join P x y (x βͺ y)
βͺ-joins
: Top P
has-top : Bottom P
has-bottom
infixr 24 _βͺ_
infixr 25 _β©_
open Joins {P = P} βͺ-joins public
open Meets {P = P} β©-meets public
: is-meet-semilattice P
has-meet-slat .is-meet-semilattice._β©_ = _β©_
has-meet-slat .is-meet-semilattice.β©-meets = β©-meets
has-meet-slat .is-meet-semilattice.has-top = has-top
has-meet-slat
: is-join-semilattice P
has-join-slat .is-join-semilattice._βͺ_ = _βͺ_
has-join-slat .is-join-semilattice.βͺ-joins = βͺ-joins
has-join-slat .is-join-semilattice.has-bottom = has-bottom
has-join-slat
open Top has-top using (top ; !) public
open Bottom has-bottom using (bot ; Β‘) public
private
variable
: Level
o β o' β' : Poset o β
P Q R
: is-prop (is-lattice P)
is-lattice-is-prop {P = P} p q = path where
is-lattice-is-prop open Order.Diagram.Top P using (H-Level-Top)
open Order.Diagram.Bottom P using (H-Level-Bottom)
module p = is-lattice p
module q = is-lattice q
open is-lattice
: β x y β x p.βͺ y β‘ x q.βͺ y
joinp = join-unique (p.βͺ-joins x y) (q.βͺ-joins x y)
joinp x y
: β x y β x p.β© y β‘ x q.β© y
meetp = meet-unique (p.β©-meets x y) (q.β©-meets x y)
meetp x y
: p β‘ q
path ._βͺ_ x y = joinp x y i
path i ._β©_ x y = meetp x y i
path i .βͺ-joins x y = is-propβpathp
path i (Ξ» i β hlevel {T = is-join P x y (joinp x y i)} 1)
(p.βͺ-joins x y) (q.βͺ-joins x y) i
.β©-meets x y = is-propβpathp
path i (Ξ» i β hlevel {T = is-meet P x y (meetp x y i)} 1)
(p.β©-meets x y) (q.β©-meets x y) i
.has-top = hlevel {T = Top P} 1 p.has-top q.has-top i
path i .has-bottom = hlevel {T = Bottom P} 1 p.has-bottom q.has-bottom i
path i
instance
H-Level-is-lattice: β {n} β H-Level (is-lattice P) (suc n)
= prop-instance is-lattice-is-prop H-Level-is-lattice
Category of latticesπ
A lattice homomorphism is a function which is, at the same time, a homomorphism for both of the semilattice 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{P : Poset o β} {Q : Poset o' β'}
(f : Monotone P Q) (S : is-lattice P) (T : is-lattice Q) : Type (o β β')
where
private
module P = Poset P
module Q = Order.Reasoning Q
module S = is-lattice S
module T = is-lattice T
field
: T.top Q.β€ f # S.top
top-β€ : f # S.bot Q.β€ T.bot
bot-β€ : β {x y} β f # x T.β© f # y Q.β€ f # (x S.β© y)
β©-β€ : β {x y} β f # (x S.βͺ y) Q.β€ f # x T.βͺ f # y βͺ-β€
unquoteDecl H-Level-is-lattice-hom = declare-record-hlevel 1 H-Level-is-lattice-hom (quote is-lattice-hom)
open is-lattice-hom
The identity function is clearly a lattice homomorphism, and lattice homomorphisms are closed under composition.
id-lattice-hom: β (L : is-lattice P)
β is-lattice-hom idβ L L
{P = P} L .top-β€ =
id-lattice-hom .β€-refl P
Poset{P = P} L .bot-β€ =
id-lattice-hom .β€-refl P
Poset{P = P} L .β©-β€ =
id-lattice-hom .β€-refl P
Poset{P = P} L .βͺ-β€ =
id-lattice-hom .β€-refl P
Poset
β-lattice-hom: β {L J K} {f : Monotone Q R} {g : Monotone P Q}
β is-lattice-hom f J K
β is-lattice-hom g L J
β is-lattice-hom (f ββ g) L K
{R = R} {f = f} f-pres g-pres .top-β€ =
β-lattice-hom .Poset.β€-trans (f-pres .top-β€) (f .pres-β€ (g-pres .top-β€))
R {R = R} {f = f} f-pres g-pres .bot-β€ =
β-lattice-hom .Poset.β€-trans (f .pres-β€ (g-pres .bot-β€)) (f-pres .bot-β€)
R {R = R} {f = f} f-pres g-pres .β©-β€ =
β-lattice-hom .Poset.β€-trans (f-pres .β©-β€) (f .pres-β€ (g-pres .β©-β€))
R {R = R} {f = f} f-pres g-pres .βͺ-β€ =
β-lattice-hom .Poset.β€-trans (f .pres-β€ (g-pres .βͺ-β€)) (f-pres .βͺ-β€) R
This allows us to carve out the category of lattices as a subcategory of the category of posets.
: β o β β Subcat (Posets o β) _ _
Lattices-subcat .Subcat.is-ob = is-lattice
Lattices-subcat o β .Subcat.is-hom = is-lattice-hom
Lattices-subcat o β .Subcat.is-hom-prop _ _ _ = hlevel 1
Lattices-subcat o β .Subcat.is-hom-id = id-lattice-hom
Lattices-subcat o β .Subcat.is-hom-β = β-lattice-hom
Lattices-subcat o β
: β o β β Precategory _ _
Lattices = Subcategory (Lattices-subcat o β)
Lattices o β
module Lattices {o} {β} = Cat.Reasoning (Lattices o β)
: β o β β Type _
Lattice = Lattices.Ob {o} {β} Lattice o β