Theory Order_Lattice_Props.Galois_Connections

(* 
  Title: Galois Connections
  Author: Georg Struth 
  Maintainer: Georg Struth <g.struth@sheffield.ac.uk> 
*)

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