Theory Order_Lattice_Props.Galois_Connections
section ‹Galois Connections›
theory Galois_Connections
imports Order_Lattice_Props
begin
subsection ‹Definitions and Basic Properties›
text ‹The approach follows the Compendium of Continuous Lattices~\<^cite>‹"GierzHKLMS80"›, without attempting completeness.
First, left and right adjoints of a Galois connection are defined.›
definition adj :: "('a::ord ⇒ 'b::ord) ⇒ ('b ⇒ 'a) ⇒ bool" (infixl "⊣" 70) where
"(f ⊣ g) = (∀x y. (f x ≤ y) = (x ≤ g y))"
definition "ladj (g::'a::Inf ⇒ 'b::ord) = (λx. ⨅{y. x ≤ g y})"
definition "radj (f::'a::Sup ⇒ 'b::ord) = (λy. ⨆{x. f x ≤ y})"
lemma ladj_radj_dual:
fixes f :: "'a::complete_lattice_with_dual ⇒ 'b::ord_with_dual"
shows "ladj f x = ∂ (radj (∂⇩F f) (∂ x))"
proof-
have "ladj f x = ∂ (⨆(∂ ` {y. ∂ (f y) ≤ ∂ x}))"
unfolding ladj_def by (metis (no_types, lifting) Collect_cong Inf_dual_var dual_dual_ord dual_iff)
also have "... = ∂ (⨆{∂ y|y. ∂ (f y) ≤ ∂ x})"
by (simp add: setcompr_eq_image)
ultimately show ?thesis
unfolding ladj_def radj_def map_dual_def comp_def
by (smt (verit) Collect_cong invol_dual_var)
qed
lemma radj_ladj_dual:
fixes f :: "'a::complete_lattice_with_dual ⇒ 'b::ord_with_dual"
shows "radj f x = ∂ (ladj (∂⇩F f) (∂ x))"
by (metis fun_dual5 invol_dual_var ladj_radj_dual map_dual_def)
lemma ladj_prop:
fixes g :: "'b::Inf ⇒ 'a::ord_with_dual"
shows "ladj g = Inf ∘ (-`) g ∘ ↑"
unfolding ladj_def vimage_def upset_prop fun_eq_iff comp_def by simp
lemma radj_prop:
fixes f :: "'b::Sup ⇒ 'a::ord"
shows "radj f = Sup ∘ (-`) f ∘ ↓"
unfolding radj_def vimage_def downset_prop fun_eq_iff comp_def by simp
text ‹The first set of properties holds without any sort assumptions.›
lemma adj_iso1: "f ⊣ g ⟹ mono f"
unfolding adj_def mono_def by (meson dual_order.refl dual_order.trans)
lemma adj_iso2: "f ⊣ g ⟹ mono g"
unfolding adj_def mono_def by (meson dual_order.refl dual_order.trans)
lemma adj_comp: "f ⊣ g ⟹ adj h k ⟹ (f ∘ h) ⊣ (k ∘ g)"
by (simp add: adj_def)
lemma adj_dual:
fixes f :: "'a::ord_with_dual ⇒ 'b::ord_with_dual"
shows "f ⊣ g = (∂⇩F g) ⊣ (∂⇩F f)"
unfolding adj_def map_dual_def comp_def by (metis (mono_tags, opaque_lifting) dual_dual_ord invol_dual_var)
subsection ‹Properties for (Pre)Orders›
text ‹The next set of properties holds in preorders or orders.›
lemma adj_cancel1:
fixes f :: "'a::preorder ⇒ 'b::ord"
shows "f ⊣ g ⟹ f ∘ g ≤ id"
by (simp add: adj_def le_funI)
lemma adj_cancel2:
fixes f :: "'a::ord ⇒ 'b::preorder"
shows "f ⊣ g ⟹ id ≤ g ∘ f"
by (simp add: adj_def eq_iff le_funI)
lemma adj_prop:
fixes f :: "'a::preorder ⇒'a"
shows "f ⊣ g ⟹ f ∘ g ≤ g ∘ f"
using adj_cancel1 adj_cancel2 order_trans by blast
lemma adj_cancel_eq1:
fixes f :: "'a::preorder ⇒ 'b::order"
shows "f ⊣ g ⟹ f ∘ g ∘ f = f"
unfolding adj_def comp_def fun_eq_iff by (meson eq_iff order_refl order_trans)
lemma adj_cancel_eq2:
fixes f :: "'a::order ⇒ 'b::preorder"
shows "f ⊣ g ⟹ g ∘ f ∘ g = g"
unfolding adj_def comp_def fun_eq_iff by (meson eq_iff order_refl order_trans)
lemma adj_idem1:
fixes f :: "'a::preorder ⇒ 'b::order"
shows "f ⊣ g ⟹ (f ∘ g) ∘ (f ∘ g) = f ∘ g"
by (simp add: adj_cancel_eq1 rewriteL_comp_comp)
lemma adj_idem2:
fixes f :: "'a::order ⇒ 'b::preorder"
shows "f ⊣ g ⟹ (g ∘ f) ∘ (g ∘ f) = g ∘ f"
by (simp add: adj_cancel_eq2 rewriteL_comp_comp)
lemma adj_iso3:
fixes f :: "'a::order ⇒ 'b::order"
shows "f ⊣ g ⟹ mono (f ∘ g)"
by (simp add: adj_iso1 adj_iso2 monoD monoI)
lemma adj_iso4:
fixes f :: "'a::order ⇒ 'b::order"
shows "f ⊣ g ⟹ mono (g ∘ f)"
by (simp add: adj_iso1 adj_iso2 monoD monoI)
lemma adj_canc1:
fixes f :: "'a::order ⇒ 'b::ord"
shows "f ⊣ g ⟹ ((f ∘ g) x = (f ∘ g) y ⟶ g x = g y)"
unfolding adj_def comp_def by (metis eq_iff)
lemma adj_canc2:
fixes f :: "'a::ord ⇒ 'b::order"
shows "f ⊣ g ⟹ ((g ∘ f) x = (g ∘ f) y ⟶ f x = f y)"
unfolding adj_def comp_def by (metis eq_iff)
lemma adj_sur_inv:
fixes f :: "'a::preorder ⇒ 'b::order"
shows "f ⊣ g ⟹ ((surj f) = (f ∘ g = id))"
unfolding adj_def surj_def comp_def by (metis eq_id_iff eq_iff order_refl order_trans)
lemma adj_surj_inj:
fixes f :: "'a::order ⇒ 'b::order"
shows "f ⊣ g ⟹ ((surj f) = (inj g))"
unfolding adj_def inj_def surj_def by (metis eq_iff order_trans)
lemma adj_inj_inv:
fixes f :: "'a::preorder ⇒ 'b::order"
shows "f ⊣ g ⟹ ((inj f) = (g ∘ f = id))"
by (metis adj_cancel_eq1 eq_id_iff inj_def o_apply)
lemma adj_inj_surj:
fixes f :: "'a::order ⇒ 'b::order"
shows "f ⊣ g ⟹ ((inj f) = (surj g))"
unfolding adj_def inj_def surj_def by (metis eq_iff order_trans)
lemma surj_id_the_inv: "surj f ⟹ g ∘ f = id ⟹ g = the_inv f"
by (metis comp_apply id_apply inj_on_id inj_on_imageI2 surj_fun_eq the_inv_f_f)
lemma inj_id_the_inv: "inj f ⟹ f ∘ g = id ⟹ f = the_inv g"
proof -
assume a1: "inj f"
assume "f ∘ g = id"
hence "∀x. the_inv g x = f x"
using a1 by (metis (no_types) comp_apply eq_id_iff inj_on_id inj_on_imageI2 the_inv_f_f)
thus ?thesis
by presburger
qed
subsection ‹Properties for Complete Lattices›
text ‹The next laws state that a function between complete lattices preserves infs
if and only if it has a lower adjoint.›
lemma radj_Inf_pres:
fixes g :: "'b::complete_lattice ⇒ 'a::complete_lattice"
shows "(∃f. f ⊣ g) ⟹ Inf_pres g"
apply (rule antisym, simp_all add: le_fun_def adj_def, safe)
apply (meson INF_greatest Inf_lower dual_order.refl dual_order.trans)
by (meson Inf_greatest dual_order.refl le_INF_iff)
lemma ladj_Sup_pres:
fixes f :: "'a::complete_lattice_with_dual ⇒ 'b::complete_lattice_with_dual"
shows "(∃g. f ⊣ g) ⟹ Sup_pres f"
using Sup_pres_map_dual_var adj_dual radj_Inf_pres by blast
lemma radj_adj:
fixes f :: "'a::complete_lattice ⇒ 'b::complete_lattice"
shows "f ⊣ g ⟹ g = (radj f)"
unfolding adj_def radj_def by (metis (mono_tags, lifting) cSup_eq_maximum eq_iff mem_Collect_eq)
lemma ladj_adj:
fixes g :: "'b::complete_lattice_with_dual ⇒ 'a::complete_lattice_with_dual"
shows "f ⊣ g ⟹ f = (ladj g)"
unfolding adj_def ladj_def by (metis (no_types, lifting) cInf_eq_minimum eq_iff mem_Collect_eq)
lemma Inf_pres_radj_aux:
fixes g :: "'a::complete_lattice ⇒ 'b::complete_lattice"
shows "Inf_pres g ⟹ (ladj g) ⊣ g"
proof-
assume a: "Inf_pres g"
{fix x y
assume b: "ladj g x ≤ y"
hence "g (ladj g x) ≤ g y"
by (simp add: Inf_subdistl_iso a monoD)
hence "⨅{g y |y. x ≤ g y} ≤ g y"
by (metis a comp_eq_dest_lhs setcompr_eq_image ladj_def)
hence "x ≤ g y"
using dual_order.trans le_Inf_iff by blast
hence "ladj g x ≤ y ⟶ x ≤ g y"
by simp}
thus ?thesis
unfolding adj_def ladj_def by (meson CollectI Inf_lower)
qed
lemma Sup_pres_ladj_aux:
fixes f :: "'a::complete_lattice_with_dual ⇒ 'b::complete_lattice_with_dual"
shows "Sup_pres f ⟹ f ⊣ (radj f)"
by (metis (no_types, opaque_lifting) Inf_pres_radj_aux Sup_pres_map_dual_var adj_dual fun_dual5 map_dual_def radj_adj)
lemma Inf_pres_radj:
fixes g :: "'b::complete_lattice ⇒ 'a::complete_lattice"
shows "Inf_pres g ⟹ (∃f. f ⊣ g)"
using Inf_pres_radj_aux by fastforce
lemma Sup_pres_ladj:
fixes f :: "'a::complete_lattice_with_dual ⇒ 'b::complete_lattice_with_dual"
shows "Sup_pres f ⟹ (∃g. f ⊣ g)"
using Sup_pres_ladj_aux by fastforce
lemma Inf_pres_upper_adj_eq:
fixes g :: "'b::complete_lattice ⇒ 'a::complete_lattice"
shows "(Inf_pres g) = (∃f. f ⊣ g)"
using radj_Inf_pres Inf_pres_radj by blast
lemma Sup_pres_ladj_eq:
fixes f :: "'a::complete_lattice_with_dual ⇒ 'b::complete_lattice_with_dual"
shows "(Sup_pres f) = (∃g. f ⊣ g)"
using Sup_pres_ladj ladj_Sup_pres by blast
lemma Sup_downset_adj: "(Sup::'a::complete_lattice set ⇒ 'a) ⊣ ↓"
unfolding adj_def downset_prop Sup_le_iff by force
lemma Sup_downset_adj_var: "(Sup (X::'a::complete_lattice set) ≤ y) = (X ⊆ ↓y)"
using Sup_downset_adj adj_def by auto
text ‹Once again many statements arise by duality, which Isabelle usually picks up.›
end