(* Title: Product_GenSet.thy Author: Clara L\"oh *) theory Product_GenSet imports Complex_Main "HOL-Algebra.Generated_Groups" begin text \The rank of groups is subadditive with respect to taking product groups. As a preparation, we show in the following how generating sets of the factors can be combined into a generating set of the product group.\ text \The predicate checking if the given set is a finite generating set:\ definition is_fin_gen_set_of :: "('a,_) monoid_scheme => 'a set => bool" where "is_fin_gen_set_of G S = (S \ carrier G \ ((generate G S) = (carrier G)) \ (finite S))" lemma gen_sets_product: fixes G :: "('a, _) monoid_scheme" and H :: "('b, _) monoid_scheme" and S T ST assumes G_is_group: "group G" and H_is_group: "group H" and S_gen_G: "is_fin_gen_set_of G S" and T_gen_H: "is_fin_gen_set_of H T" and ST_def: "ST = { (g, one H) | g . g \ S} \ {(one G, h) | h . h \ T }" shows "is_fin_gen_set_of (DirProd G H) ST" unfolding is_fin_gen_set_of_def proof (intro conjI) (* Setup for the three groups G, H, and the product group *) interpret H: group H using H_is_group by simp interpret G: group G using G_is_group by simp define GH where "GH = DirProd G H" have GH_is_group: "group GH" using GH_def G_is_group H_is_group DirProd_group by auto interpret GH: group GH using GH_is_group GH_def by simp (* Some notation for the relevant generating sets *) define Se where "Se = { (g, one H) | g. g \ S }" define eT where "eT = { (one G, h) | h. h \ T }" have ST_Se_eT: "ST = Se \ eT" using ST_def Se_def eT_def by simp (* prelims on the canonical inclusions into the product*) define i_1 where "i_1 = (\ x :: 'a. (x, one H))" have "i_1 \ hom G GH" proof - have i_11: "fst o i_1 = id" using i_1_def by auto have i_12: "snd o i_1 = (\ x . one H)" using i_1_def by auto show ?thesis using hom_pairwise[of i_1 G G H] i_11 i_12 trivial_hom[of H G] id_iso[of G] iso_imp_homomorphism GH_def by auto qed then have i_1_hom: "group_hom G GH i_1" using G_is_group GH_is_group group_hom_axioms_def[of G GH i_1] group_hom_def by auto have Se_img_i_1: "Se = i_1 ` S" using Se_def i_1_def image_def by auto define i_2 where "i_2 = (\ x :: 'b. (one G, x))" have "i_2 \ hom H GH" proof - have i_21: "fst o i_2 = (\ x . one G)" using i_2_def by auto have i_22: "snd o i_2 = id" using i_2_def by auto show ?thesis using hom_pairwise[of i_2 H G H] i_21 i_22 trivial_hom[of G H] id_iso[of H] iso_imp_homomorphism GH_def by auto qed then have i_2_hom: "group_hom H GH i_2" using G_is_group GH_is_group group_hom_axioms_def[of H GH i_2] group_hom_def by auto have eT_img_i_2: "eT = i_2 ` T" using eT_def i_2_def image_def by auto text \We now check the three defining properties of finite generating sets:\ (* The set ST is finite *) show ST_finite: "finite ST" proof - have S_finite: "finite S" using S_gen_G is_fin_gen_set_of_def by auto have T_finite: "finite T" using T_gen_H is_fin_gen_set_of_def by auto have Se_finite: "finite Se" using Se_def Se_img_i_1 S_finite finite_imageI by auto have eT_finite: "finite eT" using eT_def eT_img_i_2 T_finite finite_imageI by auto show "finite ST" using ST_Se_eT Se_finite eT_finite finite_UnI by simp qed (* The set ST is a subset of the product G x H *) show ST_sub_GH: "ST \ carrier GH" proof - have S_sub_G: "S \ carrier G" using S_gen_G is_fin_gen_set_of_def[of G S] by simp have T_sub_H: "T \ carrier H" using T_gen_H is_fin_gen_set_of_def[of H T] by simp have Se_sub_GH: "Se \ carrier GH" proof fix x assume x_in_Se: "x \ Se" define g where "g = fst x" define h where "h = snd x" have g_in_G: "g \ carrier G" using g_def x_in_Se Se_def S_sub_G by auto have "h = one H" using h_def x_in_Se Se_def by auto then have h_in_H: "h \ carrier H" by auto (* using H_is_group monoid.one_closed by simp *) have "x = (g,h)" using g_def h_def prod_eqI by simp then have "x \ carrier G \ carrier H" using g_in_G h_in_H by simp then show "x \ carrier GH" using DirProd_def GH_def by simp qed have eT_sub_GH: "eT \ carrier GH" proof fix x assume x_in_eT: "x \ eT" define g where "g = fst x" define h where "h = snd x" have h_in_H: "h \ carrier H" using h_def x_in_eT eT_def T_sub_H by auto have "g = one G" using g_def x_in_eT eT_def by auto then have g_in_G: "g \ carrier G" by auto have "x = (g,h)" using g_def h_def prod_eqI by simp then show "x \ carrier GH" using g_in_G h_in_H DirProd_def GH_def by simp qed from Se_sub_GH eT_sub_GH show ?thesis using ST_Se_eT by simp qed (* The set ST generates the product G x H *) show "generate GH ST = carrier GH" proof show "generate GH ST \ carrier GH" using GH_def GH_is_group ST_sub_GH group.generate_incl[of "DirProd G H" ST] by simp show "carrier GH \ generate GH ST" proof fix x assume x_in_GH: "x \ carrier GH" define g where "g = fst x" define h where "h = snd x" have x_gh: "x = (g,h)" using g_def h_def prod_eqI by simp have g_in_G: "g \ carrier G" using g_def x_in_GH GH_def by auto have h_in_H: "h \ carrier H" using h_def x_in_GH GH_def by auto have g_in_genS: "g \ generate G S" using g_in_G S_gen_G is_fin_gen_set_of_def[of G S] by auto have h_in_genT: "h \ generate H T" using h_in_H T_gen_H is_fin_gen_set_of_def[of H T] by auto define Ge where "Ge = {(x, one H) | x . x \ carrier G }" have "Ge \ generate GH Se" proof - have "Ge = i_1 ` (carrier G)" using Ge_def i_1_def image_def by auto then show ?thesis using S_gen_G is_fin_gen_set_of_def[of G S] Se_img_i_1 i_1_hom group_hom.generate_img[of G GH i_1 S] by auto qed then have ge_in_genSe: "(g, one H) \ generate GH Se" using Ge_def g_in_G by auto then have ge_in_genSe: "(g, one H) \ generate GH ST" using group.mono_generate[of GH Se ST] ST_def Se_def by auto define eH where "eH = {(one G, x) | x . x \ carrier H }" have "eH \ generate GH eT" proof - have "eH = i_2 ` (carrier H)" using eH_def i_2_def image_def by auto then show ?thesis using T_gen_H is_fin_gen_set_of_def[of H T] eT_img_i_2 i_2_hom group_hom.generate_img[of H GH i_2 T] by auto qed then have eh_in_geneT: "(one G, h) \ generate GH eT" using eH_def h_in_H by auto then have eh_in_geneT: "(one G, h) \ generate GH ST" using group.mono_generate[of GH eT ST] ST_def eT_def by auto show "x \ generate GH ST" proof - have x_ge_eh: "x = mult GH (g, one H) (one G, h)" proof - have "x = (g,h)" using x_gh by simp also have "\ = (mult G g (one G), mult H (one H) h)" using monoid.r_one[of G g] monoid.l_one[of H h] g_in_G h_in_H by simp ultimately show "x = mult GH (g, one H) (one G, h)" using monoid.l_one[of H] monoid.r_one[of G] DirProd_def[of G H] GH_def by auto qed then show ?thesis using x_ge_eh ge_in_genSe eh_in_geneT eng[of "(g, one H)" GH ST "(one G, h)"] by auto qed qed qed qed end