# Galois connections

Content created by Egbert Rijke and Fredrik Bakke.

Created on 2023-04-08.

module order-theory.galois-connections where

Imports
open import foundation.action-on-identifications-functions
open import foundation.dependent-pair-types
open import foundation.equivalences
open import foundation.identity-types
open import foundation.logical-equivalences
open import foundation.propositions
open import foundation.subtype-identity-principle
open import foundation.subtypes
open import foundation.universe-levels

open import order-theory.order-preserving-maps-posets
open import order-theory.posets


## Idea

A Galois connection between posets P and Q is a pair of order preserving maps f : P → Q and g : Q → P such that the logical equivalence

  (f x ≤ y) ↔ (x ≤ g y)


holds for any x : P and y : Q.

## Definitions

module _
{l1 l2 l3 l4 : Level} (P : Poset l1 l2) (Q : Poset l3 l4)
where

hom-Poset P Q → hom-Poset Q P → Prop (l1 ⊔ l2 ⊔ l3 ⊔ l4)
Π-Prop
( type-Poset P)
( λ x →
Π-Prop
( type-Poset Q)
( λ y →
iff-Prop
( leq-Poset-Prop Q (map-hom-Poset P Q f x) y)
( leq-Poset-Prop P x (map-hom-Poset Q P g y))))

hom-Poset P Q → UU (l1 ⊔ l2 ⊔ l3 ⊔ l4)

hom-Poset Q P → UU (l1 ⊔ l2 ⊔ l3 ⊔ l4)
type-subtype (λ f → adjoint-relation-galois-connection-Prop f g)

Galois-Connection : UU (l1 ⊔ l2 ⊔ l3 ⊔ l4)
Galois-Connection =
Σ ( hom-Poset Q P) is-upper-adjoint-Galois-Connection

module _
(G : Galois-Connection)
where

type-Poset Q → type-Poset P

type-Poset P → type-Poset Q

(x : type-Poset P) (y : type-Poset Q) →
leq-Poset Q (map-lower-adjoint-Galois-Connection x) y ↔

(x : type-Poset P) (y : type-Poset Q) →
leq-Poset Q (map-lower-adjoint-Galois-Connection x) y →

(x : type-Poset P) (y : type-Poset Q) →
leq-Poset P x (map-upper-adjoint-Galois-Connection y) →



## Properties

### Being a lower adjoint of a Galois connection is a property

module _
{l1 l2 l3 l4 : Level} (P : Poset l1 l2) (Q : Poset l3 l4)
(f : hom-Poset P Q)
where

(g h : is-lower-adjoint-Galois-Connection P Q f) → UU (l1 ⊔ l3)
htpy-is-lower-adjoint-Galois-Connection (g , G) (h , H) =
htpy-hom-Poset Q P g h

(g : is-lower-adjoint-Galois-Connection P Q f) →
refl-htpy-hom-Poset Q P g

(g h : is-lower-adjoint-Galois-Connection P Q f) →
(g ＝ h) ≃ htpy-is-lower-adjoint-Galois-Connection g h
extensionality-type-subtype
( G)
( extensionality-hom-Poset Q P g)

(g h : is-lower-adjoint-Galois-Connection P Q f) →
htpy-is-lower-adjoint-Galois-Connection g h → g ＝ h

(g h : is-lower-adjoint-Galois-Connection P Q f) → g ＝ h
all-elements-equal-is-lower-adjoint-Galois-Connection (g , G) (h , H) =
( g , G)
( h , H)
( λ y →
antisymmetric-leq-Poset P
( map-hom-Poset Q P g y)
( map-hom-Poset Q P h y)
( forward-implication
( H (map-hom-Poset Q P g y) y)
( backward-implication
( G (map-hom-Poset Q P g y) y)
( refl-leq-Poset P (map-hom-Poset Q P g y))))
( forward-implication
( G (map-hom-Poset Q P h y) y)
( backward-implication
( H (map-hom-Poset Q P h y) y)
( refl-leq-Poset P (map-hom-Poset Q P h y)))))

is-prop-all-elements-equal

is-lower-adjoint-galois-connection-Prop : Prop (l1 ⊔ l2 ⊔ l3 ⊔ l4)


### Being a upper adjoint of a Galois connection is a property

module _
{l1 l2 l3 l4 : Level} (P : Poset l1 l2) (Q : Poset l3 l4)
(g : hom-Poset Q P)
where

