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

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
  meetp x y = meet-unique (p.∩-meets x y) (q.∩-meets x 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)
    (p.∩-meets x y) (q.∩-meets x y) i
  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 .∩-≀ =
  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 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} {β„“}