 Closure Systems and Operators

This is the Adjunction.Closure module of the Agda Universal Algebra Library.

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

-- Imports from Agda and the Agda Standard Library  ---------------------------------------
open import Agda.Primitive          using ( _⊔_ ; lsuc ) renaming ( Set to Type )
import Algebra.Definitions
open import Data.Product            using ( Σ-syntax ; _,_ ; _×_ )
open import Function.Bundles        using ( _↔_ ; Inverse )
open import Level                   using ( Level ; Lift ) renaming ( zero to ℓ₀ )
open import Relation.Binary.Bundles using ( Poset )
open import Relation.Binary.Core    using ( Rel ; _Preserves_⟶_ )
open import Relation.Unary          using ( Pred ; _∈_ ;  )
import Relation.Binary.Reasoning.PartialOrder as ≤-Reasoning

private variable
α ρ  ℓ₁ ℓ₂ : Level
a : Type α

Closure Systems

A closure system on a set X is a collection 𝒞 of subsets of X that is closed under arbitrary intersection (including the empty intersection, so ⋂ ∅ = X ∈ 𝒞. Thus a closure system is a complete meet semilattice with respect to the subset inclusion ordering.

Since every complete meet semilattice is automatically a complete lattice, the closed sets of a closure system form a complete lattice. (See J.B. Nation’s Lattice Theory Notes, Theorem 2.5.)

Some examples of closure systems are the following:

• order ideals of an ordered set
• subalgebras of an algebra
• equivalence relations on a set
• congruence relations of an algebra
Extensive : Rel a ρ  (a  a)  Type _
Extensive _≤_ C = ∀{x}  x  C x
-- (We might propose a new stdlib equivalent to Extensive in, e.g., `Relation.Binary.Core`.)

module _ {χ ρ  : Level}{X : Type χ} where

IntersectClosed : Pred (Pred X ) ρ  Type _
IntersectClosed C =  {I : Type }{c : I  Pred X }  (∀ i  (c i)  C)   I c  C

ClosureSystem : Type _
ClosureSystem = Σ[ C  Pred (Pred X ) ρ ] IntersectClosed C

Closure Operators

Let 𝑷 = (P, ≤) be a poset. An function C : P → P is called a closure operator on 𝑷 if it is

1. (extensive) ∀ x → x ≤ C x
2. (order preserving) ∀ x y → x ≤ y → C x ≤ C y
3. (idempotent) ∀ x → C (C x) = C x

Thus, a closure operator is an extensive, idempotent poset endomorphism.

-- ClOp, the inhabitants of which denote closure operators.
record ClOp { ℓ₁ ℓ₂ : Level}(𝑨 : Poset  ℓ₁ ℓ₂) : Type  (  ℓ₂  ℓ₁) where

open Poset 𝑨
private
A = Carrier

open Algebra.Definitions (_≈_)

field
C : A  A
isExtensive       : Extensive _≤_ C
isOrderPreserving : C Preserves _≤_  _≤_
isIdempotent      : IdempotentFun C

Basic properties of closure operators

open ClOp
open Inverse

module _ {𝑨 : Poset  ℓ₁ ℓ₂}(𝑪 : ClOp 𝑨) where
open Poset 𝑨
open ≤-Reasoning 𝑨

private
c = C 𝑪
A = Carrier

Theorem 1. If 𝑨 = (A , ≦) is a poset and c is a closure operator on A, then ∀ (x y : A) → (x ≦ (c y) ↔ (c x) ≦ (c y))

clop→law⇒ : (x y : A)  x  (c y)  (c x)  (c y)
clop→law⇒ x y x≤cy = begin
c x     ≤⟨ isOrderPreserving 𝑪 x≤cy
c (c y) ≈⟨ isIdempotent 𝑪 y
c y

clop→law⇐ : (x y : A)  (c x)  (c y)  x  (c y)
clop→law⇐ x y cx≤cy = begin
x   ≤⟨ isExtensive 𝑪
c x ≤⟨ cx≤cy
c y

The converse of Theorem 1 also holds. That is,

Theorem 2. If 𝑨 = (A , ≤) is a poset and c : A → A satisfies ∀ (x y : A) → (x ≤ (c y) ↔ (c x) ≤ (c y))

then `c` is a closure operator on `A`.
module _ {𝑨 : Poset  ℓ₁ ℓ₂} where
open Poset 𝑨
private
A = Carrier

open Algebra.Definitions (_≈_)

clop←law : (c : A  A)  ((x y : A)  (x  (c y)  (c x)  (c y)))
Extensive _≤_ c × c Preserves _≤_  _≤_ × IdempotentFun c

clop←law c hyp  = e , (o , i)
where
h1 :  {x y}  x  (c y)  c x  c y
h1 {x}{y} = f (hyp x y)

h2 :  {x y}  c x  c y  x  (c y)
h2 {x}{y} = f⁻¹ (hyp x y)

e : Extensive _≤_ c
e = h2 refl

o : c Preserves _≤_  _≤_
o u = h1 (trans u e)

i : IdempotentFun c
i x = antisym (h1 refl) (h2 refl)