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 _βˆͺ_
  infixr 25 _∩_

  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-meet-slat .is-meet-semilattice.∩-meets = ∩-meets
  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

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

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 .∩-≀ =
  R .Poset.≀-trans (f-pres .∩-≀) (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!
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} {β„“}