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

{-# OPTIONS --without-K --exact-split --safe #-} module Adjunction.Closure where -- 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 α

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

Let `𝑷 = (P, ≤)`

be a poset. An function `C : P → P`

is called a *closure operator*
on `𝑷`

if it is

- (extensive)
`∀ x → x ≤ C x`

- (order preserving)
`∀ x y → x ≤ y → C x ≤ C y`

- (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

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)