# Theory Galois_Connection

```(*  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"

proof -
assume a1: "y β carrier π΄"
hence f1: "Οβ©* y β carrier π³" using upper_closure by blast
have f2: "Οβ§* (Οβ©* y) ββπ΄β y" using a1 deflation by blast
using f1 lower_closure upper_closure by auto
have "Οβ§* (Οβ©* y) β carrier π΄" using f1 lower_closure by blast
by (meson a1 f1 f2 f3 inflation is_order_A partial_order.le_antisym upper_iso use_iso2)
qed

by (simp add: idempotent_def is_order_B partial_order.eq_is_equal upper_comp)

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)

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}"
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β"
proof -
interpret F: galois_connection F
interpret G: galois_connection G

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
using F.upper_closure G.upper_closure assms(3) by auto
moreover
have "β x y. β¦x β carrier π³βFβ; y β carrier π΄βGβ β§ βΉ
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 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β"
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β"
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β"
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β"
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β"
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
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)
fix x
assume "x β carrier π³βG ββ©g Fβ"