open import 1Lab.Prelude

open import Algebra.Semilattice

open import Cat.Functor.Equivalence
open import Cat.Functor.Base
open import Cat.Prelude
open import Cat.Thin

module Algebra.Lattice where

LatticesšŸ”—

A lattice (A,∧,∨)(A, \land, \lor) is a pair of semilattices (A,∧)(A, \land) and (A,∨)(A, \lor) which ā€œfit togetherā€ with equations specifying that ∧\land and ∨\lor are duals, called absorption laws.

record is-lattice (_∧_ : A → A → A) (_∨_ : A → A → A) : Type (level-of A) where
  field
    has-meets : is-semilattice _∧_
    has-joins : is-semilattice _∨_
We rename the fields of has-meets and has-joins so they refer to the operator in their name, and hide anything extra from the hierarchy.
  open is-semilattice has-meets public
    renaming ( associative to ∧-associative
             ; commutative to ∧-commutative
             ; idempotent to ∧-idempotent
             )
    hiding ( has-is-magma ; has-is-semigroup )

  open is-semilattice has-joins public
    renaming ( associative to ∨-associative
             ; commutative to ∨-commutative
             ; idempotent to ∨-idempotent
             )
    hiding ( underlying-set ; has-is-magma ; has-is-set ; magma-hlevel )
  field
    ∧-absorbs-∨ : āˆ€ {x y} → (x ∧ (x ∨ y)) ≔ x
    ∨-absorbs-∧ : āˆ€ {x y} → (x ∨ (x ∧ y)) ≔ x

A lattice structure equips a type AA with two binary operators, the meet ∧\land and join ∨\lor, such that (A,∧,∨)(A, \land, \lor) is a lattice. Since being a semilattice includes being a set, this means that being a lattice is a property of (A,∧,∨)(A, \land, \lor):

private unquoteDecl eqv = declare-record-iso eqv (quote is-lattice)

instance
  H-Level-is-lattice : āˆ€ {M J : A → A → A} {n} → H-Level (is-lattice M J) (suc n)
  H-Level-is-lattice = prop-instance Ī» x →
    let open is-lattice x in is-hlevelā‰ƒ 1 (Iso→Equiv eqv e⁻¹) (hlevel 1) x

record Lattice-on (A : Type ā„“) : Type ā„“ where
  field
    _L∧_ : A → A → A
    _L∨_ : A → A → A

  infixr 40 _L∧_
  infixr 30 _L∨_

  field
    has-is-lattice : is-lattice _L∧_ _L∨_

  open is-lattice has-is-lattice public

  Lattice-on→is-meet-semi : is-semilattice _L∧_
  Lattice-on→is-meet-semi = has-meets

  Lattice-on→is-join-semi : is-semilattice _L∨_
  Lattice-on→is-join-semi = has-joins

open Lattice-on using (Lattice-on→is-meet-semi ; Lattice-on→is-join-semi) public

Lattice : āˆ€ ā„“ → Type (lsuc ā„“)
Lattice ℓ = Σ (Lattice-on {ℓ = ℓ})

Since the absorption laws are property, not structure, a lattice homomorphism turns out to be a function which is homomorphic for both semilattice structures, i.e.Ā one that independently preserves meets and joins.

record Lattice→ (A B : Lattice ā„“) (f : A .fst → B .fst) : Type ā„“ where
  private
    module A = Lattice-on (A .snd)
    module B = Lattice-on (B .snd)

  field
    pres-∧ : āˆ€ x y → f (x A.L∧ y) ≔ f x B.L∧ f y
    pres-∨ : āˆ€ x y → f (x A.L∨ y) ≔ f x B.L∨ f y

Latticeā‰ƒ : (A B : Lattice ā„“) (f : A .fst ā‰ƒ B .fst) → Type ā„“
Latticeā‰ƒ A B = Lattice→ A B ∘ fst

Using the automated machinery for deriving is-univalent proofs, we get that identification of lattices is the same thing as lattice isomorphism.

