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