Skip to content

Legacy.Base.Adjunction.Closure

Closure Systems and Operators

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

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

module Legacy.Base.Adjunction.Closure where

-- Imports from Agda and the Agda Standard Library  ---------------------------------------
open import Agda.Primitive           using () renaming ( Set to Type )
import Algebra.Definitions
open import Data.Product             using ( Ξ£-syntax ; _,_ ; _Γ—_ )
open import Function                 using ( _βˆ˜β‚‚_ )
open import Function.Bundles         using ( _↔_ ; Inverse)
open import Level                    using ( _βŠ”_ ; Level )
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, where _β‰ˆ_ is the equivalence carried by the poset

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
  e : Extensive _≀_ c
  e = (from βˆ˜β‚‚ hyp) _ _ refl

  o : c Preserves _≀_ ⟢ _≀_
  o u = (to βˆ˜β‚‚ hyp) _ _ (trans u e)

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

{-# WARNING_ON_USAGE Extensive       "Use Overture.Adjunction.Closure.Extensive instead. Deprecated under #305; removal planned one minor cycle later." #-}
{-# WARNING_ON_USAGE IntersectClosed "Use Overture.Adjunction.Closure.IntersectClosed instead. Deprecated under #305; removal planned one minor cycle later." #-}
{-# WARNING_ON_USAGE ClosureSystem   "Use Overture.Adjunction.Closure.ClosureSystem instead. Deprecated under #305; removal planned one minor cycle later." #-}
{-# WARNING_ON_USAGE ClOp            "Use Overture.Adjunction.Closure.ClOp instead. Deprecated under #305; removal planned one minor cycle later." #-}
{-# WARNING_ON_USAGE clop→law⇒       "Use Overture.Adjunction.Closure.clop→law⇒ instead. Deprecated under #305; removal planned one minor cycle later." #-}
{-# WARNING_ON_USAGE clopβ†’law⇐       "Use Overture.Adjunction.Closure.clopβ†’law⇐ instead. Deprecated under #305; removal planned one minor cycle later." #-}
{-# WARNING_ON_USAGE clop←law        "Use Overture.Adjunction.Closure.clop←law instead. Deprecated under #305; removal planned one minor cycle later." #-}