open import Cat.Functor.Subcategory
open import Cat.Prelude

open import Order.Semilattice.Join
open import Order.Semilattice.Meet
open import Order.Diagram.Bottom
open import Order.Diagram.Join
open import Order.Diagram.Meet
open import Order.Diagram.Top
open import Order.Base

import Cat.Reasoning

import Order.Diagram.Join.Reasoning as Joins
import Order.Diagram.Meet.Reasoning as Meets
import Order.Reasoning

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 β
β©-meets : β x y β is-meet P x y (x β© y)

_βͺ_     : β P β β β P β β β P β
βͺ-joins : β x y β is-join P x y (x βͺ y)

has-top : Top P
has-bottom : Bottom P

infixr 24 _βͺ_

open Joins {P = P} βͺ-joins public
open Meets {P = P} β©-meets public

has-meet-slat : is-meet-semilattice P
has-meet-slat .is-meet-semilattice.has-top = has-top

has-join-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

open Top has-top using (top ; !) public
open Bottom has-bottom using (bot ; Β‘) public

private
variable
o β o' β' : Level
P Q R : Poset o β

is-lattice-is-prop : is-prop (is-lattice P)
is-lattice-is-prop {P = P} p q = path where
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

joinp : β x y β x p.βͺ y β‘ x q.βͺ y
joinp x y = join-unique (p.βͺ-joins x y) (q.βͺ-joins x y)

meetp : β x y β x p.β© y β‘ x q.β© y

path : p β‘ q
path i ._βͺ_ x y = joinp x y i
path i ._β©_ x y = meetp x y i
path i .βͺ-joins x y = is-propβpathp
(Ξ» i β hlevel {T = is-join P x y (joinp x y i)} 1)
(p.βͺ-joins x y) (q.βͺ-joins x y) i
path i .β©-meets x y = is-propβpathp
(Ξ» i β hlevel {T = is-meet P x y (meetp x y i)} 1)
path 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

instance
H-Level-is-lattice
: β {n} β H-Level (is-lattice P) (suc n)
H-Level-is-lattice = prop-instance is-lattice-is-prop


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
top-β€ : T.top Q.β€ f # S.top
bot-β€ : f # S.bot Q.β€ T.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
id-lattice-hom {P = P} L .top-β€ =
Poset.β€-refl P
id-lattice-hom {P = P} L .bot-β€ =
Poset.β€-refl P
id-lattice-hom {P = P} L .β©-β€ =
Poset.β€-refl P
id-lattice-hom {P = P} L .βͺ-β€ =
Poset.β€-refl P

β-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
β-lattice-hom {R = R} {f = f} f-pres g-pres .top-β€ =
R .Poset.β€-trans (f-pres .top-β€) (f .pres-β€ (g-pres .top-β€))
β-lattice-hom {R = R} {f = f} f-pres g-pres .bot-β€ =
R .Poset.β€-trans (f .pres-β€ (g-pres .bot-β€)) (f-pres .bot-β€)
β-lattice-hom {R = R} {f = f} f-pres g-pres .β©-β€ =
β-lattice-hom {R = R} {f = f} f-pres g-pres .βͺ-β€ =
R .Poset.β€-trans (f .pres-β€ (g-pres .βͺ-β€)) (f-pres .βͺ-β€)


This allows us to carve out the category of lattices as a subcategory of the category of posets.

Lattices-subcat : β o β β Subcat (Posets o β) _ _
Lattices-subcat o β .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 : β o β β Precategory _ _
Lattices o β = Subcategory (Lattices-subcat o β)

module Lattices {o} {β} = Cat.Reasoning (Lattices o β)

Lattice : β o β β Type _
Lattice o β = Lattices.Ob {o} {β}