(f h : is-upper-adjoint-Galois-Connection P Q g) → UU (l1 ⊔ l3)
htpy-is-upper-adjoint-Galois-Connection (f , F) (h , H) =
htpy-hom-Poset P Q f h

(f : is-upper-adjoint-Galois-Connection P Q g) →
refl-htpy-hom-Poset P Q f

(f h : is-upper-adjoint-Galois-Connection P Q g) →
(f ＝ h) ≃ htpy-is-upper-adjoint-Galois-Connection f h
extensionality-type-subtype
( λ u → adjoint-relation-galois-connection-Prop P Q u g)
( F)
( extensionality-hom-Poset P Q f)

(f h : is-upper-adjoint-Galois-Connection P Q g) →
htpy-is-upper-adjoint-Galois-Connection f h → f ＝ h

(f h : is-upper-adjoint-Galois-Connection P Q g) → f ＝ h
all-elements-equal-is-upper-adjoint-Galois-Connection (f , F) (h , H) =
( f , F)
( h , H)
( λ x →
antisymmetric-leq-Poset Q
( map-hom-Poset P Q f x)
( map-hom-Poset P Q h x)
( backward-implication
( F x (map-hom-Poset P Q h x))
( forward-implication
( H x (map-hom-Poset P Q h x))
( refl-leq-Poset Q (map-hom-Poset P Q h x))))
( backward-implication
( H x (map-hom-Poset P Q f x))
( forward-implication
( F x (map-hom-Poset P Q f x))
( refl-leq-Poset Q (map-hom-Poset P Q f x)))))

is-prop-all-elements-equal

is-upper-adjoint-galois-connection-Prop : Prop (l1 ⊔ l2 ⊔ l3 ⊔ l4)


### Characterizing equalities of Galois connections

#### Characterizing equalities of Galois connections as homotopies of their upper adjoints

module _
{l1 l2 l3 l4 : Level} (P : Poset l1 l2) (Q : Poset l3 l4)
where

(G H : Galois-Connection P Q) → UU (l1 ⊔ l3)
htpy-hom-Poset Q P

(G H : Galois-Connection P Q) →
is-prop-htpy-hom-Poset Q P

(G H : Galois-Connection P Q) →
(G ＝ H) ≃ htpy-upper-adjoint-Galois-Connection G H
extensionality-type-subtype
( G)
( refl-htpy-hom-Poset Q P g)
( extensionality-hom-Poset Q P g)

(G H : Galois-Connection P Q) →
htpy-upper-adjoint-Galois-Connection G H → G ＝ H


#### Characterizing equalities of Galois connection by homotopies of their lower adjoints

module _
{l1 l2 l3 l4 : Level} (P : Poset l1 l2) (Q : Poset l3 l4)
where

(G H : Galois-Connection P Q) → UU (l1 ⊔ l3)
htpy-hom-Poset P Q

(G H : Galois-Connection P Q) →
is-prop-htpy-hom-Poset P Q

(G H : Galois-Connection P Q) →
antisymmetric-leq-Poset P
( map-upper-adjoint-Galois-Connection P Q G y)
( map-upper-adjoint-Galois-Connection P Q H y)
( map-upper-adjoint-Galois-Connection P Q G y)
( y)
( concatenate-eq-leq-Poset Q
( inv (K (map-upper-adjoint-Galois-Connection P Q G y)))
( map-upper-adjoint-Galois-Connection P Q G y)
( y)
( refl-leq-Poset P (map-upper-adjoint-Galois-Connection P Q G y)))))
( map-upper-adjoint-Galois-Connection P Q H y)
( y)
( concatenate-eq-leq-Poset Q
( K (map-upper-adjoint-Galois-Connection P Q H y))
( map-upper-adjoint-Galois-Connection P Q H y)
( y)
( refl-leq-Poset P (map-upper-adjoint-Galois-Connection P Q H y)))))

