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, \land, \lor)$ is a pair of semilattices $(A, \land)$ and $(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 $A$ with two binary operators, the meet $\land$ and join $\lor$, such that $(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, \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, \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, \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 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 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 _ _ _ _)