Lattice-univalent : āˆ€ {ā„“} → is-univalent (HomT→Str (Latticeā‰ƒ {ā„“ = ā„“}))
Lattice-univalent {ā„“ = ā„“} =
  Derive-univalent-record (record-desc (Lattice-on {ā„“ = ā„“}) Latticeā‰ƒ
    (record:
      field[ Lattice-on._L∧_ by Lattice→.pres-∧ ]
      field[ Lattice-on._L∨_ by Lattice→.pres-∨ ]
      axiom[ Lattice-on.has-is-lattice by (Ī» _ → hlevel 1) ]))

Order-theoreticallyšŸ”—

We already know that a given semilattice structure can induce one of two posets, depending on whether the semilattice operator is being considered as equipping the poset with meets or joins. We’d then expect that a lattice, having two semi-lattices, would have four poset structures. However, there are only two, which we call the ā€œcovariantā€ and ā€œcontravariantā€ orderings.

Lattice→covariant-on : Lattice-on A → Poset (level-of A) (level-of A)
Lattice→covariant-on lat = Semilattice-on→Meet-on (Lattice-on→is-meet-semi lat)

Lattice→contravariant-on : Lattice-on A → Poset (level-of A) (level-of A)
Lattice→contravariant-on lat = Semilattice-on→Join-on (Lattice-on→is-meet-semi lat)

Above, the ā€œcovariant orderā€ is obtaining by considering the (A,∧)(A, \land) semilattice as inducing meets on the poset (hence the operator being called ∧\land). It can also be obtained in a dual way, by considering that (A,∨)(A, \lor) induces joins on the poset. By the absorption laws, these constructions give rise to the same poset; We start by defining a monotone map (that is, a Functor) between the two possibilities:

covariant-order-map
  : (l : Lattice-on A)
  → Monotone-map
      (Semilattice-on→Meet-on (Lattice-on→is-meet-semi l))
      (Semilattice-on→Join-on (Lattice-on→is-join-semi l))
covariant-order-map {A = A} l = F where
  open Lattice-on l
    hiding (Lattice-on→is-join-semi ; Lattice-on→is-meet-semi)

  F : Monotone-map (Semilattice-on→Meet-on (Lattice-on→is-meet-semi l))
                   (Semilattice-on→Join-on (Lattice-on→is-join-semi l))
  F .Fā‚€ = id
  F .F₁ {x} {y} p = q where abstract
    q : y ≔ x L∨ y
    q =
      y             ā‰”āŸØ sym ∨-absorbs-∧ āŸ©ā‰”
      y L∨ (y L∧ x) ā‰”āŸØ apā‚‚ _L∨_ refl ∧-commutative āŸ©ā‰”
      y L∨ (x L∧ y) ā‰”āŸØ apā‚‚ _L∨_ refl (sym p) āŸ©ā‰”
      y L∨ x        ā‰”āŸØ ∨-commutative āŸ©ā‰”
      x L∨ y        āˆŽ
  F .F-id = has-is-set _ _ _ _
  F .F-∘ _ _ = has-is-set _ _ _ _

We now show that this functor is an equivalence: It is fully faithful and split essentially surjective.

covariant-order-map-is-equivalence
  : (l : Lattice-on A) → is-equivalence (covariant-order-map l)
covariant-order-map-is-equivalence l =
  ff+split-eso→is-equivalence ff eso
  where
    open Lattice-on l hiding (Lattice-on→is-join-semi)
    import
      Cat.Reasoning
        (Semilattice-on→Join-on (Lattice-on→is-join-semi l) .Poset.underlying)
      as D

A tiny calculation shows that this functor is fully faithful, and essential surjectivity is immediate:

    ff : is-fully-faithful (covariant-order-map l)
    ff {x} {y} .is-eqv p .centre .fst =
      x             ā‰”āŸØ sym ∧-absorbs-∨ āŸ©ā‰”
      x L∧ (x L∨ y) ā‰”āŸØ apā‚‚ _L∧_ refl (sym p) āŸ©ā‰”
      x L∧ y        āˆŽ
    ff .is-eqv y .centre .snd = has-is-set _ _ _ _
    ff .is-eqv y .paths x =
      Σ-path (has-is-set _ _ _ _)
             (is-prop→is-set (has-is-set _ _) _ _ _ _)

    eso : is-split-eso (covariant-order-map l)
    eso y .fst = y
    eso y .snd =
      D.make-iso (sym ∨-idempotent) (sym ∨-idempotent)
        (has-is-set _ _ _ _)
        (has-is-set _ _ _ _)