 Galois Connections

This is the Adjunction.Galois 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 ( _⊔_ ;  Level ; lsuc) renaming ( Set to Type )
open import Data.Product            using ( _,_ ; _×_ ; swap ) renaming ( proj₁ to fst )
open import Function.Base           using ( _∘_ ; id )
open import Relation.Binary.Bundles using ( Poset )
open import Relation.Binary.Core    using ( REL ; Rel ; _⇒_ ; _Preserves_⟶_ )
open import Relation.Unary          using ( _⊆_ ;  _∈_ ; Pred   )
import Relation.Binary.Structures as BS

private variable
α β ℓᵃ ρᵃ ℓᵇ ρᵇ : Level

If 𝑨 = (A, ≤) and 𝑩 = (B, ≤) are two partially ordered sets (posets), then a Galois connection between 𝑨 and 𝑩 is a pair (F , G) of functions such that

1. F : A → B
2. G : B → A
3. ∀ (a : A)(b : B) → F(a) ≤ b → a ≤ G(b) r. ∀ (a : A)(b : B) → a ≤ G(b) → F(a) ≤ b

In other terms, F is a left adjoint of G and G is a right adjoint of F.

module _ (A : Poset α ℓᵃ ρᵃ)
(B : Poset β ℓᵇ ρᵇ)
where
open Poset
private
_≤A_ = _≤_ A
_≤B_ = _≤_ B

record Galois : Type (lsuc (α  β  ρᵃ  ρᵇ))  where
field
F : Carrier A  Carrier B
G : Carrier B  Carrier A
GF≥id :  a   a ≤A G (F a)
FG≥id :  b   b ≤B F (G b)

module _ {𝒜 : Type α}{ : Type β} where

-- For A ⊆ 𝒜, define A ⃗ R = {b : b ∈ ℬ,  ∀ a ∈ A → R a b }
_⃗_ :  {ρᵃ ρᵇ}  Pred 𝒜 ρᵃ  REL 𝒜  ρᵇ  Pred  (α  ρᵃ  ρᵇ)
A  R = λ b  A   a  R a b)

-- For B ⊆ ℬ, define R ⃖ B = {a : a ∈ 𝒜,  ∀ b ∈ B → R a b }
_⃖_ :  {ρᵃ ρᵇ}  REL 𝒜  ρᵃ  Pred  ρᵇ  Pred 𝒜 (β  ρᵃ  ρᵇ)
R  B = λ a  B  R a

←→≥id :  {ρᵃ ρʳ} {A : Pred 𝒜 ρᵃ} {R : REL 𝒜  ρʳ}  A  R  (A  R)
←→≥id p b = b p

→←≥id :  {ρᵇ ρʳ} {B : Pred  ρᵇ} {R : REL 𝒜  ρʳ}   B  (R  B)  R
→←≥id p a = a p

→←→⊆→ :  {ρᵃ ρʳ} {A : Pred 𝒜 ρᵃ}{R : REL 𝒜  ρʳ}  (R  (A  R))  R  A  R
→←→⊆→ p a = p  z  z a)

←→←⊆← :  {ρᵇ ρʳ} {B : Pred  ρᵇ}{R : REL 𝒜  ρʳ}   R  ((R  B)  R)  R  B
←→←⊆← p b = p  z  z b)

-- Definition of "closed" with respect to the closure operator λ A → R ⃖ (A ⃗ R)
←→Closed :  {ρᵃ ρʳ} {A : Pred 𝒜 ρᵃ} {R : REL 𝒜  ρʳ}  Type _
←→Closed {A = A}{R} = R  (A  R)  A

-- Definition of "closed" with respect to the closure operator λ B → (R ⃖ B) ⃗ R
→←Closed :  {ρᵇ ρʳ} {B : Pred  ρᵇ}{R : REL 𝒜  ρʳ}  Type _
→←Closed {B = B}{R} = (R  B)  R  B

The poset of subsets of a set

Here we define a type that represents the poset of subsets of a given set equipped with the usual set inclusion relation. (It seems there is no definition in the standard library of this important example of a poset; we should propose adding it.)

open Poset

module _ {α ρ : Level} {𝒜 : Type α} where

_≐_ : Pred 𝒜 ρ  Pred 𝒜 ρ  Type (α  ρ)
P  Q = (P  Q) × (Q  P)

open BS.IsEquivalence renaming (refl to ref ; sym to symm ; trans to tran)

≐-iseqv : BS.IsEquivalence _≐_
ref ≐-iseqv = id , id
symm ≐-iseqv = swap
tran ≐-iseqv (u₁ , u₂) (v₁ , v₂) = v₁  u₁ , u₂  v₂

module _ {α : Level} (ρ : Level) (𝒜 : Type α) where

PosetOfSubsets : Poset (α  lsuc ρ) (α  ρ) (α  ρ)
Carrier PosetOfSubsets = Pred 𝒜 ρ
_≈_ PosetOfSubsets = _≐_
_≤_ PosetOfSubsets = _⊆_
isPartialOrder PosetOfSubsets =
record { isPreorder = record { isEquivalence = ≐-iseqv
; reflexive = fst
; trans = λ u v  v  u
}
; antisym = _,_
}

A Binary relation from one poset to another induces a Galois connection, but only in a very special situation, namely when all the involved sets are of the same size. This is akin to the situation with Adjunctions in Category Theory (unsurprisingly). In other words, there is likely a unit/counit definition that is more level polymorphic.

module _ { : Level}{𝒜 : Type } { : Type } where

𝒫𝒜 : Poset (lsuc )
𝒫ℬ : Poset (lsuc )
𝒫𝒜 = PosetOfSubsets  𝒜
𝒫ℬ = PosetOfSubsets

-- Every binary relation from one poset to another induces a Galois connection.
Rel→Gal : (R : REL 𝒜  )  Galois 𝒫𝒜 𝒫ℬ
Rel→Gal R = record { F = _⃗ R
; G = R ⃖_
; GF≥id = λ _  ←→≥id
; FG≥id = λ _  →←≥id }