Galois connections
module order-theory.galois-connections where
Imports
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 : type-hom-Poset P Q → type-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 : type-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 : type-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 = Σ ( type-hom-Poset Q P) is-upper-adjoint-Galois-Connection module _ (G : Galois-Connection) where upper-adjoint-Galois-Connection : type-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 : type-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 : type-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 : type-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-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-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
- Erné, Koslowski, Melton, Strecker. A primer on Galois connections. Annals New York Academy of Sciences 704 (1993)