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