Skip to content

Overture.Adjunction.Galois

Galois Connections

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

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

module Overture.Adjunction.Galois where

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

-- Imports from the Agda Standard Library --------------------------------------
open import Data.Product             using ( _,_ ; _ร—_ ; swap ; projโ‚ )
open import Function.Base            using ( _โˆ˜_ ; id )
open import Level                    using ( _โŠ”_ ;  Level ; suc )
open import Relation.Binary.Bundles  using ( Poset )
open import Relation.Binary.Core     using ( REL )
open import Relation.Unary           using ( _โŠ†_ ; Pred   )

open import Relation.Binary.Structures using (IsEquivalence ; IsPartialOrder ; IsPreorder)

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)
  4. โˆ€ (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 _ (๐‘จ : Poset ฮฑ โ„“แตƒ ฯแตƒ)(๐‘ฉ : Poset ฮฒ โ„“แต‡ ฯแต‡) where
  open Poset ๐‘จ renaming ( Carrier to A ; _โ‰ค_ to _โ‰คแดฌ_ ) using ()
  open Poset ๐‘ฉ renaming ( Carrier to B ; _โ‰ค_ to _โ‰คแดฎ_ ) using ()
  record Galois : Type (suc (ฮฑ โŠ” ฮฒ โŠ” ฯแตƒ โŠ” ฯแต‡))  where
    field
      F : A โ†’ B
      G : B โ†’ A
      GFโ‰ฅid : โˆ€ a โ†’  a โ‰คแดฌ G (F a)
      FGโ‰ฅid : โˆ€ 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.)

module _ {ฮฑ ฯ : Level} {๐’œ : Type ฮฑ} where

  _โ‰_ : Pred ๐’œ ฯ โ†’ Pred ๐’œ ฯ โ†’ Type (ฮฑ โŠ” ฯ)
  P โ‰ Q = (P โŠ† Q) ร— (Q โŠ† P)

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

  โ‰-iseqv : IsEquivalence _โ‰_
  refl โ‰-iseqv = id , id
  sym โ‰-iseqv = swap
  trans โ‰-iseqv (uโ‚ , uโ‚‚) (vโ‚ , vโ‚‚) = vโ‚ โˆ˜ uโ‚ , uโ‚‚ โˆ˜ vโ‚‚

module _ {ฮฑ : Level} (ฯ : Level) (๐’œ : Type ฮฑ) where
   open Poset           using (Carrier ; _โ‰ˆ_ ; _โ‰ค_ ; isPartialOrder)
   open IsPartialOrder  using (isPreorder ; antisym)
   open IsPreorder      using (isEquivalence ; reflexive ; trans)

   PosetOfSubsets : Poset (ฮฑ โŠ” suc ฯ) (ฮฑ โŠ” ฯ) (ฮฑ โŠ” ฯ)
   PosetOfSubsets .Carrier = Pred ๐’œ ฯ
   PosetOfSubsets ._โ‰ˆ_ = _โ‰_
   PosetOfSubsets ._โ‰ค_ = _โŠ†_
   PosetOfSubsets .isPartialOrder .isPreorder .isEquivalence  = โ‰-iseqv
   PosetOfSubsets .isPartialOrder .isPreorder .reflexive      = projโ‚
   PosetOfSubsets .isPartialOrder .isPreorder .trans          = ฮป u v โ†’ v โˆ˜ u
   PosetOfSubsets .isPartialOrder .antisym                    = _,_

A binary relation from one poset to another induces a Galois connection. 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 (suc โ„“) โ„“ โ„“
  ๐’ซ๐’œ = 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 }