Skip to content

Overture.Adjunction.Closure

Closure Systems and Operators

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

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

module Overture.Adjunction.Closure where

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

-- Imports from the Agda Standard Library  ---------------------------------------
import Algebra.Definitions
open import Data.Product             using ( Ξ£-syntax ; _,_ ; _Γ—_ )
open import Function                 using ( _βˆ˜β‚‚_ )
open import Function.Bundles         using ( _↔_ ; Inverse)
open import Level                    using ( _βŠ”_ ; Level ) renaming ( suc to lsuc )
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 Theorem 2.5 in J.B. Nation's Lattice Theory Notes.)

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 (Ο‡ βŠ” ρ βŠ” lsuc β„“)
  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. A 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 𝑨 using (Carrier; _β‰ˆ_; _≀_)
  open Algebra.Definitions (_β‰ˆ_)
  field
    C                  : Carrier β†’ Carrier
    isExtensive        : Extensive _≀_ C
    isOrderPreserving  : C Preserves _≀_ ⟢ _≀_
    isIdempotent       : IdempotentFun C

Basic properties of closure operators

module _ {𝑨 : Poset β„“ ℓ₁ β„“β‚‚} where
  open Poset 𝑨 renaming (Carrier to A) using (_β‰ˆ_; _≀_; refl; trans; antisym)
  open Algebra.Definitions (_β‰ˆ_) using (IdempotentFun)
  open Inverse using (from; to)

  module _ {π‘ͺ : ClOp 𝑨} where
    open ClOp π‘ͺ
    open ≀-Reasoning 𝑨

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  β†’  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  β†’  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.

  clop←law :  (c : A β†’ A) β†’ (βˆ€ x y β†’ x ≀ c y ↔ c x ≀ c y)
    β†’ Extensive _≀_ c  Γ— c Preserves _≀_ ⟢ _≀_  Γ— IdempotentFun c

  clop←law c hyp  = e , (o , i)
    where
    -- c is extensive: x ≀ c x
    e : Extensive _≀_ c
    e = (from βˆ˜β‚‚ hyp) _ _ refl

    -- c is order preserving:  x ≀ y β†’ c x ≀ c y
    o : c Preserves _≀_ ⟢ _≀_
    o u = (to βˆ˜β‚‚ hyp) _ _ (trans u e)

    -- c is idempotent:  c (c x) = c x
    i : IdempotentFun c
    i x = antisym ((to βˆ˜β‚‚ hyp) _ _ refl) ((from βˆ˜β‚‚ hyp) _ _ refl)