Order.CompleteLattice

Complete Lattices

This is the Order.CompleteLattice module of the Agda Universal Algebra Library.

The standard library provides order-theoretic semilattices, lattices, and bounded lattices, but no complete lattice, so we define one here.

A complete lattice is a partially ordered set in which every family of elements (indexed by a type at a fixed level ι) has a supremum and an infimum.

Although this notion is pure order theory, complete lattices are pervasive in universal algebra — the congruence lattice (Setoid.Congruences.CompleteLattice) and the subalgebra lattice (Setoid.Subalgebras.CompleteLattice) are the motivating instances — so it lives in its own top-level Order/ tree. Note this is the order-theoretic notion of lattice (a poset with meets and joins); for lattices as equational algebras over Sig-Lattice see instead the Classical.*.Lattice modules (the two presentations are equivalent via a standard theorem). Every supremum/infimum is required to exist only for ι-small index types, the customary predicative reading of "complete."

{-# OPTIONS --cubical-compatible --exact-split --safe #-}

module Order.CompleteLattice where

open import Agda.Primitive   using () renaming ( Set to Type )

-- Imports from the Agda Standard Library ---------------------------------------
open import Level            using ( Level ; _⊔_ ; suc )
open import Relation.Binary  using ( IsPartialOrder ) renaming ( Rel to BinaryRel )

CompleteLattice c ℓ₁ ℓ₂ ι is a carrier at level c with an equality at level ℓ₁ and a partial order at level ℓ₂, such that every ι-indexed family has a least upper bound ⨆ and a greatest lower bound ⨅.

record CompleteLattice (c ℓ₁ ℓ₂ ι : Level) : Type (suc (c ⊔ ℓ₁ ⊔ ℓ₂ ⊔ ι)) where
  field
    Carrier         : Type c
    _≈_             : BinaryRel Carrier ℓ₁
    _≤_             : BinaryRel Carrier ℓ₂
    isPartialOrder  : IsPartialOrder _≈_ _≤_

    -- Infinitary supremum and infimum of an ι-indexed family.
    ⨆ : {I : Type ι} → (I → Carrier) → Carrier
    ⨅ : {I : Type ι} → (I → Carrier) → Carrier

    -- ⨆ f is the least upper bound of the family f.
    ⨆-upper  : {I : Type ι} (f : I → Carrier) (i : I) → f i ≤ ⨆ f
    ⨆-least  : {I : Type ι} (f : I → Carrier) (x : Carrier) → (∀ i → f i ≤ x) → ⨆ f ≤ x

    -- ⨅ f is the greatest lower bound of the family f.
    ⨅-lower     : {I : Type ι} (f : I → Carrier) (i : I) → ⨅ f ≤ f i
    ⨅-greatest  : {I : Type ι} (f : I → Carrier) (x : Carrier) → (∀ i → x ≤ f i) → x ≤ ⨅ f