# Theory Galois_Connection

theory Galois_Connection
imports Complete_Lattice
```(*  Title:      HOL/Algebra/Galois_Connection.thy
Author:     Alasdair Armstrong and Simon Foster
Copyright:  Alasdair Armstrong and Simon Foster
*)

theory Galois_Connection
imports Complete_Lattice
begin

section ‹Galois connections›

subsection ‹Definition and basic properties›

record ('a, 'b, 'c, 'd) galcon =
orderA :: "('a, 'c) gorder_scheme" ("𝒳ı")
orderB :: "('b, 'd) gorder_scheme" ("𝒴ı")
lower  :: "'a ⇒ 'b" ("π⇧*ı")
upper  :: "'b ⇒ 'a" ("π⇩*ı")

type_synonym ('a, 'b) galois = "('a, 'b, unit, unit) galcon"

abbreviation "inv_galcon G ≡ ⦇ orderA = inv_gorder 𝒴⇘G⇙, orderB = inv_gorder 𝒳⇘G⇙, lower = upper G, upper = lower G ⦈"

definition comp_galcon :: "('b, 'c) galois ⇒ ('a, 'b) galois ⇒ ('a, 'c) galois" (infixr "∘⇩g" 85)
where "G ∘⇩g F = ⦇ orderA = orderA F, orderB = orderB G, lower = lower G ∘ lower F, upper = upper F ∘ upper G ⦈"

definition id_galcon :: "'a gorder ⇒ ('a, 'a) galois" ("I⇩g") where
"I⇩g(A) = ⦇ orderA = A, orderB = A, lower = id, upper = id ⦈"

subsection ‹Well-typed connections›

locale connection =
fixes G (structure)
assumes is_order_A: "partial_order 𝒳"
and is_order_B: "partial_order 𝒴"
and lower_closure: "π⇧* ∈ carrier 𝒳 → carrier 𝒴"
and upper_closure: "π⇩* ∈ carrier 𝒴 → carrier 𝒳"
begin

lemma lower_closed: "x ∈ carrier 𝒳 ⟹ π⇧* x ∈ carrier 𝒴"
using lower_closure by auto

lemma upper_closed: "y ∈ carrier 𝒴 ⟹ π⇩* y ∈ carrier 𝒳"
using upper_closure by auto

end

subsection ‹Galois connections›

locale galois_connection = connection +
assumes galois_property: "⟦x ∈ carrier 𝒳; y ∈ carrier 𝒴⟧ ⟹ π⇧* x ⊑⇘𝒴⇙ y ⟷ x ⊑⇘𝒳⇙ π⇩* y"
begin

lemma is_weak_order_A: "weak_partial_order 𝒳"
proof -
interpret po: partial_order 𝒳
by (metis is_order_A)
show ?thesis ..
qed

lemma is_weak_order_B: "weak_partial_order 𝒴"
proof -
interpret po: partial_order 𝒴
by (metis is_order_B)
show ?thesis ..
qed

lemma right: "⟦x ∈ carrier 𝒳; y ∈ carrier 𝒴; π⇧* x ⊑⇘𝒴⇙ y⟧ ⟹ x ⊑⇘𝒳⇙ π⇩* y"
by (metis galois_property)

lemma left: "⟦x ∈ carrier 𝒳; y ∈ carrier 𝒴; x ⊑⇘𝒳⇙ π⇩* y⟧ ⟹ π⇧* x ⊑⇘𝒴⇙ y"
by (metis galois_property)

lemma deflation: "y ∈ carrier 𝒴 ⟹ π⇧* (π⇩* y) ⊑⇘𝒴⇙ y"
by (metis Pi_iff is_weak_order_A left upper_closure weak_partial_order.le_refl)

lemma inflation: "x ∈ carrier 𝒳 ⟹ x ⊑⇘𝒳⇙ π⇩* (π⇧* x)"
by (metis (no_types, lifting) PiE galois_connection.right galois_connection_axioms is_weak_order_B lower_closure weak_partial_order.le_refl)

lemma lower_iso: "isotone 𝒳 𝒴 π⇧*"
show "weak_partial_order 𝒳"
by (metis is_weak_order_A)
show "weak_partial_order 𝒴"
by (metis is_weak_order_B)
fix x y
assume a: "x ∈ carrier 𝒳" "y ∈ carrier 𝒳" "x ⊑⇘𝒳⇙ y"
have b: "π⇧* y ∈ carrier 𝒴"
using a(2) lower_closure by blast
then have "π⇩* (π⇧* y) ∈ carrier 𝒳"
using upper_closure by blast
then have "x ⊑⇘𝒳⇙ π⇩* (π⇧* y)"
by (meson a inflation is_weak_order_A weak_partial_order.le_trans)
thus "π⇧* x ⊑⇘𝒴⇙ π⇧* y"
by (meson b a(1) Pi_iff galois_property lower_closure upper_closure)
qed

lemma upper_iso: "isotone 𝒴 𝒳 π⇩*"
apply (metis is_weak_order_B)
apply (metis is_weak_order_A)
apply (metis (no_types, lifting) Pi_mem deflation is_weak_order_B lower_closure right upper_closure weak_partial_order.le_trans)
done

lemma lower_comp: "x ∈ carrier 𝒳 ⟹ π⇧* (π⇩* (π⇧* x)) = π⇧* x"
by (meson deflation funcset_mem inflation is_order_B lower_closure lower_iso partial_order.le_antisym upper_closure use_iso2)

lemma lower_comp': "x ∈ carrier 𝒳 ⟹ (π⇧* ∘ π⇩* ∘ π⇧*) x = π⇧* x"

lemma upper_comp: "y ∈ carrier 𝒴 ⟹ π⇩* (π⇧* (π⇩* y)) = π⇩* y"
proof -
assume a1: "y ∈ carrier 𝒴"
hence f1: "π⇩* y ∈ carrier 𝒳" using upper_closure by blast
have f2: "π⇧* (π⇩* y) ⊑⇘𝒴⇙ y" using a1 deflation by blast
have f3: "π⇩* (π⇧* (π⇩* y)) ∈ carrier 𝒳"
using f1 lower_closure upper_closure by auto
have "π⇧* (π⇩* y) ∈ carrier 𝒴" using f1 lower_closure by blast
thus "π⇩* (π⇧* (π⇩* y)) = π⇩* y"
by (meson a1 f1 f2 f3 inflation is_order_A partial_order.le_antisym upper_iso use_iso2)
qed

lemma upper_comp': "y ∈ carrier 𝒴 ⟹ (π⇩* ∘ π⇧* ∘ π⇩*) y = π⇩* y"

lemma adjoint_idem1: "idempotent 𝒴 (π⇧* ∘ π⇩*)"
by (simp add: idempotent_def is_order_B partial_order.eq_is_equal upper_comp)

lemma adjoint_idem2: "idempotent 𝒳 (π⇩* ∘ π⇧*)"
by (simp add: idempotent_def is_order_A partial_order.eq_is_equal lower_comp)

lemma fg_iso: "isotone 𝒴 𝒴 (π⇧* ∘ π⇩*)"
by (metis iso_compose lower_closure lower_iso upper_closure upper_iso)

lemma gf_iso: "isotone 𝒳 𝒳 (π⇩* ∘ π⇧*)"
by (metis iso_compose lower_closure lower_iso upper_closure upper_iso)

lemma semi_inverse1: "x ∈ carrier 𝒳 ⟹ π⇧* x = π⇧* (π⇩* (π⇧* x))"
by (metis lower_comp)

lemma semi_inverse2: "x ∈ carrier 𝒴 ⟹ π⇩* x = π⇩* (π⇧* (π⇩* x))"
by (metis upper_comp)

theorem lower_by_complete_lattice:
assumes "complete_lattice 𝒴" "x ∈ carrier 𝒳"
shows "π⇧*(x) = ⨅⇘𝒴⇙ { y ∈ carrier 𝒴. x ⊑⇘𝒳⇙ π⇩*(y) }"
proof -
interpret Y: complete_lattice 𝒴

show ?thesis
proof (rule Y.le_antisym)
show x: "π⇧* x ∈ carrier 𝒴"
using assms(2) lower_closure by blast
show "π⇧* x ⊑⇘𝒴⇙ ⨅⇘𝒴⇙{y ∈ carrier 𝒴. x ⊑⇘𝒳⇙ π⇩* y}"
proof (rule Y.weak.inf_greatest)
show "{y ∈ carrier 𝒴. x ⊑⇘𝒳⇙ π⇩* y} ⊆ carrier 𝒴"
by auto
show "π⇧* x ∈ carrier 𝒴" by (fact x)
fix z
assume "z ∈ {y ∈ carrier 𝒴. x ⊑⇘𝒳⇙ π⇩* y}"
thus "π⇧* x ⊑⇘𝒴⇙ z"
using assms(2) left by auto
qed
show "⨅⇘𝒴⇙{y ∈ carrier 𝒴. x ⊑⇘𝒳⇙ π⇩* y} ⊑⇘𝒴⇙ π⇧* x"
proof (rule Y.weak.inf_lower)
show "{y ∈ carrier 𝒴. x ⊑⇘𝒳⇙ π⇩* y} ⊆ carrier 𝒴"
by auto
show "π⇧* x ∈ {y ∈ carrier 𝒴. x ⊑⇘𝒳⇙ π⇩* y}"
proof (auto)
show "π⇧* x ∈ carrier 𝒴" by (fact x)
show "x ⊑⇘𝒳⇙ π⇩* (π⇧* x)"
using assms(2) inflation by blast
qed
qed
show "⨅⇘𝒴⇙{y ∈ carrier 𝒴. x ⊑⇘𝒳⇙ π⇩* y} ∈ carrier 𝒴"
by (auto intro: Y.weak.inf_closed)
qed
qed

theorem upper_by_complete_lattice:
assumes "complete_lattice 𝒳" "y ∈ carrier 𝒴"
shows "π⇩*(y) = ⨆⇘𝒳⇙ { x ∈ carrier 𝒳. π⇧*(x) ⊑⇘𝒴⇙ y }"
proof -
interpret X: complete_lattice 𝒳
show ?thesis
proof (rule X.le_antisym)
show y: "π⇩* y ∈ carrier 𝒳"
using assms(2) upper_closure by blast
show "π⇩* y ⊑⇘𝒳⇙ ⨆⇘𝒳⇙{x ∈ carrier 𝒳. π⇧* x ⊑⇘𝒴⇙ y}"
proof (rule X.weak.sup_upper)
show "{x ∈ carrier 𝒳. π⇧* x ⊑⇘𝒴⇙ y} ⊆ carrier 𝒳"
by auto
show "π⇩* y ∈ {x ∈ carrier 𝒳. π⇧* x ⊑⇘𝒴⇙ y}"
proof (auto)
show "π⇩* y ∈ carrier 𝒳" by (fact y)
show "π⇧* (π⇩* y) ⊑⇘𝒴⇙ y"
qed
qed
show "⨆⇘𝒳⇙{x ∈ carrier 𝒳. π⇧* x ⊑⇘𝒴⇙ y} ⊑⇘𝒳⇙ π⇩* y"
proof (rule X.weak.sup_least)
show "{x ∈ carrier 𝒳. π⇧* x ⊑⇘𝒴⇙ y} ⊆ carrier 𝒳"
by auto
show "π⇩* y ∈ carrier 𝒳" by (fact y)
fix z
assume "z ∈ {x ∈ carrier 𝒳. π⇧* x ⊑⇘𝒴⇙ y}"
thus "z ⊑⇘𝒳⇙ π⇩* y"
qed
show "⨆⇘𝒳⇙{x ∈ carrier 𝒳. π⇧* x ⊑⇘𝒴⇙ y} ∈ carrier 𝒳"
by (auto intro: X.weak.sup_closed)
qed
qed

end

lemma dual_galois [simp]: " galois_connection ⦇ orderA = inv_gorder B, orderB = inv_gorder A, lower = f, upper = g ⦈
= galois_connection ⦇ orderA = A, orderB = B, lower = g, upper = f ⦈"
by (auto simp add: galois_connection_def galois_connection_axioms_def connection_def dual_order_iff)

definition lower_adjoint :: "('a, 'c) gorder_scheme ⇒ ('b, 'd) gorder_scheme ⇒ ('a ⇒ 'b) ⇒ bool" where
"lower_adjoint A B f ≡ ∃g. galois_connection ⦇ orderA = A, orderB = B, lower = f, upper = g ⦈"

definition upper_adjoint :: "('a, 'c) gorder_scheme ⇒ ('b, 'd) gorder_scheme ⇒ ('b ⇒ 'a) ⇒ bool" where
"upper_adjoint A B g ≡ ∃f. galois_connection ⦇ orderA = A, orderB = B, lower = f, upper = g ⦈"

lemma lower_type: "lower_adjoint A B f ⟹ f ∈ carrier A → carrier B"

lemma upper_type: "upper_adjoint A B g ⟹ g ∈ carrier B → carrier A"

subsection ‹Composition of Galois connections›

lemma id_galois: "partial_order A ⟹ galois_connection (I⇩g(A))"
by (simp add: id_galcon_def galois_connection_def galois_connection_axioms_def connection_def)

lemma comp_galcon_closed:
assumes "galois_connection G" "galois_connection F" "𝒴⇘F⇙ = 𝒳⇘G⇙"
shows "galois_connection (G ∘⇩g F)"
proof -
interpret F: galois_connection F
interpret G: galois_connection G

have "partial_order 𝒳⇘G ∘⇩g F⇙"
moreover have "partial_order 𝒴⇘G ∘⇩g F⇙"
moreover have "π⇧*⇘G⇙ ∘ π⇧*⇘F⇙ ∈ carrier 𝒳⇘F⇙ → carrier 𝒴⇘G⇙"
using F.lower_closure G.lower_closure assms(3) by auto
moreover have "π⇩*⇘F⇙ ∘ π⇩*⇘G⇙ ∈ carrier 𝒴⇘G⇙ → carrier 𝒳⇘F⇙"
using F.upper_closure G.upper_closure assms(3) by auto
moreover
have "⋀ x y. ⟦x ∈ carrier 𝒳⇘F⇙; y ∈ carrier 𝒴⇘G⇙ ⟧ ⟹
(π⇧*⇘G⇙ (π⇧*⇘F⇙ x) ⊑⇘𝒴⇘G⇙⇙ y) = (x ⊑⇘𝒳⇘F⇙⇙ π⇩*⇘F⇙ (π⇩*⇘G⇙ y))"
by (metis F.galois_property F.lower_closure G.galois_property G.upper_closure assms(3) Pi_iff)
ultimately show ?thesis
by (simp add: comp_galcon_def galois_connection_def galois_connection_axioms_def connection_def)
qed

lemma comp_galcon_right_unit [simp]: "F ∘⇩g I⇩g(𝒳⇘F⇙) = F"

lemma comp_galcon_left_unit [simp]: "I⇩g(𝒴⇘F⇙) ∘⇩g F = F"

lemma galois_connectionI:
assumes
"partial_order A" "partial_order B"
"L ∈ carrier A → carrier B" "R ∈ carrier B → carrier A"
"isotone A B L" "isotone B A R"
"⋀ x y. ⟦ x ∈ carrier A; y ∈ carrier B ⟧ ⟹ L x ⊑⇘B⇙ y ⟷ x ⊑⇘A⇙ R y"
shows "galois_connection ⦇ orderA = A, orderB = B, lower = L, upper = R ⦈"
using assms by (simp add: galois_connection_def connection_def galois_connection_axioms_def)

lemma galois_connectionI':
assumes
"partial_order A" "partial_order B"
"L ∈ carrier A → carrier B" "R ∈ carrier B → carrier A"
"isotone A B L" "isotone B A R"
"⋀ X. X ∈ carrier(B) ⟹ L(R(X)) ⊑⇘B⇙ X"
"⋀ X. X ∈ carrier(A) ⟹ X ⊑⇘A⇙ R(L(X))"
shows "galois_connection ⦇ orderA = A, orderB = B, lower = L, upper = R ⦈"
using assms
by (auto simp add: galois_connection_def connection_def galois_connection_axioms_def, (meson PiE isotone_def weak_partial_order.le_trans)+)

subsection ‹Retracts›

locale retract = galois_connection +
assumes retract_property: "x ∈ carrier 𝒳 ⟹ π⇩* (π⇧* x) ⊑⇘𝒳⇙ x"
begin
lemma retract_inverse: "x ∈ carrier 𝒳 ⟹ π⇩* (π⇧* x) = x"
by (meson funcset_mem inflation is_order_A lower_closure partial_order.le_antisym retract_axioms retract_axioms_def retract_def upper_closure)

lemma retract_injective: "inj_on π⇧* (carrier 𝒳)"
by (metis inj_onI retract_inverse)
end

theorem comp_retract_closed:
assumes "retract G" "retract F" "𝒴⇘F⇙ = 𝒳⇘G⇙"
shows "retract (G ∘⇩g F)"
proof -
interpret f: retract F
interpret g: retract G
interpret gf: galois_connection "(G ∘⇩g F)"
by (simp add: assms(1) assms(2) assms(3) comp_galcon_closed retract.axioms(1))
show ?thesis
proof
fix x
assume "x ∈ carrier 𝒳⇘G ∘⇩g F⇙"
thus "le 𝒳⇘G ∘⇩g F⇙ (π⇩*⇘G ∘⇩g F⇙ (π⇧*⇘G ∘⇩g F⇙ x)) x"
using assms(3) f.inflation f.lower_closed f.retract_inverse g.retract_inverse by (auto simp add: comp_galcon_def)
qed
qed

subsection ‹Coretracts›

locale coretract = galois_connection +
assumes coretract_property: "y ∈ carrier 𝒴 ⟹ y ⊑⇘𝒴⇙ π⇧* (π⇩* y)"
begin
lemma coretract_inverse: "y ∈ carrier 𝒴 ⟹ π⇧* (π⇩* y) = y"
by (meson coretract_axioms coretract_axioms_def coretract_def deflation funcset_mem is_order_B lower_closure partial_order.le_antisym upper_closure)

lemma retract_injective: "inj_on π⇩* (carrier 𝒴)"
by (metis coretract_inverse inj_onI)
end

theorem comp_coretract_closed:
assumes "coretract G" "coretract F" "𝒴⇘F⇙ = 𝒳⇘G⇙"
shows "coretract (G ∘⇩g F)"
proof -
interpret f: coretract F
interpret g: coretract G
interpret gf: galois_connection "(G ∘⇩g F)"
by (simp add: assms(1) assms(2) assms(3) comp_galcon_closed coretract.axioms(1))
show ?thesis
proof
fix y
assume "y ∈ carrier 𝒴⇘G ∘⇩g F⇙"
thus "le 𝒴⇘G ∘⇩g F⇙ y (π⇧*⇘G ∘⇩g F⇙ (π⇩*⇘G ∘⇩g F⇙ y))"
by (simp add: comp_galcon_def assms(3) f.coretract_inverse g.coretract_property g.upper_closed)
qed
qed

subsection ‹Galois Bijections›

locale galois_bijection = connection +
assumes lower_iso: "isotone 𝒳 𝒴 π⇧*"
and upper_iso: "isotone 𝒴 𝒳 π⇩*"
and lower_inv_eq: "x ∈ carrier 𝒳 ⟹ π⇩* (π⇧* x) = x"
and upper_inv_eq: "y ∈ carrier 𝒴 ⟹ π⇧* (π⇩* y) = y"
begin

lemma lower_bij: "bij_betw π⇧* (carrier 𝒳) (carrier 𝒴)"
by (rule bij_betwI[where g="π⇩*"], auto intro: upper_inv_eq lower_inv_eq upper_closed lower_closed)

lemma upper_bij: "bij_betw π⇩* (carrier 𝒴) (carrier 𝒳)"
by (rule bij_betwI[where g="π⇧*"], auto intro: upper_inv_eq lower_inv_eq upper_closed lower_closed)

sublocale gal_bij_conn: galois_connection
apply (unfold_locales, auto)
using lower_closed lower_inv_eq upper_iso use_iso2 apply fastforce
using lower_iso upper_closed upper_inv_eq use_iso2 apply fastforce
done

sublocale gal_bij_ret: retract
by (unfold_locales, simp add: gal_bij_conn.is_weak_order_A lower_inv_eq weak_partial_order.le_refl)

sublocale gal_bij_coret: coretract
by (unfold_locales, simp add: gal_bij_conn.is_weak_order_B upper_inv_eq weak_partial_order.le_refl)

end

theorem comp_galois_bijection_closed:
assumes "galois_bijection G" "galois_bijection F" "𝒴⇘F⇙ = 𝒳⇘G⇙"
shows "galois_bijection (G ∘⇩g F)"
proof -
interpret f: galois_bijection F
interpret g: galois_bijection G
interpret gf: galois_connection "(G ∘⇩g F)"
by (simp add: assms(3) comp_galcon_closed f.gal_bij_conn.galois_connection_axioms g.gal_bij_conn.galois_connection_axioms galois_connection.axioms(1))
show ?thesis
proof
show "isotone 𝒳⇘G ∘⇩g F⇙ 𝒴⇘G ∘⇩g F⇙ π⇧*⇘G ∘⇩g F⇙"
by (simp add: comp_galcon_def, metis comp_galcon_def galcon.select_convs(1) galcon.select_convs(2) galcon.select_convs(3) gf.lower_iso)
show "isotone 𝒴⇘G ∘⇩g F⇙ 𝒳⇘G ∘⇩g F⇙ π⇩*⇘G ∘⇩g F⇙"
fix x
assume "x ∈ carrier 𝒳⇘G ∘⇩g F⇙"
thus "π⇩*⇘G ∘⇩g F⇙ (π⇧*⇘G ∘⇩g F⇙ x) = x"
using assms(3) f.lower_closed f.lower_inv_eq g.lower_inv_eq by (auto simp add: comp_galcon_def)
next
fix y
assume "y ∈ carrier 𝒴⇘G ∘⇩g F⇙"
thus "π⇧*⇘G ∘⇩g F⇙ (π⇩*⇘G ∘⇩g F⇙ y) = y"
by (simp add: comp_galcon_def assms(3) f.upper_inv_eq g.upper_closed g.upper_inv_eq)
qed
qed

end
```