Galois connections

Content created by Egbert Rijke and Fredrik Bakke.

Created on 2023-04-08.
Last modified on 2024-04-11.

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

  adjoint-relation-galois-connection-Prop :
    hom-Poset P Q  hom-Poset Q P  Prop (l1  l2  l3  l4)
  adjoint-relation-galois-connection-Prop f g =
    Π-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))))

  is-lower-adjoint-Galois-Connection :
    hom-Poset P Q  UU (l1  l2  l3  l4)
  is-lower-adjoint-Galois-Connection f =
    type-subtype (adjoint-relation-galois-connection-Prop f)

  is-upper-adjoint-Galois-Connection :
    hom-Poset Q P  UU (l1  l2  l3  l4)
  is-upper-adjoint-Galois-Connection g =
    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

    upper-adjoint-Galois-Connection : hom-Poset Q P
    upper-adjoint-Galois-Connection = pr1 G

    map-upper-adjoint-Galois-Connection :
      type-Poset Q  type-Poset P
    map-upper-adjoint-Galois-Connection =
      map-hom-Poset Q P upper-adjoint-Galois-Connection

    preserves-order-upper-adjoint-Galois-Connection :
      preserves-order-Poset Q P map-upper-adjoint-Galois-Connection
    preserves-order-upper-adjoint-Galois-Connection =
      preserves-order-map-hom-Poset Q P upper-adjoint-Galois-Connection

    is-upper-adjoint-upper-adjoint-Galois-Connection :
      is-upper-adjoint-Galois-Connection upper-adjoint-Galois-Connection
    is-upper-adjoint-upper-adjoint-Galois-Connection = pr2 G

    lower-adjoint-Galois-Connection : hom-Poset P Q
    lower-adjoint-Galois-Connection =
      pr1 is-upper-adjoint-upper-adjoint-Galois-Connection

    map-lower-adjoint-Galois-Connection :
      type-Poset P  type-Poset Q
    map-lower-adjoint-Galois-Connection =
      map-hom-Poset P Q lower-adjoint-Galois-Connection

    preserves-order-lower-adjoint-Galois-Connection :
      preserves-order-Poset P Q map-lower-adjoint-Galois-Connection
    preserves-order-lower-adjoint-Galois-Connection =
      preserves-order-map-hom-Poset P Q lower-adjoint-Galois-Connection

    adjoint-relation-Galois-Connection :
      (x : type-Poset P) (y : type-Poset Q) 
      leq-Poset Q (map-lower-adjoint-Galois-Connection x) y 
      leq-Poset P x (map-upper-adjoint-Galois-Connection y)
    adjoint-relation-Galois-Connection =
      pr2 is-upper-adjoint-upper-adjoint-Galois-Connection

    map-adjoint-relation-Galois-Connection :
      (x : type-Poset P) (y : type-Poset Q) 
      leq-Poset Q (map-lower-adjoint-Galois-Connection x) y 
      leq-Poset P x (map-upper-adjoint-Galois-Connection y)
    map-adjoint-relation-Galois-Connection x y =
      forward-implication (adjoint-relation-Galois-Connection x y)

    map-inv-adjoint-relation-Galois-Connection :
      (x : type-Poset P) (y : type-Poset Q) 
      leq-Poset P x (map-upper-adjoint-Galois-Connection y) 
      leq-Poset Q (map-lower-adjoint-Galois-Connection x) y
    map-inv-adjoint-relation-Galois-Connection x y =
      backward-implication (adjoint-relation-Galois-Connection x y)

    is-lower-adjoint-lower-adjoint-Galois-Connection :
      is-lower-adjoint-Galois-Connection lower-adjoint-Galois-Connection
    pr1 is-lower-adjoint-lower-adjoint-Galois-Connection =
      upper-adjoint-Galois-Connection
    pr2 is-lower-adjoint-lower-adjoint-Galois-Connection =
      adjoint-relation-Galois-Connection

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

  htpy-is-lower-adjoint-Galois-Connection :
    (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

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

  extensionality-is-lower-adjoint-Galois-Connection :
    (g h : is-lower-adjoint-Galois-Connection P Q f) 
    (g  h)  htpy-is-lower-adjoint-Galois-Connection g h
  extensionality-is-lower-adjoint-Galois-Connection (g , G) =
    extensionality-type-subtype
      ( adjoint-relation-galois-connection-Prop P Q f)
      ( G)
      ( refl-htpy-is-lower-adjoint-Galois-Connection (g , G))
      ( extensionality-hom-Poset Q P g)

  eq-htpy-is-lower-adjoint-Galois-Connection :
    (g h : is-lower-adjoint-Galois-Connection P Q f) 
    htpy-is-lower-adjoint-Galois-Connection g h  g  h
  eq-htpy-is-lower-adjoint-Galois-Connection g h =
    map-inv-equiv (extensionality-is-lower-adjoint-Galois-Connection g h)

  all-elements-equal-is-lower-adjoint-Galois-Connection :
    (g h : is-lower-adjoint-Galois-Connection P Q f)  g  h
  all-elements-equal-is-lower-adjoint-Galois-Connection (g , G) (h , H) =
    eq-htpy-is-lower-adjoint-Galois-Connection
      ( 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-is-lower-adjoint-Galois-Connection :
    is-prop (is-lower-adjoint-Galois-Connection P Q f)
  is-prop-is-lower-adjoint-Galois-Connection =
    is-prop-all-elements-equal
      all-elements-equal-is-lower-adjoint-Galois-Connection

  is-lower-adjoint-galois-connection-Prop : Prop (l1  l2  l3  l4)
  pr1 is-lower-adjoint-galois-connection-Prop =
    is-lower-adjoint-Galois-Connection P Q f
  pr2 is-lower-adjoint-galois-connection-Prop =
    is-prop-is-lower-adjoint-Galois-Connection

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

  htpy-is-upper-adjoint-Galois-Connection :
    (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

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

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

  eq-htpy-is-upper-adjoint-Galois-Connection :
    (f h : is-upper-adjoint-Galois-Connection P Q g) 
    htpy-is-upper-adjoint-Galois-Connection f h  f  h
  eq-htpy-is-upper-adjoint-Galois-Connection f h =
    map-inv-equiv (extensionality-is-upper-adjoint-Galois-Connection f h)

  all-elements-equal-is-upper-adjoint-Galois-Connection :
    (f h : is-upper-adjoint-Galois-Connection P Q g)  f  h
  all-elements-equal-is-upper-adjoint-Galois-Connection (f , F) (h , H) =
    eq-htpy-is-upper-adjoint-Galois-Connection
      ( 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-is-upper-adjoint-Galois-Connection :
    is-prop (is-upper-adjoint-Galois-Connection P Q g)
  is-prop-is-upper-adjoint-Galois-Connection =
    is-prop-all-elements-equal
      all-elements-equal-is-upper-adjoint-Galois-Connection

  is-upper-adjoint-galois-connection-Prop : Prop (l1  l2  l3  l4)
  pr1 is-upper-adjoint-galois-connection-Prop =
    is-upper-adjoint-Galois-Connection P Q g
  pr2 is-upper-adjoint-galois-connection-Prop =
    is-prop-is-upper-adjoint-Galois-Connection

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

  htpy-upper-adjoint-Galois-Connection :
    (G H : Galois-Connection P Q)  UU (l1  l3)
  htpy-upper-adjoint-Galois-Connection G H =
    htpy-hom-Poset Q P
      ( upper-adjoint-Galois-Connection P Q G)
      ( upper-adjoint-Galois-Connection P Q H)

  is-prop-htpy-upper-adjoint-Galois-Connection :
    (G H : Galois-Connection P Q) 
    is-prop (htpy-upper-adjoint-Galois-Connection G H)
  is-prop-htpy-upper-adjoint-Galois-Connection G H =
    is-prop-htpy-hom-Poset Q P
      ( upper-adjoint-Galois-Connection P Q G)
      ( upper-adjoint-Galois-Connection P Q H)

  extensionality-upper-adjoint-Galois-Connection :
    (G H : Galois-Connection P Q) 
    (G  H)  htpy-upper-adjoint-Galois-Connection G H
  extensionality-upper-adjoint-Galois-Connection (g , G) =
    extensionality-type-subtype
      ( is-upper-adjoint-galois-connection-Prop P Q)
      ( G)
      ( refl-htpy-hom-Poset Q P g)
      ( extensionality-hom-Poset Q P g)

  eq-htpy-upper-adjoint-Galois-Connection :
    (G H : Galois-Connection P Q) 
    htpy-upper-adjoint-Galois-Connection G H  G  H
  eq-htpy-upper-adjoint-Galois-Connection G H =
    map-inv-equiv (extensionality-upper-adjoint-Galois-Connection 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

  htpy-lower-adjoint-Galois-Connection :
    (G H : Galois-Connection P Q)  UU (l1  l3)
  htpy-lower-adjoint-Galois-Connection G H =
    htpy-hom-Poset P Q
      ( lower-adjoint-Galois-Connection P Q G)
      ( lower-adjoint-Galois-Connection P Q H)

  is-prop-htpy-lower-adjoint-Galois-Connection :
    (G H : Galois-Connection P Q) 
    is-prop (htpy-lower-adjoint-Galois-Connection G H)
  is-prop-htpy-lower-adjoint-Galois-Connection G H =
    is-prop-htpy-hom-Poset P Q
      ( lower-adjoint-Galois-Connection P Q G)
      ( lower-adjoint-Galois-Connection P Q H)

  htpy-upper-adjoint-htpy-lower-adjoint-Galois-Connection :
    (G H : Galois-Connection P Q) 
    htpy-lower-adjoint-Galois-Connection G H 
    htpy-upper-adjoint-Galois-Connection P Q G H
  htpy-upper-adjoint-htpy-lower-adjoint-Galois-Connection G H K y =
    antisymmetric-leq-Poset P
      ( map-upper-adjoint-Galois-Connection P Q G y)
      ( map-upper-adjoint-Galois-Connection P Q H y)
      ( map-adjoint-relation-Galois-Connection P Q H
        ( 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-inv-adjoint-relation-Galois-Connection P Q G
            ( map-upper-adjoint-Galois-Connection P Q G y)
            ( y)
            ( refl-leq-Poset P (map-upper-adjoint-Galois-Connection P Q G y)))))
      ( map-adjoint-relation-Galois-Connection P Q G
        ( 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-inv-adjoint-relation-Galois-Connection P Q H
            ( map-upper-adjoint-Galois-Connection P Q H y)
            ( y)
            ( refl-leq-Poset P (map-upper-adjoint-Galois-Connection P Q H y)))))

  htpy-lower-adjoint-htpy-upper-adjoint-Galois-Connection :
    (G H : Galois-Connection P Q) 
    htpy-upper-adjoint-Galois-Connection P Q G H 
    htpy-lower-adjoint-Galois-Connection G H
  htpy-lower-adjoint-htpy-upper-adjoint-Galois-Connection G H K x =
    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))))

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

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

  equiv-htpy-lower-adjoint-htpy-upper-adjoint-Galois-Connection :
    (G H : Galois-Connection P Q) 
    htpy-upper-adjoint-Galois-Connection P Q G H 
    htpy-lower-adjoint-Galois-Connection G H
  pr1 (equiv-htpy-lower-adjoint-htpy-upper-adjoint-Galois-Connection G H) =
    htpy-lower-adjoint-htpy-upper-adjoint-Galois-Connection G H
  pr2 (equiv-htpy-lower-adjoint-htpy-upper-adjoint-Galois-Connection G H) =
    is-equiv-htpy-lower-adjoint-htpy-upper-adjoint-Galois-Connection G H

  extensionality-lower-adjoint-Galois-Connection :
    (G H : Galois-Connection P Q) 
    (G  H)  htpy-lower-adjoint-Galois-Connection G H
  extensionality-lower-adjoint-Galois-Connection G H =
    equiv-htpy-lower-adjoint-htpy-upper-adjoint-Galois-Connection G H ∘e
    extensionality-upper-adjoint-Galois-Connection P Q 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

  compute-upper-lower-upper-adjoint-Galois-Connection :
    (y : type-Poset Q) 
    map-upper-adjoint-Galois-Connection P Q G y 
    map-upper-adjoint-Galois-Connection P Q G
      ( map-lower-adjoint-Galois-Connection P Q G
        ( map-upper-adjoint-Galois-Connection P Q G y))
  compute-upper-lower-upper-adjoint-Galois-Connection y =
    antisymmetric-leq-Poset P
      ( map-upper-adjoint-Galois-Connection P Q G y)
      ( map-upper-adjoint-Galois-Connection P Q G
        ( map-lower-adjoint-Galois-Connection P Q G
          ( map-upper-adjoint-Galois-Connection P Q G y)))
      ( map-adjoint-relation-Galois-Connection P Q G
        ( map-upper-adjoint-Galois-Connection P Q G y)
        ( map-lower-adjoint-Galois-Connection P Q G
          ( map-upper-adjoint-Galois-Connection P Q G y))
        ( refl-leq-Poset Q _))
      ( preserves-order-upper-adjoint-Galois-Connection P Q G
        ( map-lower-adjoint-Galois-Connection P Q G
          ( map-upper-adjoint-Galois-Connection P Q G y))
        ( y)
        ( map-inv-adjoint-relation-Galois-Connection P Q G
          ( 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

  compute-lower-upper-lower-adjoint-Galois-Connection :
    (x : type-Poset P) 
    map-lower-adjoint-Galois-Connection P Q G x 
    map-lower-adjoint-Galois-Connection P Q G
      ( map-upper-adjoint-Galois-Connection P Q G
        ( map-lower-adjoint-Galois-Connection P Q G x))
  compute-lower-upper-lower-adjoint-Galois-Connection x =
    antisymmetric-leq-Poset Q
      ( map-lower-adjoint-Galois-Connection P Q G x)
      ( map-lower-adjoint-Galois-Connection P Q G
        ( map-upper-adjoint-Galois-Connection P Q G
          ( map-lower-adjoint-Galois-Connection P Q G x)))
      ( preserves-order-lower-adjoint-Galois-Connection P Q G x
        ( map-upper-adjoint-Galois-Connection P Q G
          ( 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-inv-adjoint-relation-Galois-Connection P Q G
        ( map-upper-adjoint-Galois-Connection P Q G
          ( 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
          ( lower-adjoint-Galois-Connection P Q G)
          ( upper-adjoint-Galois-Connection P Q G))
        ( comp-hom-Poset Q P Q
          ( lower-adjoint-Galois-Connection P Q G)
          ( upper-adjoint-Galois-Connection P Q G)))
      ( comp-hom-Poset Q P Q
        ( lower-adjoint-Galois-Connection P Q G)
        ( upper-adjoint-Galois-Connection P Q G))
  htpy-idempotent-lower-upper-Galois-Connection x =
    ap
      ( map-lower-adjoint-Galois-Connection P Q G)
      ( 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
          ( upper-adjoint-Galois-Connection P Q G)
          ( lower-adjoint-Galois-Connection P Q G))
        ( comp-hom-Poset P Q P
          ( upper-adjoint-Galois-Connection P Q G)
          ( lower-adjoint-Galois-Connection P Q G)))
      ( comp-hom-Poset P Q P
        ( upper-adjoint-Galois-Connection P Q G)
        ( lower-adjoint-Galois-Connection P Q G))
  htpy-idempotent-upper-lower-Galois-Connection y =
    ap
      ( map-upper-adjoint-Galois-Connection P Q G)
      ( inv
        ( compute-lower-upper-lower-adjoint-Galois-Connection P Q G y))

References

[EKMS93]
M. Erné, J. Koslowski, A. Melton, and G. E. Strecker. A Primer on Galois Connections. Annals of the New York Academy of Sciences, 704(1):103–125, 1993. doi:10.1111/j.1749-6632.1993.tb52513.x.

Recent changes