(* Title: Graphing_OrbitRelation.thy Author: Clara L\"oh *) text \We give simple examples of graphings of orbit relations. The goal is to show that generating sets of groups lead to graphings of orbit relations.\ theory Graphing_OrbitRelation imports Complex_Main RelRel_Iso Graphing "HOL-Algebra.Group_Action" "HOL-Algebra.Generated_Groups" begin section \Orbit relations\ definition orbit_relation :: "('a,_) monoid_scheme => 'b set => ('a => 'b => 'b) => ('b \ 'b) set" where "orbit_relation G X rho = { (x, y) | x y. x \ X \ y \ orbit G rho x }" (*HOL-Algebra.Group_Action*) text \Orbit relations are equivalence relations; this is just a wrapper around the proofs from the group action library.\ lemma orbit_relation_rel_on_basespace: fixes G X rho assumes G_is_group: "group G" and rho_is_action: "group_action G X rho" shows "orbit_relation G X rho \ X \ X" proof - (* Setup *) interpret G: group G using G_is_group by simp interpret rho: group_action G X rho using rho_is_action by simp define r where "r = orbit_relation G X rho" show "r \ X \ X" proof fix xy assume xy_in_r: "xy \ r" show "xy \ X \ X" proof (cases xy) case (Pair x y) have x_in_X: "x \ X" using xy_in_r r_def orbit_relation_def[of G X rho] Pair by simp have y_in_X: "y \ X" proof - have "y \ orbit G rho x" using xy_in_r r_def orbit_relation_def[of G X rho] Pair by simp then obtain g where "g \ carrier G" "rho g x = y" using orbit_def[of G rho x] by auto then show "y \ X" using rho_is_action x_in_X group_action.element_image[of G X rho g x y] by simp qed show ?thesis using x_in_X y_in_X Pair by simp qed qed qed lemma orbit_relation_is_eqrel: fixes G X rho assumes G_is_group: "group G" and rho_is_action: "group_action G X rho" shows "equiv X (orbit_relation G X rho)" unfolding equiv_def proof (intro conjI) (* Setup *) interpret G: group G using G_is_group by simp interpret rho: group_action G X rho using rho_is_action by simp define r where "r = orbit_relation G X rho" text \We show that \r\ is a relation on \X\ that satisfies reflexivity, symmetry, and transitivity.\ have r_rel_on_X: "r \ X \ X" using orbit_relation_rel_on_basespace[of G X rho] G_is_group rho_is_action r_def by simp show "refl_on X r" unfolding refl_on_def proof (rule conjI) show "r \ X \ X" using r_rel_on_X by simp show "\ x \ X. (x,x) \ r" proof (intro ballI) fix x assume x_in_X: "x \ X" then have "x \ orbit G rho x" using rho_is_action group_action.orbit_refl[of G X rho] by simp then show "(x,x) \ r" using r_def orbit_relation_def[of G X rho] x_in_X by simp qed qed show "sym r" unfolding sym_def proof (intro allI impI) fix x y assume xy_in_r: "(x,y) \ r" then have x_y_in_X: "x \ X" "y \ X" using r_rel_on_X by auto have "x \ orbit G rho y" proof - have "y \ orbit G rho x" using r_def orbit_relation_def[of G X rho] xy_in_r by simp then show ?thesis using group_action.orbit_sym[of G X rho x y] rho_is_action x_y_in_X by simp qed then show "(y,x) \ r" using r_def orbit_relation_def[of G X rho] x_y_in_X by simp qed show "trans r" unfolding trans_def proof (intro allI impI) fix x y z assume xy_in_r: "(x,y) \ r" and yz_in_r: "(y,z) \ r" then have x_y_z_in_X: "x \ X" "y \ X" "z \ X" using r_rel_on_X by auto have "z \ orbit G rho x" proof - have "y \ orbit G rho x" using r_def orbit_relation_def[of G X rho] xy_in_r by simp moreover have "z \ orbit G rho y" using r_def orbit_relation_def[of G X rho] yz_in_r by simp ultimately show ?thesis using group_action.orbit_trans[of G X rho x y z] rho_is_action x_y_z_in_X by simp qed then show "(x,z) \ r" using r_def orbit_relation_def[of G X rho] x_y_z_in_X by simp qed qed section \A simple graphing of an orbit relation\ text \The automorphism of a group element in a group action as a partial automorphism.\ definition transl_auto_of :: "('a,_) monoid_scheme => 'b set => ('a => 'b => 'b) => 'a => ('b => 'b)" where "transl_auto_of G X rho g = (\ x \ X. (rho g) x)" definition partial_transl_auto_of :: "('a,_) monoid_scheme => 'b set => ('a => 'b => 'b) => 'a => 'b rel" where "partial_transl_auto_of G X rho g = { (x, y) | x y. x \ X \ y = (transl_auto_of G X rho g) x }" definition graphing_of_subset :: "('a,_) monoid_scheme => 'b set => ('a => 'b => 'b) => 'a set => 'b rel set" where "graphing_of_subset G X rho S = { partial_transl_auto_of G X rho g | g. g \ S \ carrier G}" subsection \Basic properties of translations in group actions\ lemma partial_transl_auto_domain_range: fixes G X rho g assumes G_is_group: "group G" and rho_is_action: "group_action G X rho" and g_in_G: "g \ carrier G" shows domain: "Domain (partial_transl_auto_of G X rho g) = X" and range: "Range (partial_transl_auto_of G X rho g) = X" and all: "partial_transl_auto_of G X rho g \ X \ X" proof - (* Setup *) interpret rho: group_action G X rho using rho_is_action by simp define phi where "phi = partial_transl_auto_of G X rho g" define f where "f = rho g" have f_bij: "bij_betw f X X" using rho_is_action group_action.bij_prop0[of G X rho g] f_def g_in_G Bij_def[of X] by simp then have f_surj: "f ` X = X" using bij_betw_def[of f X X] by simp show domain_phi: "Domain phi = X" using phi_def partial_transl_auto_of_def[of G X rho g] by auto show range_phi: "Range phi = X" proof show "Range phi \ X" proof fix y assume y_in_range: "y \ Range phi" then obtain xy where xy_prop: "xy \ phi" "y = snd xy" using Range_def by auto define x where "x = fst xy" have xy_xy: "xy = (x,y)" using xy_prop x_def prod_eqI by simp then have x_in_X: "x \ X" using x_def xy_prop phi_def partial_transl_auto_of_def[of G X rho g] by auto show "y \ X" proof - have "(x,y) \ phi" using xy_xy xy_prop by simp then have "y = transl_auto_of G X rho g x" using phi_def partial_transl_auto_of_def[of G X rho g] by auto then have "f x = y" using f_def transl_auto_of_def[of G X rho g] x_in_X by simp then show "y \ X" using f_surj image_def x_in_X by auto qed qed show "X \ Range phi" proof fix y assume y_in_X: "y \ X" from f_surj obtain "x" where x_prop: "x \ X" "y = f x" using image_def[of f X] y_in_X by auto then have "(x,y) \ phi" using phi_def f_def partial_transl_auto_of_def[of G X rho g] transl_auto_of_def[of G X rho g] by simp then show "y \ Range phi" using Range_def by auto qed qed show "phi \ X \ X" using domain_phi range_phi by auto qed lemma partial_transl_auto_is_partial_auto: fixes G X rho g assumes G_is_group: "group G" and rho_is_action: "group_action G X rho" and g_in_G: "g \ carrier G" shows "is_partial_iso_of (orbit_relation G X rho) (partial_transl_auto_of G X rho g)" proof (intro is_graph_of_partial_isoI) (* Setup *) interpret G: group G using G_is_group by simp interpret rho: group_action G X rho using rho_is_action by simp define r where "r = orbit_relation G X rho" define phi where "phi = partial_transl_auto_of G X rho g" show "phi \ r" proof fix "xy" assume xy_in_phi: "xy \ phi" show "xy \ r" proof (cases xy) case (Pair x y) have x_in_X: "x \ X" using xy_in_phi phi_def Pair partial_transl_auto_of_def[of G X rho g] by auto have y_in_orbit: "y \ orbit G rho x" proof - from xy_in_phi obtain "y = (rho g) x" using phi_def partial_transl_auto_of_def[of G X rho g] transl_auto_of_def[of G X rho g] x_in_X Pair by auto then show ?thesis using orbit_def[of G rho x] rho_is_action g_in_G x_in_X by auto qed show ?thesis using r_def orbit_relation_def[of G X rho] x_in_X y_in_orbit Pair by simp qed qed show "is_graph_of_iso phi" proof (intro is_graph_of_isoI is_graph_of_inv_isosI) define f1 where "f1 = rho g" define f2 where "f2 = rho (m_inv G g)" have domain_phi: "Domain phi = X" and range_phi: "Range phi = X" using partial_transl_auto_domain_range[of G X rho g] G_is_group g_in_G phi_def rho_is_action by auto show "is_graph_of phi f1" unfolding is_graph_of_def proof - show "phi = {(x,y). x \ Domain phi \ y = f1 x}" using domain_phi f1_def phi_def partial_transl_auto_of_def[of G X rho g] transl_auto_of_def[of G X rho] by auto qed show "\ x \ Domain phi. (f2 o f1) x = x" proof (intro ballI) fix x assume "x \ Domain phi" then have x_in_X: "x \ X" using domain_phi by simp have "(f2 o f1) x = (rho (m_inv G g)) ((rho g) x)" using f2_def f1_def by simp also have "\ = rho (mult G (m_inv G g) g) x" using rho_is_action group_action.composition_rule[of G X rho x "m_inv G g" g, THEN sym] g_in_G group.inv_closed[of G g] x_in_X by simp also have "\ = (rho (one G)) x" using group.l_inv[of G g] g_in_G by simp finally show "(f2 o f1) x = x" using group_action.id_eq_one[of G X rho, THEN sym] rho_is_action x_in_X by simp qed show "\ x \ Range phi. (f1 o f2) x = x" proof (intro ballI) fix x assume "x \ Range phi" then have x_in_X: "x \ X" using range_phi by simp have "(f1 o f2) x = (rho g) (rho (m_inv G g) x)" using f1_def f2_def by simp also have "\ = rho (mult G g (m_inv G g)) x" using rho_is_action group_action.composition_rule[of G X rho x g "m_inv G g", THEN sym] g_in_G group.inv_closed[of G g] x_in_X by simp also have "\ = rho (one G) x" using group.r_inv[of G g] g_in_G by simp finally show "(f1 o f2) x = x" using group_action.id_eq_one[of G X rho, THEN sym] rho_is_action x_in_X by simp qed qed qed subsection \Some basic properties of general graphings\ lemma graphing_subrel: fixes X r Phi assumes Phi_family_of_partial_isos: "\ phi \ Phi. is_partial_iso_of r phi" and r_is_eqrel: "equiv X r" shows "r \ X \ X" and "Union Phi \ X \ X" and "generated_equiv_rel X (Union Phi) \ r" proof - have UPhi_sub_r: "Union Phi \ r" proof fix x assume "x \ Union Phi" then obtain phi where "phi \ Phi" and x_in_phi: "x \ phi" by auto then have "is_partial_iso_of r phi" using Phi_family_of_partial_isos by simp then have "phi \ r" using is_partial_iso_of_def[of r phi] by simp then show "x \ r" using x_in_phi by auto qed show r_sub_XX: "r \ X \ X" using r_is_eqrel equiv_def[of X r] refl_on_def[of X r] by simp then show Phi_sub_XX: "Union Phi \ X \ X" using UPhi_sub_r subset_trans by simp have "generated_equiv_rel X (Union Phi) \ generated_equiv_rel X r" using UPhi_sub_r r_sub_XX generated_equiv_rel_mono[of "Union Phi" X r] by simp then show "generated_equiv_rel X (Union Phi) \ r" using r_is_eqrel generated_equiv_rel_of_equiv_rel[of X r, THEN sym] by simp qed lemma graphing_of_subset_relonbase: fixes G X rho S_gen_G assumes G_is_group: "group G" and rho_is_action: "group_action G X rho" and S_sub_G: "S \ carrier G" shows "Union (graphing_of_subset G X rho S) \ X \X" proof define Phi where "Phi = graphing_of_subset G X rho S" fix xy assume "xy \ Union Phi" then obtain phi where "phi \ Phi" and xy_in_phi: "xy \ phi" by auto then obtain g where "g \ S" and "phi = partial_transl_auto_of G X rho g" using Phi_def graphing_of_subset_def[of G X rho S] by auto then show "xy \ X \ X" using xy_in_phi S_sub_G G_is_group rho_is_action partial_transl_auto_domain_range[of G X rho g] by blast qed subsection \Basic properties of graphings consisting of translations.\ lemma graphing_of_subset_mono: fixes G X rho S T assumes G_is_group: "group G" and rho_is_action: "group_action G X rho" and S_sub_T: "S \ T" and T_sub_G: "T \ carrier G" shows "graphing_of_subset G X rho S\ graphing_of_subset G X rho T" proof fix phi assume phi_in_genS: "phi \ graphing_of_subset G X rho S" have S_sub_G: "S \ carrier G" using S_sub_T T_sub_G by simp from graphing_of_subset_def[of G X rho S] obtain g where g_in_S: "g \ S" and phi_via_g: "phi = partial_transl_auto_of G X rho g" using phi_in_genS S_sub_G by auto then have "g \ T" using g_in_S S_sub_T by auto then show "phi \ graphing_of_subset G X rho T" using graphing_of_subset_def[of G X rho T] phi_via_g T_sub_G by auto qed lemma graphing_of_subset_contains_subsetaction: fixes G X rho S x g assumes G_is_group: "group G" and rho_is_action: "group_action G X rho" and S_sub_G: "S \ carrier G" and x_in_X: "x \ X" and g_in_S: "g \ S" shows "(x, (rho g) x) \ generated_equiv_rel X (Union (graphing_of_subset G X rho S))" proof - define Phi where "Phi = graphing_of_subset G X rho S" define s where "s = generated_equiv_rel X (Union Phi)" have g_in_G: "g \ carrier G" using g_in_S S_sub_G by auto have "(transl_auto_of G X rho g) x = (rho g) x" using x_in_X g_in_G transl_auto_of_def[of G X rho g] by simp then have "(x, (rho g) x) \ partial_transl_auto_of G X rho g" using x_in_X partial_transl_auto_of_def[of G X rho g] by simp then have "(x, (rho g) x) \ Union Phi" using Phi_def g_in_S g_in_G graphing_of_subset_def[of G X rho S] Union_iff[of "(x, (rho g) x)" Phi] by auto then show ?thesis using Phi_def graphing_subrel S_sub_G G_is_group rho_is_action graphing_of_subset_relonbase[of G X rho S] generated_equiv_rel_contains_generator[of "Union Phi" X] by auto qed subsection \The graphing of all group elements\ lemma whole_group_leads_to_graphing: fixes G X rho assumes G_is_group: "group G" and rho_is_action: "group_action G X rho" shows "is_graphing_of X (orbit_relation G X rho) (graphing_of_subset G X rho (carrier G))" unfolding is_graphing_of_def proof define r where "r = orbit_relation G X rho" define Phi where "Phi = graphing_of_subset G X rho (carrier G)" have Phi_is_family_of_partial_isos: "\ phi \ Phi. is_partial_iso_of r phi" proof fix phi assume "phi \ Phi" then obtain g where g_in_G: "g \ carrier G" and "phi = partial_transl_auto_of G X rho g" using Phi_def graphing_of_subset_def[of G X rho "carrier G"] by auto then show "is_partial_iso_of r phi" using partial_transl_auto_is_partial_auto[of G X rho g] r_def g_in_G G_is_group rho_is_action by simp qed show UPhi_sub_r: "generated_equiv_rel X (Union Phi) \ r" using Phi_is_family_of_partial_isos graphing_subrel[of Phi r X] orbit_relation_is_eqrel[of G X rho] r_def G_is_group rho_is_action by simp have r_sub_UPhi: "r \ Union Phi" proof fix xy assume xy_in_r: "xy \ r" show "xy \ Union Phi" proof (cases xy) case (Pair x y) from xy_in_r obtain g where y_via_g: "y = (rho g) x" and g_in_G: "g \ carrier G" using r_def orbit_relation_def[of G X rho] orbit_def[of G rho x] Pair by auto have x_in_X: "x \ X" using orbit_relation_rel_on_basespace[of G X rho] G_is_group rho_is_action xy_in_r Pair r_def by auto have "(x,y) \ partial_transl_auto_of G X rho g" using y_via_g partial_transl_auto_of_def[of G X rho g] transl_auto_of_def[of G X rho g] restrict_def x_in_X by simp then show "xy \ Union Phi" using Phi_def graphing_of_subset_def[of G X rho "carrier G"] g_in_G Pair by auto qed qed show "r \ generated_equiv_rel X (Union Phi)" proof - have r_is_eqrel: "equiv X r" using r_def G_is_group rho_is_action orbit_relation_is_eqrel[of G X rho] by simp then have "generated_equiv_rel X r \ generated_equiv_rel X (Union Phi)" using r_sub_UPhi generated_equiv_rel_mono[of r X "Union Phi"] graphing_subrel[of Phi r X] Phi_is_family_of_partial_isos by simp then show ?thesis using generated_equiv_rel_of_equiv_rel[of X r] r_is_eqrel by simp qed qed subsection \The graphing of a generating set\ text \We can now prove the main result: The translations of a generating set of a group form graphings for actions of this group.\ theorem generating_set_leads_to_graphing: fixes G X rho S assumes G_is_group: "group G" and rho_is_action: "group_action G X rho" and S_sub_G: "S \ carrier G" and S_gen_G: "generate G S = carrier G" shows "is_graphing_of X (orbit_relation G X rho) (graphing_of_subset G X rho S)" unfolding is_graphing_of_def proof define Phi where "Phi = graphing_of_subset G X rho S" define r where "r = orbit_relation G X rho" define s where "s = generated_equiv_rel X (Union Phi)" have Phi_is_family_of_partial_isos: "\ phi \ Phi. is_partial_iso_of r phi" proof fix phi assume "phi \ Phi" then obtain g where g_in_S: "g \ S" and "phi = partial_transl_auto_of G X rho g" using Phi_def graphing_of_subset_def[of G X rho S] by auto then show "is_partial_iso_of r phi" using partial_transl_auto_is_partial_auto[of G X rho g] r_def g_in_S G_is_group rho_is_action S_sub_G by auto qed text \The easy inclusion:\ have s_sub_r: "s \ r" using Phi_is_family_of_partial_isos graphing_subrel[of Phi r X] orbit_relation_is_eqrel[of G X rho] r_def G_is_group rho_is_action s_def by simp text \For the converse inclusion, we first collect some easy facts; in particular, that the two considered relations indeed are equivalence relations on the underlying space of the action:\ have r_eqrel: "equiv X r" using r_def orbit_relation_is_eqrel[of G X rho] G_is_group rho_is_action by simp have r_sub_XX: "r \ X \ X" and UPhi_sub_XX: "Union Phi \ X \ X" using graphing_subrel[of Phi r X] Phi_is_family_of_partial_isos r_eqrel by auto have s_eqrel: "equiv X s" using s_def generated_equiv_rel_is_equiv_rel[of "Union Phi" X] UPhi_sub_XX by simp text \The converse (not so easy) inclusion:\ have r_sub_s: "r \ s" proof fix xy assume "xy \ r" then show "xy \ s" proof (induct xy) case (Pair x y) text \We prove inductively that the generated equivalence relation contains all the pairs related by group elements in the generated subgroup. The induction is over the inductive structure of the generated subgroup (as smallest subset that contains the generating set, the inverses of elements of the generating set, and which is closed under multiplication. For this induction to work, we will need to generalise over the first component via an all-quantifier.\ have gen_S_orbits: "\ g x. g \ generate G S ==> x \ X ==> (x, (rho g) x) \ s" proof - fix g assume g_in_genS: "g \ generate G S" then show orbit_of_x: "\ x. x \ X ==> (x, (rho g) x) \ s" proof (induct g) case (one) (* \ x. x \ X ==> (x, rho (one G) x) \ s *) show "(x, rho (one G) x) \ s" proof - have "(x, rho (one G) x) = (x,x)" using rho_is_action group_action.id_eq_one[of G X rho, THEN sym] one by simp then show "(x, rho (one G) x) \ s" using s_eqrel equiv_def[of X s] refl_onD[of X s x] one by simp qed next case (incl) fix g assume "g \ S" then show "(x, (rho g) x) \ s" using s_def Phi_def G_is_group rho_is_action S_sub_G incl graphing_of_subset_contains_subsetaction[of G X rho S x g] by auto next case (inv) fix g assume g_in_S: "g \ S" then show "(x, (rho (m_inv G g)) x) \ s" proof - have g_in_G: "g \ carrier G" using g_in_S S_sub_G by auto define y where "y = (rho (m_inv G g)) x" have y_in_X: "y \ X" using group_action.element_image[of G X rho "m_inv G g" x y] rho_is_action y_def inv g_in_G G_is_group group.inv_closed[of G g] by simp have x_via_y: "(rho g) y = x" using G_is_group rho_is_action y_in_X inv y_def g_in_G group.inv_closed[of G g] group_action.composition_rule[of G X rho x g "m_inv G g", THEN sym] group.r_inv[of G g] group_action.id_eq_one[of G X rho, THEN sym] by auto have "(y, (rho g) y) \ s" using s_def Phi_def G_is_group rho_is_action S_sub_G g_in_S g_in_G y_in_X graphing_of_subset_contains_subsetaction[of G X rho S y g] by simp then have "((rho g) y, y) \ s" using s_eqrel equiv_def[of X s] sym_def[of s] by simp then show "(x, (rho (m_inv G g)) x) \ s" using x_via_y y_def by simp qed next case (eng g1 g2 x) then show "(x, rho (mult G g1 g2) x) \ s" proof - have g1_in_G: "g1 \ carrier G" and g2_in_G: "g2 \ carrier G" using eng G_is_group group.generate_in_carrier[of G S] S_sub_G by auto define y where "y = rho g2 x" have y_in_X: "y \ X" using group_action.element_image[of G X rho g2 x y] rho_is_action y_def eng g2_in_G G_is_group by simp then have x_via_y: "rho (mult G g1 g2) x = rho g1 y" using group_action.composition_rule[of G X rho x g1 g2] rho_is_action y_def g1_in_G g2_in_G eng by simp have "(x, y) \ s" and "(y, rho g1 y) \ s" using eng y_in_X y_def by auto then have "(x, rho g1 y) \ s" using s_eqrel equiv_def[of X s] trans_def[of s] by auto then show "(x, rho (mult G g1 g2) x) \ s" using x_via_y by simp qed qed qed text \Finally, we only need to the statement on orbits into a statement on pairs:\ have x_in_X: "x \ X" using r_def orbit_relation_def[of G X rho] Pair by auto from Pair obtain g where "g \ carrier G" and y_gx: "y = rho g x" using r_def orbit_relation_def[of G X rho] orbit_def[of G rho x] by auto then have "g \ generate G S" using S_gen_G by simp then have "(x, rho g x) \ s" using gen_S_orbits[of g x] x_in_X by simp then show "(x,y) \ s" using y_gx by auto qed qed show "r \ s" using r_sub_s by simp show "s \ r" using s_sub_r by simp qed end