(* Title: HOL/Algebra/Generated_Groups.thy Author: Paulo Emílio de Vilhena *) section ‹Generated Groups› theory Generated_Groups imports Group Coset begin subsection ‹Generated Groups› inductive_set generate :: "('a, 'b) monoid_scheme ⇒ 'a set ⇒ 'a set" for G and H where one: "𝟭⇘G⇙ ∈ generate G H" | incl: "h ∈ H ⟹ h ∈ generate G H" | inv: "h ∈ H ⟹ inv⇘G⇙ h ∈ generate G H" | eng: "h1 ∈ generate G H ⟹ h2 ∈ generate G H ⟹ h1 ⊗⇘G⇙ h2 ∈ generate G H" subsubsection ‹Basic Properties› lemma (in group) generate_consistent: assumes "K ⊆ H" "subgroup H G" shows "generate (G ⦇ carrier := H ⦈) K = generate G K" proof show "generate (G ⦇ carrier := H ⦈) K ⊆ generate G K" proof fix h assume "h ∈ generate (G ⦇ carrier := H ⦈) K" thus "h ∈ generate G K" proof (induction, simp add: one, simp_all add: incl[of _ K G] eng) case inv thus ?case using m_inv_consistent assms generate.inv[of _ K G] by auto qed qed next show "generate G K ⊆ generate (G ⦇ carrier := H ⦈) K" proof note gen_simps = one incl eng fix h assume "h ∈ generate G K" thus "h ∈ generate (G ⦇ carrier := H ⦈) K" using gen_simps[where ?G = "G ⦇ carrier := H ⦈"] proof (induction, auto) fix h assume "h ∈ K" thus "inv h ∈ generate (G ⦇ carrier := H ⦈) K" using m_inv_consistent assms generate.inv[of h K "G ⦇ carrier := H ⦈"] by auto qed qed qed lemma (in group) generate_in_carrier: assumes "H ⊆ carrier G" and "h ∈ generate G H" shows "h ∈ carrier G" using assms(2,1) by (induct h rule: generate.induct) (auto) lemma (in group) generate_incl: assumes "H ⊆ carrier G" shows "generate G H ⊆ carrier G" using generate_in_carrier[OF assms(1)] by auto lemma (in group) generate_m_inv_closed: assumes "H ⊆ carrier G" and "h ∈ generate G H" shows "(inv h) ∈ generate G H" using assms(2,1) proof (induction rule: generate.induct, auto simp add: one inv incl) fix h1 h2 assume h1: "h1 ∈ generate G H" "inv h1 ∈ generate G H" and h2: "h2 ∈ generate G H" "inv h2 ∈ generate G H" hence "inv (h1 ⊗ h2) = (inv h2) ⊗ (inv h1)" by (meson assms generate_in_carrier group.inv_mult_group is_group) thus "inv (h1 ⊗ h2) ∈ generate G H" using generate.eng[OF h2(2) h1(2)] by simp qed lemma (in group) generate_is_subgroup: assumes "H ⊆ carrier G" shows "subgroup (generate G H) G" using subgroup.intro[OF generate_incl eng one generate_m_inv_closed] assms by auto lemma (in group) mono_generate: assumes "K ⊆ H" shows "generate G K ⊆ generate G H" proof fix h assume "h ∈ generate G K" thus "h ∈ generate G H" using assms by (induction) (auto simp add: one incl inv eng) qed lemma (in group) generate_subgroup_incl: assumes "K ⊆ H" "subgroup H G" shows "generate G K ⊆ H" using group.generate_incl[OF subgroup_imp_group[OF assms(2)], of K] assms(1) by (simp add: generate_consistent[OF assms]) lemma (in group) generate_minimal: assumes "H ⊆ carrier G" shows "generate G H = ⋂ { H'. subgroup H' G ∧ H ⊆ H' }" using generate_subgroup_incl generate_is_subgroup[OF assms] incl[of _ H] by blast lemma (in group) generateI: assumes "subgroup E G" "H ⊆ E" and "⋀K. ⟦ subgroup K G; H ⊆ K ⟧ ⟹ E ⊆ K" shows "E = generate G H" proof - have subset: "H ⊆ carrier G" using subgroup.subset assms by auto show ?thesis using assms unfolding generate_minimal[OF subset] by blast qed lemma (in group) normal_generateI: assumes "H ⊆ carrier G" and "⋀h g. ⟦ h ∈ H; g ∈ carrier G ⟧ ⟹ g ⊗ h ⊗ (inv g) ∈ H" shows "generate G H ⊲ G" proof (rule normal_invI[OF generate_is_subgroup[OF assms(1)]]) fix g h assume g: "g ∈ carrier G" show "h ∈ generate G H ⟹ g ⊗ h ⊗ (inv g) ∈ generate G H" proof (induct h rule: generate.induct) case one thus ?case using g generate.one by auto next case incl show ?case using generate.incl[OF assms(2)[OF incl g]] . next case (inv h) hence h: "h ∈ carrier G" using assms(1) by auto hence "inv (g ⊗ h ⊗ (inv g)) = g ⊗ (inv h) ⊗ (inv g)" using g by (simp add: inv_mult_group m_assoc) thus ?case using generate_m_inv_closed[OF assms(1) generate.incl[OF assms(2)[OF inv g]]] by simp next case (eng h1 h2) note in_carrier = eng(1,3)[THEN generate_in_carrier[OF assms(1)]] have "g ⊗ (h1 ⊗ h2) ⊗ inv g = (g ⊗ h1 ⊗ inv g) ⊗ (g ⊗ h2 ⊗ inv g)" using in_carrier g by (simp add: inv_solve_left m_assoc) thus ?case using generate.eng[OF eng(2,4)] by simp qed qed lemma (in group) subgroup_int_pow_closed: assumes "subgroup H G" "h ∈ H" shows "h [^] (k :: int) ∈ H" using group.int_pow_closed[OF subgroup_imp_group[OF assms(1)]] assms(2) unfolding int_pow_consistent[OF assms] by simp lemma (in group) generate_pow: assumes "a ∈ carrier G" shows "generate G { a } = { a [^] (k :: int) | k. k ∈ UNIV }" proof show "{ a [^] (k :: int) | k. k ∈ UNIV } ⊆ generate G { a }" using subgroup_int_pow_closed[OF generate_is_subgroup[of "{ a }"] incl[of a]] assms by auto next show "generate G { a } ⊆ { a [^] (k :: int) | k. k ∈ UNIV }" proof fix h assume "h ∈ generate G { a }" hence "∃k :: int. h = a [^] k" proof (induction) case one then show ?case using int_pow_0 [of G] by metis next case (incl h) then show ?case by (metis assms int_pow_1 singletonD) next case (inv h) then show ?case by (metis assms int_pow_1 int_pow_neg singletonD) next case (eng h1 h2) then show ?case using assms by (metis int_pow_mult) qed then show "h ∈ { a [^] (k :: int) | k. k ∈ UNIV }" by blast qed qed corollary (in group) generate_one: "generate G { 𝟭 } = { 𝟭 }" using generate_pow[of "𝟭", OF one_closed] by simp corollary (in group) generate_empty: "generate G {} = { 𝟭 }" using mono_generate[of "{}" "{ 𝟭 }"] generate.one unfolding generate_one by auto lemma (in group_hom) "subgroup K G ⟹ subgroup (h ` K) H" using subgroup_img_is_subgroup by auto lemma (in group_hom) generate_img: assumes "K ⊆ carrier G" shows "generate H (h ` K) = h ` (generate G K)" proof have "h ` K ⊆ h ` (generate G K)" using incl[of _ K G] by auto thus "generate H (h ` K) ⊆ h ` (generate G K)" using generate_subgroup_incl subgroup_img_is_subgroup[OF G.generate_is_subgroup[OF assms]] by auto next show "h ` (generate G K) ⊆ generate H (h ` K)" proof fix a assume "a ∈ h ` (generate G K)" then obtain k where "k ∈ generate G K" "a = h k" by blast show "a ∈ generate H (h ` K)" using ‹k ∈ generate G K› unfolding ‹a = h k› proof (induct k, auto simp add: generate.one[of H] generate.incl[of _ "h ` K" H]) case (inv k) show ?case using assms generate.inv[of "h k" "h ` K" H] inv by auto next case eng show ?case using generate.eng[OF eng(2,4)] eng(1,3)[THEN G.generate_in_carrier[OF assms]] by auto qed qed qed subsection ‹Derived Subgroup› subsubsection ‹Definitions› abbreviation derived_set :: "('a, 'b) monoid_scheme ⇒ 'a set ⇒ 'a set" where "derived_set G H ≡ ⋃h1 ∈ H. (⋃h2 ∈ H. { h1 ⊗⇘G⇙ h2 ⊗⇘G⇙ (inv⇘G⇙ h1) ⊗⇘G⇙ (inv⇘G⇙ h2) })" definition derived :: "('a, 'b) monoid_scheme ⇒ 'a set ⇒ 'a set" where "derived G H = generate G (derived_set G H)" subsubsection ‹Basic Properties› lemma (in group) derived_set_incl: assumes "K ⊆ H" "subgroup H G" shows "derived_set G K ⊆ H" using assms(1) subgroupE(3-4)[OF assms(2)] by (auto simp add: subset_iff) lemma (in group) derived_incl: assumes "K ⊆ H" "subgroup H G" shows "derived G K ⊆ H" using generate_subgroup_incl[OF derived_set_incl] assms unfolding derived_def by auto lemma (in group) derived_set_in_carrier: assumes "H ⊆ carrier G" shows "derived_set G H ⊆ carrier G" using derived_set_incl[OF assms subgroup_self] . lemma (in group) derived_in_carrier: assumes "H ⊆ carrier G" shows "derived G H ⊆ carrier G" using derived_incl[OF assms subgroup_self] . lemma (in group) exp_of_derived_in_carrier: assumes "H ⊆ carrier G" shows "(derived G ^^ n) H ⊆ carrier G" using assms derived_in_carrier by (induct n) (auto) lemma (in group) derived_is_subgroup: assumes "H ⊆ carrier G" shows "subgroup (derived G H) G" unfolding derived_def using generate_is_subgroup[OF derived_set_in_carrier[OF assms]] . lemma (in group) exp_of_derived_is_subgroup: assumes "subgroup H G" shows "subgroup ((derived G ^^ n) H) G" using assms derived_is_subgroup subgroup.subset by (induct n) (auto) lemma (in group) exp_of_derived_is_subgroup': assumes "H ⊆ carrier G" shows "subgroup ((derived G ^^ (Suc n)) H) G" using assms derived_is_subgroup[OF subgroup.subset] derived_is_subgroup by (induct n) (auto) lemma (in group) mono_derived_set: assumes "K ⊆ H" shows "derived_set G K ⊆ derived_set G H" using assms by auto lemma (in group) mono_derived: assumes "K ⊆ H" shows "derived G K ⊆ derived G H" unfolding derived_def using mono_generate[OF mono_derived_set[OF assms]] . lemma (in group) mono_exp_of_derived: assumes "K ⊆ H" shows "(derived G ^^ n) K ⊆ (derived G ^^ n) H" using assms mono_derived by (induct n) (auto) lemma (in group) derived_set_consistent: assumes "K ⊆ H" "subgroup H G" shows "derived_set (G ⦇ carrier := H ⦈) K = derived_set G K" using m_inv_consistent[OF assms(2)] assms(1) by (auto simp add: subset_iff) lemma (in group) derived_consistent: assumes "K ⊆ H" "subgroup H G" shows "derived (G ⦇ carrier := H ⦈) K = derived G K" using generate_consistent[OF derived_set_incl] derived_set_consistent assms by (simp add: derived_def) lemma (in comm_group) derived_eq_singleton: assumes "H ⊆ carrier G" shows "derived G H = { 𝟭 }" proof (cases "derived_set G H = {}") case True show ?thesis using generate_empty unfolding derived_def True by simp next case False have aux_lemma: "h ∈ derived_set G H ⟹ h = 𝟭" for h using assms by (auto simp add: subset_iff) (metis (no_types, lifting) m_comm m_closed inv_closed inv_solve_right l_inv l_inv_ex) have "derived_set G H = { 𝟭 }" proof show "derived_set G H ⊆ { 𝟭 }" using aux_lemma by auto next obtain h where h: "h ∈ derived_set G H" using False by blast thus "{ 𝟭 } ⊆ derived_set G H" using aux_lemma[OF h] by auto qed thus ?thesis using generate_one unfolding derived_def by auto qed lemma (in group) derived_is_normal: assumes "H ⊲ G" shows "derived G H ⊲ G" proof - interpret H: normal H G using assms . show ?thesis unfolding derived_def proof (rule normal_generateI[OF derived_set_in_carrier[OF H.subset]]) fix h g assume "h ∈ derived_set G H" and g: "g ∈ carrier G" then obtain h1 h2 where h: "h1 ∈ H" "h2 ∈ H" "h = h1 ⊗ h2 ⊗ inv h1 ⊗ inv h2" by auto hence in_carrier: "h1 ∈ carrier G" "h2 ∈ carrier G" "g ∈ carrier G" using H.subset g by auto have "g ⊗ h ⊗ inv g = g ⊗ h1 ⊗ (inv g ⊗ g) ⊗ h2 ⊗ (inv g ⊗ g) ⊗ inv h1 ⊗ (inv g ⊗ g) ⊗ inv h2 ⊗ inv g" unfolding h(3) by (simp add: in_carrier m_assoc) also have " ... = (g ⊗ h1 ⊗ inv g) ⊗ (g ⊗ h2 ⊗ inv g) ⊗ (g ⊗ inv h1 ⊗ inv g) ⊗ (g ⊗ inv h2 ⊗ inv g)" using in_carrier m_assoc inv_closed m_closed by presburger finally have "g ⊗ h ⊗ inv g = (g ⊗ h1 ⊗ inv g) ⊗ (g ⊗ h2 ⊗ inv g) ⊗ inv (g ⊗ h1 ⊗ inv g) ⊗ inv (g ⊗ h2 ⊗ inv g)" by (simp add: in_carrier inv_mult_group m_assoc) thus "g ⊗ h ⊗ inv g ∈ derived_set G H" using h(1-2)[THEN H.inv_op_closed2[OF g]] by auto qed qed lemma (in group) normal_self: "carrier G ⊲ G" by (rule normal_invI[OF subgroup_self], simp) corollary (in group) derived_self_is_normal: "derived G (carrier G) ⊲ G" using derived_is_normal[OF normal_self] . corollary (in group) derived_subgroup_is_normal: assumes "subgroup H G" shows "derived G H ⊲ G ⦇ carrier := H ⦈" using group.derived_self_is_normal[OF subgroup_imp_group[OF assms]] derived_consistent[OF _ assms] by simp corollary (in group) derived_quot_is_group: "group (G Mod (derived G (carrier G)))" using normal.factorgroup_is_group[OF derived_self_is_normal] by auto lemma (in group) derived_quot_is_comm_group: "comm_group (G Mod (derived G (carrier G)))" proof (rule group.group_comm_groupI[OF derived_quot_is_group], simp add: FactGroup_def) interpret DG: normal "derived G (carrier G)" G using derived_self_is_normal . fix H K assume "H ∈ rcosets derived G (carrier G)" and "K ∈ rcosets derived G (carrier G)" then obtain g1 g2 where g1: "g1 ∈ carrier G" "H = derived G (carrier G) #> g1" and g2: "g2 ∈ carrier G" "K = derived G (carrier G) #> g2" unfolding RCOSETS_def by auto hence "H <#> K = derived G (carrier G) #> (g1 ⊗ g2)" by (simp add: DG.rcos_sum) also have " ... = derived G (carrier G) #> (g2 ⊗ g1)" proof - { fix g1 g2 assume g1: "g1 ∈ carrier G" and g2: "g2 ∈ carrier G" have "derived G (carrier G) #> (g1 ⊗ g2) ⊆ derived G (carrier G) #> (g2 ⊗ g1)" proof fix h assume "h ∈ derived G (carrier G) #> (g1 ⊗ g2)" then obtain g' where h: "g' ∈ carrier G" "g' ∈ derived G (carrier G)" "h = g' ⊗ (g1 ⊗ g2)" using DG.subset unfolding r_coset_def by auto hence "h = g' ⊗ (g1 ⊗ g2) ⊗ (inv g1 ⊗ inv g2 ⊗ g2 ⊗ g1)" using g1 g2 by (simp add: m_assoc) hence "h = (g' ⊗ (g1 ⊗ g2 ⊗ inv g1 ⊗ inv g2)) ⊗ (g2 ⊗ g1)" using h(1) g1 g2 inv_closed m_assoc m_closed by presburger moreover have "g1 ⊗ g2 ⊗ inv g1 ⊗ inv g2 ∈ derived G (carrier G)" using incl[of _ "derived_set G (carrier G)"] g1 g2 unfolding derived_def by blast hence "g' ⊗ (g1 ⊗ g2 ⊗ inv g1 ⊗ inv g2) ∈ derived G (carrier G)" using DG.m_closed[OF h(2)] by simp ultimately show "h ∈ derived G (carrier G) #> (g2 ⊗ g1)" unfolding r_coset_def by blast qed } thus ?thesis using g1(1) g2(1) by auto qed also have " ... = K <#> H" by (simp add: g1 g2 DG.rcos_sum) finally show "H <#> K = K <#> H" . qed corollary (in group) derived_quot_of_subgroup_is_comm_group: assumes "subgroup H G" shows "comm_group ((G ⦇ carrier := H ⦈) Mod (derived G H))" using group.derived_quot_is_comm_group[OF subgroup_imp_group[OF assms]] derived_consistent[OF _ assms] by simp proposition (in group) derived_minimal: assumes "H ⊲ G" and "comm_group (G Mod H)" shows "derived G (carrier G) ⊆ H" proof - interpret H: normal H G using assms(1) . show ?thesis unfolding derived_def proof (rule generate_subgroup_incl[OF _ H.subgroup_axioms]) show "derived_set G (carrier G) ⊆ H" proof fix h assume "h ∈ derived_set G (carrier G)" then obtain g1 g2 where h: "g1 ∈ carrier G" "g2 ∈ carrier G" "h = g1 ⊗ g2 ⊗ inv g1 ⊗ inv g2" by auto have "H #> (g1 ⊗ g2) = (H #> g1) <#> (H #> g2)" by (simp add: h(1-2) H.rcos_sum) also have " ... = (H #> g2) <#> (H #> g1)" using comm_groupE(4)[OF assms(2)] h(1-2) unfolding FactGroup_def RCOSETS_def by auto also have " ... = H #> (g2 ⊗ g1)" by (simp add: h(1-2) H.rcos_sum) finally have "H #> (g1 ⊗ g2) = H #> (g2 ⊗ g1)" . then obtain h' where "h' ∈ H" "𝟭 ⊗ (g1 ⊗ g2) = h' ⊗ (g2 ⊗ g1)" using H.one_closed unfolding r_coset_def by blast thus "h ∈ H" using h m_assoc by auto qed qed qed proposition (in group) derived_of_subgroup_minimal: assumes "K ⊲ G ⦇ carrier := H ⦈" "subgroup H G" and "comm_group ((G ⦇ carrier := H ⦈) Mod K)" shows "derived G H ⊆ K" using group.derived_minimal[OF subgroup_imp_group[OF assms(2)] assms(1,3)] derived_consistent[OF _ assms(2)] by simp lemma (in group_hom) derived_img: assumes "K ⊆ carrier G" shows "derived H (h ` K) = h ` (derived G K)" proof - have "derived_set H (h ` K) = h ` (derived_set G K)" proof show "derived_set H (h ` K) ⊆ h ` derived_set G K" proof fix a assume "a ∈ derived_set H (h ` K)" then obtain k1 k2 where "k1 ∈ K" "k2 ∈ K" "a = (h k1) ⊗⇘H⇙ (h k2) ⊗⇘H⇙ inv⇘H⇙ (h k1) ⊗⇘H⇙ inv⇘H⇙ (h k2)" by auto hence "a = h (k1 ⊗ k2 ⊗ inv k1 ⊗ inv k2)" using assms by (simp add: subset_iff) from this ‹k1 ∈ K› and ‹k2 ∈ K› show "a ∈ h ` derived_set G K" by auto qed next show "h ` (derived_set G K) ⊆ derived_set H (h ` K)" proof fix a assume "a ∈ h ` (derived_set G K)" then obtain k1 k2 where "k1 ∈ K" "k2 ∈ K" "a = h (k1 ⊗ k2 ⊗ inv k1 ⊗ inv k2)" by auto hence "a = (h k1) ⊗⇘H⇙ (h k2) ⊗⇘H⇙ inv⇘H⇙ (h k1) ⊗⇘H⇙ inv⇘H⇙ (h k2)" using assms by (simp add: subset_iff) from this ‹k1 ∈ K› and ‹k2 ∈ K› show "a ∈ derived_set H (h ` K)" by auto qed qed thus ?thesis unfolding derived_def using generate_img[OF G.derived_set_in_carrier[OF assms]] by simp qed lemma (in group_hom) exp_of_derived_img: assumes "K ⊆ carrier G" shows "(derived H ^^ n) (h ` K) = h ` ((derived G ^^ n) K)" using derived_img[OF G.exp_of_derived_in_carrier[OF assms]] by (induct n) (auto) subsubsection ‹Generated subgroup of a group› definition subgroup_generated :: "('a, 'b) monoid_scheme ⇒ 'a set ⇒ ('a, 'b) monoid_scheme" where "subgroup_generated G S = G⦇carrier := generate G (carrier G ∩ S)⦈" lemma carrier_subgroup_generated: "carrier (subgroup_generated G S) = generate G (carrier G ∩ S)" by (auto simp: subgroup_generated_def) lemma (in group) subgroup_generated_subset_carrier_subset: "S ⊆ carrier G ⟹ S ⊆ carrier(subgroup_generated G S)" by (simp add: Int_absorb1 carrier_subgroup_generated generate.incl subsetI) lemma (in group) subgroup_generated_minimal: "⟦subgroup H G; S ⊆ H⟧ ⟹ carrier(subgroup_generated G S) ⊆ H" by (simp add: carrier_subgroup_generated generate_subgroup_incl le_infI2) lemma (in group) carrier_subgroup_generated_subset: "carrier (subgroup_generated G A) ⊆ carrier G" apply (clarsimp simp: carrier_subgroup_generated) by (meson Int_lower1 generate_in_carrier) lemma (in group) group_subgroup_generated [simp]: "group (subgroup_generated G S)" unfolding subgroup_generated_def by (simp add: generate_is_subgroup subgroup_imp_group) lemma (in group) abelian_subgroup_generated: assumes "comm_group G" shows "comm_group (subgroup_generated G S)" (is "comm_group ?GS") proof (rule group.group_comm_groupI) show "Group.group ?GS" by simp next fix x y assume "x ∈ carrier ?GS" "y ∈ carrier ?GS" with assms show "x ⊗⇘?GS⇙ y = y ⊗⇘?GS⇙ x" apply (simp add: subgroup_generated_def) by (meson Int_lower1 comm_groupE(4) generate_in_carrier) qed lemma (in group) subgroup_of_subgroup_generated: assumes "H ⊆ B" "subgroup H G" shows "subgroup H (subgroup_generated G B)" proof unfold_locales fix x assume "x ∈ H" with assms show "inv⇘subgroup_generated G B⇙ x ∈ H" unfolding subgroup_generated_def by (metis IntI Int_commute Int_lower2 generate.incl generate_is_subgroup m_inv_consistent subgroup_def subsetCE) next show "H ⊆ carrier (subgroup_generated G B)" using assms apply (auto simp: carrier_subgroup_generated) by (metis Int_iff generate.incl inf.orderE subgroup.mem_carrier) qed (use assms in ‹auto simp: subgroup_generated_def subgroup_def›) lemma carrier_subgroup_generated_alt: assumes "Group.group G" "S ⊆ carrier G" shows "carrier (subgroup_generated G S) = ⋂{H. subgroup H G ∧ carrier G ∩ S ⊆ H}" using assms by (auto simp: group.generate_minimal subgroup_generated_def) lemma one_subgroup_generated [simp]: "𝟭⇘subgroup_generated G S⇙ = 𝟭⇘G⇙" by (auto simp: subgroup_generated_def) lemma mult_subgroup_generated [simp]: "mult (subgroup_generated G S) = mult G" by (auto simp: subgroup_generated_def) lemma (in group) inv_subgroup_generated [simp]: assumes "f ∈ carrier (subgroup_generated G S)" shows "inv⇘subgroup_generated G S⇙ f = inv f" proof (rule group.inv_equality) show "Group.group (subgroup_generated G S)" by simp have [simp]: "f ∈ carrier G" by (metis Int_lower1 assms carrier_subgroup_generated generate_in_carrier) show "inv f ⊗⇘subgroup_generated G S⇙ f = 𝟭⇘subgroup_generated G S⇙" by (simp add: assms) show "f ∈ carrier (subgroup_generated G S)" using assms by (simp add: generate.incl subgroup_generated_def) show "inv f ∈ carrier (subgroup_generated G S)" using assms by (simp add: subgroup_generated_def generate_m_inv_closed) qed lemma subgroup_generated_restrict [simp]: "subgroup_generated G (carrier G ∩ S) = subgroup_generated G S" by (simp add: subgroup_generated_def) lemma (in subgroup) carrier_subgroup_generated_subgroup [simp]: "carrier (subgroup_generated G H) = H" by (auto simp: generate.incl carrier_subgroup_generated elim: generate.induct) lemma (in group) subgroup_subgroup_generated_iff: "subgroup H (subgroup_generated G B) ⟷ subgroup H G ∧ H ⊆ carrier(subgroup_generated G B)" (is "?lhs = ?rhs") proof assume L: ?lhs then have Hsub: "H ⊆ generate G (carrier G ∩ B)" by (simp add: subgroup_def subgroup_generated_def) then have H: "H ⊆ carrier G" "H ⊆ carrier(subgroup_generated G B)" unfolding carrier_subgroup_generated using generate_incl by blast+ with Hsub have "subgroup H G" by (metis Int_commute Int_lower2 L carrier_subgroup_generated generate_consistent generate_is_subgroup inf.orderE subgroup.carrier_subgroup_generated_subgroup subgroup_generated_def) with H show ?rhs by blast next assume ?rhs then show ?lhs by (simp add: generate_is_subgroup subgroup_generated_def subgroup_incl) qed lemma (in group) subgroup_subgroup_generated: "subgroup (carrier(subgroup_generated G S)) G" using group.subgroup_self group_subgroup_generated subgroup_subgroup_generated_iff by blast lemma pow_subgroup_generated: "pow (subgroup_generated G S) = (pow G :: 'a ⇒ nat ⇒ 'a)" proof - have "x [^]⇘subgroup_generated G S⇙ n = x [^]⇘G⇙ n" for x and n::nat by (induction n) auto then show ?thesis by force qed lemma (in group) subgroup_generated2 [simp]: "subgroup_generated (subgroup_generated G S) S = subgroup_generated G S" proof - have *: "⋀A. carrier G ∩ A ⊆ carrier (subgroup_generated (subgroup_generated G A) A)" by (metis (no_types, opaque_lifting) Int_assoc carrier_subgroup_generated generate.incl inf.order_iff subset_iff) show ?thesis apply (auto intro!: monoid.equality) using group.carrier_subgroup_generated_subset group_subgroup_generated apply blast apply (metis (no_types, opaque_lifting) "*" group.subgroup_subgroup_generated group_subgroup_generated subgroup_generated_minimal subgroup_generated_restrict subgroup_subgroup_generated_iff subset_eq) apply (simp add: subgroup_generated_def) done qed lemma (in group) int_pow_subgroup_generated: fixes n::int assumes "x ∈ carrier (subgroup_generated G S)" shows "x [^]⇘subgroup_generated G S⇙ n = x [^]⇘G⇙ n" proof - have "x [^] nat (- n) ∈ carrier (subgroup_generated G S)" by (metis assms group.is_monoid group_subgroup_generated monoid.nat_pow_closed pow_subgroup_generated) then show ?thesis by (metis group.inv_subgroup_generated int_pow_def2 is_group pow_subgroup_generated) qed lemma kernel_from_subgroup_generated [simp]: "subgroup S G ⟹ kernel (subgroup_generated G S) H f = kernel G H f ∩ S" using subgroup.carrier_subgroup_generated_subgroup subgroup.subset by (fastforce simp add: kernel_def set_eq_iff) lemma kernel_to_subgroup_generated [simp]: "kernel G (subgroup_generated H S) f = kernel G H f" by (simp add: kernel_def) subsection ‹And homomorphisms› lemma (in group) hom_from_subgroup_generated: "h ∈ hom G H ⟹ h ∈ hom(subgroup_generated G A) H" apply (simp add: hom_def carrier_subgroup_generated Pi_iff) apply (metis group.generate_in_carrier inf_le1 is_group) done lemma hom_into_subgroup: "⟦h ∈ hom G G'; h ` (carrier G) ⊆ H⟧ ⟹ h ∈ hom G (subgroup_generated G' H)" by (auto simp: hom_def carrier_subgroup_generated Pi_iff generate.incl image_subset_iff) lemma hom_into_subgroup_eq_gen: "group G ⟹ h ∈ hom K (subgroup_generated G H) ⟷ h ∈ hom K G ∧ h ` (carrier K) ⊆ carrier(subgroup_generated G H)" using group.carrier_subgroup_generated_subset [of G H] by (auto simp: hom_def) lemma hom_into_subgroup_eq: "⟦subgroup H G; group G⟧ ⟹ (h ∈ hom K (subgroup_generated G H) ⟷ h ∈ hom K G ∧ h ` (carrier K) ⊆ H)" by (simp add: hom_into_subgroup_eq_gen image_subset_iff subgroup.carrier_subgroup_generated_subgroup) lemma (in group_hom) hom_between_subgroups: assumes "h ` A ⊆ B" shows "h ∈ hom (subgroup_generated G A) (subgroup_generated H B)" proof - have [simp]: "group G" "group H" by (simp_all add: G.is_group H.is_group) have "x ∈ generate G (carrier G ∩ A) ⟹ h x ∈ generate H (carrier H ∩ B)" for x proof (induction x rule: generate.induct) case (incl h) then show ?case by (meson IntE IntI assms generate.incl hom_closed image_subset_iff) next case (inv h) then show ?case by (metis G.inv_closed G.inv_inv IntE IntI assms generate.simps hom_inv image_subset_iff local.inv_closed) next case (eng h1 h2) then show ?case by (metis G.generate_in_carrier generate.simps inf.cobounded1 local.hom_mult) qed (auto simp: generate.intros) then have "h ` carrier (subgroup_generated G A) ⊆ carrier (subgroup_generated H B)" using group.carrier_subgroup_generated_subset [of G A] by (auto simp: carrier_subgroup_generated) then show ?thesis by (simp add: hom_into_subgroup_eq_gen group.hom_from_subgroup_generated homh) qed lemma (in group_hom) subgroup_generated_by_image: assumes "S ⊆ carrier G" shows "carrier (subgroup_generated H (h ` S)) = h ` (carrier(subgroup_generated G S))" proof have "x ∈ generate H (carrier H ∩ h ` S) ⟹ x ∈ h ` generate G (carrier G ∩ S)" for x proof (erule generate.induct) show "𝟭⇘H⇙ ∈ h ` generate G (carrier G ∩ S)" using generate.one by force next fix f assume "f ∈ carrier H ∩ h ` S" with assms show "f ∈ h ` generate G (carrier G ∩ S)" "inv⇘H⇙ f ∈ h ` generate G (carrier G ∩ S)" apply (auto simp: Int_absorb1 generate.incl) apply (metis generate.simps hom_inv imageI subsetCE) done next fix h1 h2 assume "h1 ∈ generate H (carrier H ∩ h ` S)" "h1 ∈ h ` generate G (carrier G ∩ S)" "h2 ∈ generate H (carrier H ∩ h ` S)" "h2 ∈ h ` generate G (carrier G ∩ S)" then show "h1 ⊗⇘H⇙ h2 ∈ h ` generate G (carrier G ∩ S)" using H.subgroupE(4) group.generate_is_subgroup subgroup_img_is_subgroup by (simp add: G.generate_is_subgroup) qed then show "carrier (subgroup_generated H (h ` S)) ⊆ h ` carrier (subgroup_generated G S)" by (auto simp: carrier_subgroup_generated) next have "h ` S ⊆ carrier H" by (metis (no_types) assms hom_closed image_subset_iff subsetCE) then show "h ` carrier (subgroup_generated G S) ⊆ carrier (subgroup_generated H (h ` S))" apply (clarsimp simp: carrier_subgroup_generated) by (metis Int_absorb1 assms generate_img imageI) qed lemma (in group_hom) iso_between_subgroups: assumes "h ∈ iso G H" "S ⊆ carrier G" "h ` S = T" shows "h ∈ iso (subgroup_generated G S) (subgroup_generated H T)" using assms by (metis G.carrier_subgroup_generated_subset Group.iso_iff hom_between_subgroups inj_on_subset subgroup_generated_by_image subsetI) lemma (in group) subgroup_generated_group_carrier: "subgroup_generated G (carrier G) = G" proof (rule monoid.equality) show "carrier (subgroup_generated G (carrier G)) = carrier G" by (simp add: subgroup.carrier_subgroup_generated_subgroup subgroup_self) qed (auto simp: subgroup_generated_def) lemma iso_onto_image: assumes "group G" "group H" shows "f ∈ iso G (subgroup_generated H (f ` carrier G)) ⟷ f ∈ hom G H ∧ inj_on f (carrier G)" using assms apply (auto simp: iso_def bij_betw_def hom_into_subgroup_eq_gen carrier_subgroup_generated hom_carrier generate.incl Int_absorb1 Int_absorb2) by (metis group.generateI group.subgroupE(1) group.subgroup_self group_hom.generate_img group_hom.intro group_hom_axioms.intro) lemma (in group) iso_onto_image: "group H ⟹ f ∈ iso G (subgroup_generated H (f ` carrier G)) ⟷ f ∈ mon G H" by (simp add: mon_def epi_def hom_into_subgroup_eq_gen iso_onto_image) end