(G H : Galois-Connection P Q) →
htpy-upper-adjoint-Galois-Connection P Q G H →
antisymmetric-leq-Poset Q
( map-lower-adjoint-Galois-Connection P Q G x)
( map-lower-adjoint-Galois-Connection P Q H x)
( map-inv-adjoint-relation-Galois-Connection P Q G x
( map-lower-adjoint-Galois-Connection P Q H x)
( concatenate-leq-eq-Poset P
( map-adjoint-relation-Galois-Connection P Q H x
( map-lower-adjoint-Galois-Connection P Q H x)
( refl-leq-Poset Q (map-lower-adjoint-Galois-Connection P Q H x)))
( inv (K (map-lower-adjoint-Galois-Connection P Q H x)))))
( map-inv-adjoint-relation-Galois-Connection P Q H x
( map-lower-adjoint-Galois-Connection P Q G x)
( concatenate-leq-eq-Poset P
( map-adjoint-relation-Galois-Connection P Q G x
( map-lower-adjoint-Galois-Connection P Q G x)
( refl-leq-Poset Q (map-lower-adjoint-Galois-Connection P Q G x)))
( K (map-lower-adjoint-Galois-Connection P Q G x))))

(G H : Galois-Connection P Q) →
is-equiv-has-converse-is-prop
( is-prop-htpy-upper-adjoint-Galois-Connection P Q G H)

(G H : Galois-Connection P Q) →
is-equiv-has-converse-is-prop
( is-prop-htpy-upper-adjoint-Galois-Connection P Q G H)

(G H : Galois-Connection P Q) →
htpy-upper-adjoint-Galois-Connection P Q G H ≃

(G H : Galois-Connection P Q) →
(G ＝ H) ≃ htpy-lower-adjoint-Galois-Connection G H


### G y = GFG y for any Galois connection (G , F)

module _
{l1 l2 l3 l4 : Level} (P : Poset l1 l2) (Q : Poset l3 l4)
(G : Galois-Connection P Q)
where

(y : type-Poset Q) →
map-upper-adjoint-Galois-Connection P Q G y ＝
( map-upper-adjoint-Galois-Connection P Q G y))
antisymmetric-leq-Poset P
( map-upper-adjoint-Galois-Connection P Q G y)
( map-upper-adjoint-Galois-Connection P Q G y)))
( map-upper-adjoint-Galois-Connection P Q G y)
( map-upper-adjoint-Galois-Connection P Q G y))
( refl-leq-Poset Q _))
( map-upper-adjoint-Galois-Connection P Q G y))
( y)
( map-upper-adjoint-Galois-Connection P Q G y)
( y)
( refl-leq-Poset P _)))


### F x = FGF x for any Galois connection (G , F)

module _
{l1 l2 l3 l4 : Level} (P : Poset l1 l2) (Q : Poset l3 l4)
(G : Galois-Connection P Q)
where

(x : type-Poset P) →
map-lower-adjoint-Galois-Connection P Q G x ＝
( map-lower-adjoint-Galois-Connection P Q G x))
antisymmetric-leq-Poset Q
( map-lower-adjoint-Galois-Connection P Q G x)
( map-lower-adjoint-Galois-Connection P Q G x)))
( preserves-order-lower-adjoint-Galois-Connection P Q G x
( map-lower-adjoint-Galois-Connection P Q G x))
( map-adjoint-relation-Galois-Connection P Q G x
( map-lower-adjoint-Galois-Connection P Q G x)
( refl-leq-Poset Q _)))
( map-lower-adjoint-Galois-Connection P Q G x))
( map-lower-adjoint-Galois-Connection P Q G x)
( refl-leq-Poset P _))


### The composite FG is idempotent for every Galois connection (G , F)

module _
{l1 l2 l3 l4 : Level} (P : Poset l1 l2) (Q : Poset l3 l4)
(G : Galois-Connection P Q)
where

htpy-idempotent-lower-upper-Galois-Connection :
htpy-hom-Poset Q Q
( comp-hom-Poset Q Q Q
( comp-hom-Poset Q P Q
( comp-hom-Poset Q P Q
( comp-hom-Poset Q P Q
htpy-idempotent-lower-upper-Galois-Connection x =
ap
( inv
( compute-upper-lower-upper-adjoint-Galois-Connection P Q G x))


### The composite GF is idempotent for every Galois connection (G , F)

module _
{l1 l2 l3 l4 : Level} (P : Poset l1 l2) (Q : Poset l3 l4)
(G : Galois-Connection P Q)
where

htpy-idempotent-upper-lower-Galois-Connection :
htpy-hom-Poset P P
( comp-hom-Poset P P P
( comp-hom-Poset P Q P
( comp-hom-Poset P Q P
( comp-hom-Poset P Q P