Lattices.Examples.N5¶

Worked example: the pentagon `N₅`¶

This is the Lattices.Examples.N5 module of the agda-lattices library.

The pentagon N₅ has a bottom ⊥, a top ⊤, a two-element chain a < c between them, and an element b incomparable to both: ⊥ < a < c < ⊤ and ⊥ < b < ⊤. It is the smallest lattice that is not modular. Unlike the diamond of Lattices.Examples.M3, it satisfies all three conditions of Lattices.Semidistributive: both semidistributive laws and Whitman's condition (W). By Nation's theorem (Freese, Ježek, and Nation (1995), Theorem 5.55), a finite lattice with these three properties is a sublattice of a free lattice, so N₅ is one. For N₅ this is also elementary: N₅ is generated by a, b, and c, so FL(3) maps onto it, and FL(3) is therefore not modular; by Dedekind's criterion a lattice that is not modular has a sublattice isomorphic to N₅.

As for M₃, the lattice is given by its tables through Lattices.Table, and the three verdicts are the values of the decision procedures, extracted by from-yes.

{-# OPTIONS --without-K --exact-split --safe #-}

module Lattices.Examples.N5 where

-- Imports from the Agda Standard Library ---------------------------------------
open import Data.Fin.Base                          using ( Fin )
open import Data.Fin.Patterns                      using ( 0F ; 1F ; 2F ; 3F ; 4F )
open import Data.Product                           using ( proj₁ )
open import Data.Vec.Base                          using ( _∷_ ; [] )
open import Level                                  using ( 0ℓ )

-- Imports from the Agda Universal Algebra Library ------------------------------
open import Lattices.Semidistributive
  using  ( IsJoinSemidistributive ; IsMeetSemidistributive ; SatisfiesW
         ; isJoinSemidistributive? ; isMeetSemidistributive? ; satisfiesW? )
open import Classical.Structures.Lattice.Basic  using ( Lattice )
open import Lattices.Table  using ( LatticeTableLaws ; latticeTableLaws?
                                                      ; tableLattice ; tableLattice-FiniteAlgebra )
open import Overture.Cayley                     using ( Table ; ⟦_⟧ ; from-yes )
open import Setoid.Algebras.Finite              using ( FiniteAlgebra )

The tables¶

The carrier is Fin 5, with ⊥, a, b, c, ⊤ numbered 0 to 4.

`∧`	⊥	a	b	c	⊤	`∨`	⊥	a	b	c	⊤
⊥	⊥	⊥	⊥	⊥	⊥	⊥	⊥	a	b	c	⊤
a	⊥	a	⊥	a	a	a	a	a	⊤	c	⊤
b	⊥	⊥	b	⊥	b	b	b	⊤	b	⊤	⊤
c	⊥	a	⊥	c	c	c	c	c	⊤	c	⊤
⊤	⊥	a	b	c	⊤	⊤	⊤	⊤	⊤	⊤	⊤

infixl 7 _∧_ _∨_

⊥ a b c ⊤ : Fin 5
⊥ = 0F
a = 1F
b = 2F
c = 3F
⊤ = 4F

∧-table : Table 5
∧-table = (0F ∷ 0F ∷ 0F ∷ 0F ∷ 0F ∷ [])
        ∷ (0F ∷ 1F ∷ 0F ∷ 1F ∷ 1F ∷ [])
        ∷ (0F ∷ 0F ∷ 2F ∷ 0F ∷ 2F ∷ [])
        ∷ (0F ∷ 1F ∷ 0F ∷ 3F ∷ 3F ∷ [])
        ∷ (0F ∷ 1F ∷ 2F ∷ 3F ∷ 4F ∷ [])
        ∷ []

∨-table : Table 5
∨-table = (0F ∷ 1F ∷ 2F ∷ 3F ∷ 4F ∷ [])
        ∷ (1F ∷ 1F ∷ 4F ∷ 3F ∷ 4F ∷ [])
        ∷ (2F ∷ 4F ∷ 2F ∷ 4F ∷ 4F ∷ [])
        ∷ (3F ∷ 3F ∷ 4F ∷ 3F ∷ 4F ∷ [])
        ∷ (4F ∷ 4F ∷ 4F ∷ 4F ∷ 4F ∷ [])
        ∷ []

_∧_ _∨_ : Fin 5 → Fin 5 → Fin 5
_∧_ = ⟦ ∧-table ⟧
_∨_ = ⟦ ∨-table ⟧

The lattice¶

As for M₃, the laws are decided (N₅-laws), and the lattice N₅ and its enumeration N₅-finite are built from them.

N₅-laws : LatticeTableLaws _∧_ _∨_
N₅-laws = from-yes (latticeTableLaws? _∧_ _∨_)

N₅ : Lattice 0ℓ 0ℓ
N₅ = tableLattice _∧_ _∨_ N₅-laws

N₅-finite : FiniteAlgebra (proj₁ N₅)
N₅-finite = tableLattice-FiniteAlgebra _∧_ _∨_ N₅-laws

The verdicts¶

All three procedures answer yes.

N₅-joinSemidistributive : IsJoinSemidistributive N₅
N₅-joinSemidistributive = from-yes (isJoinSemidistributive? N₅ N₅-finite)

N₅-meetSemidistributive : IsMeetSemidistributive N₅
N₅-meetSemidistributive = from-yes (isMeetSemidistributive? N₅ N₅-finite)

N₅-satisfiesW : SatisfiesW N₅
N₅-satisfiesW = from-yes (satisfiesW? N₅ N₅-finite)

`∧`	⊥	a	b	c	⊤	`∨`	⊥	a	b	c	⊤
⊥	⊥	⊥	⊥	⊥	⊥	⊥	⊥	a	b	c	⊤
a	⊥	a	⊥	a	a	a	a	a	⊤	c	⊤
b	⊥	⊥	b	⊥	b	b	b	⊤	b	⊤	⊤
c	⊥	a	⊥	c	c	c	c	c	⊤	c	⊤
⊤	⊥	a	b	c	⊤	⊤	⊤	⊤	⊤	⊤	⊤

`∧`	⊥	a	b	c	⊤	`∨`	⊥	a	b	c	⊤
⊥	⊥	⊥	⊥	⊥	⊥	⊥	⊥	a	b	c	⊤
a	⊥	a	⊥	a	a	a	a	a	⊤	c	⊤
b	⊥	⊥	b	⊥	b	b	b	⊤	b	⊤	⊤
c	⊥	a	⊥	c	c	c	c	c	⊤	c	⊤
⊤	⊥	a	b	c	⊤	⊤	⊤	⊤	⊤	⊤	⊤

Lattices.Examples.N5¶

Worked example: the pentagon N₅¶

The tables¶

The lattice¶

The verdicts¶

Worked example: the pentagon `N₅`¶

`∧`	⊥	a	b	c	⊤	`∨`	⊥	a	b	c	⊤
⊥	⊥	⊥	⊥	⊥	⊥	⊥	⊥	a	b	c	⊤
a	⊥	a	⊥	a	a	a	a	a	⊤	c	⊤
b	⊥	⊥	b	⊥	b	b	b	⊤	b	⊤	⊤
c	⊥	a	⊥	c	c	c	c	c	⊤	c	⊤
⊤	⊥	a	b	c	⊤	⊤	⊤	⊤	⊤	⊤	⊤