Classical.Structures.Lattice

Lattices

This is the Classical.Structures.Lattice module of the Agda Universal Algebra Library.

This is a barrel module: it declares nothing of its own and re-exports the eight modules that develop lattices in the Classical/ tree. A lattice here is an algebra over Sig-Lattice satisfying Th-Lattice, that is, the equational presentation; the order-theoretic presentation, in which meet and join are recovered as the infimum and supremum of a partial order, is what Setoid.Subalgebras.CompleteLattice and Setoid.Congruences.CompleteLattice build instead.

Guide to the submodules of Classical.Structures.Lattice

• Classical.Structures.Lattice.Basic: the type Lattice itself, the two magma reducts, and the named accessors;
• Classical.Structures.Lattice.DistributiveLattice: the same signature with distributivity added to the theory;
• Classical.Structures.Lattice.Dual: meet and join exchanged. Since Th-Lattice is self-dual the construction needs no new equations. Dualizing twice recovers each operation pointwise, but the involution is not formalized there, because stating it as an equality of Lattice values would need function extensionality and no consumer has required it;
• Classical.Structures.Lattice.Free: the free lattice FL(X), with Whitman's decision procedure for its order, its universal property, and the bridge that makes derivable equality under Th-Lattice decidable;
• Classical.Structures.Lattice.FilterIdeal: principal filters and principal ideals, and the fact that the union of a principal filter and a principal ideal is again a sublattice universe;
• Classical.Structures.Lattice.Product: the direct product of two lattices, coordinatewise;
• Classical.Structures.Lattice.OrdinalSum: one lattice stacked on another with the top of the lower glued to the bottom of the upper, written L ⊕ₐ M;
• Classical.Structures.Lattice.Partitions: the partition lattice Eq(n), the equivalence relations on an n-element set ordered by refinement.

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

module Classical.Structures.Lattice where

open import Classical.Structures.Lattice.Basic                public
open import Classical.Structures.Lattice.DistributiveLattice  public
open import Classical.Structures.Lattice.Dual                 public
open import Classical.Structures.Lattice.FilterIdeal          public
open import Classical.Structures.Lattice.Free                 public
open import Classical.Structures.Lattice.OrdinalSum           public
open import Classical.Structures.Lattice.Partitions           public
open import Classical.Structures.Lattice.Product              public