module Order.Lattice where

LatticesπŸ”—

A lattice is a poset which is a semilattice in two compatible, dual ways. We have a β€œmeet” semilattice (A,∩,⊀)(A, \cap, \top), and a β€œjoin” semilattice (A,βˆͺ,βŠ₯)(A, \cup, \bot) β€” and we take the order on AA induced by, for definiteness, the ∩\cap semilattice. The question is then: how do we write, algebraically, a condition on ∩\cap and βˆͺ\cup which guarantees that βˆͺ\cup provides (A,≀)(A, \le) with joins?

The answer is yes! Of course, since if it were not, this page would not be being written. A lattice structure on (A,⊀,βŠ₯,∩,βˆͺ)(A, \top, \bot, \cap, \cup) is a pair of semilattices (A,∩,⊀)(A, \cap, \top) and (A,βˆͺ,βŠ₯)(A, \cup, \bot), such that the ∩\cap and βˆͺ\cup 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 x≀yx \le y iff x=x∩yx = x \cap y, and the other is given by y=xβˆͺyy = x \cup y. As an exercise, try to work out that these are the same thing in the lattice of subsets of a fixed AA.

Really, there are four orderings we could imagine defining on a semilattice: x≀yx \le y iff. x=x∩yx = x \cap y, y=x∩yy = x \cap y, x=xβˆͺyx = x \cup y, and y=xβˆͺyy = x \cup y. The absorption laws serve to cut these possibilities in half, because using them we can show that x=x∩yx = x \cap y is the same as y=xβˆͺyy = x \cup y (and, respectively, y=x∩yy = x \cap y is the same as x=xβˆͺyx = x \cup y).

  βˆͺ-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 (A,s)β†’(A,t)(A, s) \to (A, t) β€” preservation of the operations guarantees that we get ⊀s=⊀t\top_s = \top_t (for each operation; βŠ₯\bot, ∩\cap and βˆͺ\cup), which eventually gives s=ts = t.

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 β„“)
Lattice : βˆ€ β„“ β†’ Type (lsuc β„“)
Lattice β„“ = Precategory.Ob (Lattices β„“)

record make-lattice {β„“} (A : Type β„“) : Type β„“ where
  no-eta-equality
  field
    has-is-set : is-set A
    cup : A β†’ A β†’ A
    cap : A β†’ A β†’ A
    top : A
    bot : A

    cup-assoc      : βˆ€ {x y z} β†’ cup x (cup y z) ≑ cup (cup x y) z
    cup-commutes   : βˆ€ {x y} β†’ cup x y ≑ cup y x
    cup-idempotent : βˆ€ {x} β†’ cup x x ≑ x
    cup-idl        : βˆ€ {x} β†’ cup bot x ≑ x

    cap-assoc      : βˆ€ {x y z} β†’ cap x (cap y z) ≑ cap (cap x y) z
    cap-commutes   : βˆ€ {x y} β†’ cap x y ≑ cap y x
    cap-idempotent : βˆ€ {x} β†’ cap x x ≑ x
    cap-idl        : βˆ€ {x} β†’ cap top x ≑ x

    cap-absorbs : βˆ€ {x y} β†’ cap x (cup x y) ≑ x
    cup-absorbs : βˆ€ {x y} β†’ cup x (cap x y) ≑ x

  make-meets : make-semilattice A
  make-meets .make-semilattice.has-is-set  = has-is-set
  make-meets .make-semilattice.top         = top
  make-meets .make-semilattice.op          = cap
  make-meets .make-semilattice.idl         = cap-idl
  make-meets .make-semilattice.associative = cap-assoc
  make-meets .make-semilattice.commutative = cap-commutes
  make-meets .make-semilattice.idempotent  = cap-idempotent

  make-joins : make-semilattice A
  make-joins .make-semilattice.has-is-set  = has-is-set
  make-joins .make-semilattice.top         = bot
  make-joins .make-semilattice.op          = cup
  make-joins .make-semilattice.idl         = cup-idl
  make-joins .make-semilattice.associative = cup-assoc
  make-joins .make-semilattice.commutative = cup-commutes
  make-joins .make-semilattice.idempotent  = cup-idempotent

open make-lattice
open Lattice-on
open is-lattice
open is-semilattice

to-lattice : βˆ€ {β„“} (A : Type β„“) β†’ make-lattice A β†’ Lattice β„“
∣ to-lattice A x .fst ∣ = A
to-lattice A x .fst .is-tr = x .has-is-set
to-lattice A x .snd .top = x .top
to-lattice A x .snd .bot = x .bot
to-lattice A x .snd ._∩_ = x .cap
to-lattice A x .snd ._βˆͺ_ = x .cup
to-lattice A x .snd .has-is-lattice .has-meets = to-semilattice-on (make-meets x) .Semilattice-on.has-is-semilattice
to-lattice A x .snd .has-is-lattice .has-joins = to-semilattice-on (make-joins x) .Semilattice-on.has-is-semilattice
to-lattice A x .snd .has-is-lattice .∩-absorbs-βˆͺ = x .cap-absorbs
to-lattice A x .snd .has-is-lattice .βˆͺ-absorbs-∩ = x .cup-absorbs