(* Title: HOL/Algebra/Generated_Groups.thy
Author: Paulo EmÃlio de Vilhena
*)
theory Generated_Groups
imports Group Coset
begin
section\<open>Generated Groups\<close>
inductive_set
generate :: "('a, 'b) monoid_scheme \<Rightarrow> 'a set \<Rightarrow> 'a set"
for G and H where
one: "\<one>\<^bsub>G\<^esub> \<in> generate G H"
| incl: "h \<in> H \<Longrightarrow> h \<in> generate G H"
| inv: "h \<in> H \<Longrightarrow> inv\<^bsub>G\<^esub> h \<in> generate G H"
| eng: "h1 \<in> generate G H \<Longrightarrow> h2 \<in> generate G H \<Longrightarrow> h1 \<otimes>\<^bsub>G\<^esub> h2 \<in> generate G H"
subsection\<open>Basic Properties of Generated Groups - First Part\<close>
lemma (in group) generate_in_carrier:
assumes "H \<subseteq> carrier G"
shows "h \<in> generate G H \<Longrightarrow> h \<in> carrier G"
apply (induction rule: generate.induct) using assms by blast+
lemma (in group) generate_m_inv_closed:
assumes "H \<subseteq> carrier G"
shows "h \<in> generate G H \<Longrightarrow> (inv h) \<in> generate G H"
proof (induction rule: generate.induct)
case one thus ?case by (simp add: generate.one)
next
case (incl h) thus ?case using generate.inv[OF incl(1), of G] by simp
next
case (inv h) thus ?case using assms generate.incl by fastforce
next
case (eng h1 h2)
hence "inv (h1 \<otimes> h2) = (inv h2) \<otimes> (inv h1)"
by (meson assms generate_in_carrier group.inv_mult_group is_group)
thus ?case using generate.eng[OF eng(4) eng(3)] by simp
qed
lemma (in group) generate_is_subgroup:
assumes "H \<subseteq> carrier G"
shows "subgroup (generate G H) G"
proof (intro subgroupI)
show "generate G H \<subseteq> carrier G" using generate_in_carrier[OF assms] by blast
show "generate G H \<noteq> {}" using generate.one by auto
show "\<And>h. h \<in> generate G H \<Longrightarrow> inv h \<in> generate G H"
using generate_m_inv_closed[OF assms] by blast
show "\<And>h1 h2. \<lbrakk> h1 \<in> generate G H; h2 \<in> generate G H \<rbrakk> \<Longrightarrow> h1 \<otimes> h2 \<in> generate G H"
by (simp add: generate.eng)
qed
subsection\<open>Characterisations of Generated Groups\<close>
lemma (in group) generate_min_subgroup1:
assumes "H \<subseteq> carrier G"
and "subgroup E G" "H \<subseteq> E"
shows "generate G H \<subseteq> E"
proof
fix h show "h \<in> generate G H \<Longrightarrow> h \<in> E"
proof (induct rule: generate.induct)
case one thus ?case using subgroup.one_closed[OF assms(2)] by simp
case incl thus ?case using assms(3) by blast
case inv thus ?case using subgroup.m_inv_closed[OF assms(2)] assms(3) by blast
next
case eng thus ?case using subgroup.m_closed[OF assms(2)] by simp
qed
qed
lemma (in group) generateI:
assumes "H \<subseteq> carrier G"
and "subgroup E G" "H \<subseteq> E"
and "\<And>K. \<lbrakk> subgroup K G; H \<subseteq> K \<rbrakk> \<Longrightarrow> E \<subseteq> K"
shows "E = generate G H"
proof
show "E \<subseteq> generate G H"
using assms generate_is_subgroup generate.incl by (metis subset_iff)
show "generate G H \<subseteq> E"
using generate_min_subgroup1[OF assms(1-3)] by simp
qed
lemma (in group) generateE:
assumes "H \<subseteq> carrier G" and "E = generate G H"
shows "subgroup E G" and "H \<subseteq> E" and "\<And>K. \<lbrakk> subgroup K G; H \<subseteq> K \<rbrakk> \<Longrightarrow> E \<subseteq> K"
proof -
show "subgroup E G" using assms generate_is_subgroup by simp
show "H \<subseteq> E" using assms(2) by (simp add: generate.incl subsetI)
show "\<And>K. subgroup K G \<Longrightarrow> H \<subseteq> K \<Longrightarrow> E \<subseteq> K"
using assms generate_min_subgroup1 by auto
qed
lemma (in group) generate_min_subgroup2:
assumes "H \<subseteq> carrier G"
shows "generate G H = \<Inter>{K. subgroup K G \<and> H \<subseteq> K}"
proof
have "subgroup (generate G H) G \<and> H \<subseteq> generate G H"
by (simp add: assms generateE(2) generate_is_subgroup)
thus "\<Inter>{K. subgroup K G \<and> H \<subseteq> K} \<subseteq> generate G H" by blast
next
have "\<And>K. subgroup K G \<and> H \<subseteq> K \<Longrightarrow> generate G H \<subseteq> K"
by (simp add: assms generate_min_subgroup1)
thus "generate G H \<subseteq> \<Inter>{K. subgroup K G \<and> H \<subseteq> K}" by blast
qed
subsection\<open>Representation of Elements from a Generated Group\<close>
text\<open>We define a sort of syntax tree to allow induction arguments with elements of a generated group\<close>
datatype 'a repr =
One | Inv "'a" | Leaf "'a" | Mult "'a repr" "'a repr"
fun norm :: "('a, 'b) monoid_scheme \<Rightarrow> 'a repr \<Rightarrow> 'a"
where
"norm G (One) = \<one>\<^bsub>G\<^esub>"
| "norm G (Inv h) = (inv\<^bsub>G\<^esub> h)"
| "norm G (Leaf h) = h"
| "norm G (Mult h1 h2) = (norm G h1) \<otimes>\<^bsub>G\<^esub> (norm G h2)"
fun elts :: "'a repr \<Rightarrow> 'a set"
where
"elts (One) = {}"
| "elts (Inv h) = { h }"
| "elts (Leaf h) = { h }"
| "elts (Mult h1 h2) = (elts h1) \<union> (elts h2)"
lemma (in group) generate_repr_iff:
assumes "H \<subseteq> carrier G"
shows "(h \<in> generate G H) \<longleftrightarrow> (\<exists>r. (elts r) \<subseteq> H \<and> norm G r = h)"
proof
show "h \<in> generate G H \<Longrightarrow> \<exists>r. (elts r) \<subseteq> H \<and> norm G r = h"
proof (induction rule: generate.induct)
case one thus ?case
using elts.simps(1) norm.simps(1)[of G] by fastforce
next
case (incl h)
hence "elts (Leaf h) \<subseteq> H \<and> norm G (Leaf h) = h" by simp
thus ?case by blast
next
case (inv h)
hence "elts (Inv h) \<subseteq> H \<and> norm G (Inv h) = inv h" by auto
thus ?case by blast
next
case (eng h1 h2)
then obtain r1 r2 where r1: "elts r1 \<subseteq> H" "norm G r1 = h1"
and r2: "elts r2 \<subseteq> H" "norm G r2 = h2" by blast
hence "elts (Mult r1 r2) \<subseteq> H \<and> norm G (Mult r1 r2) = h1 \<otimes> h2" by simp
thus ?case by blast
qed
show "\<exists>r. elts r \<subseteq> H \<and> norm G r = h \<Longrightarrow> h \<in> generate G H"
proof -
assume "\<exists>r. elts r \<subseteq> H \<and> norm G r = h"
then obtain r where "elts r \<subseteq> H" "norm G r = h" by blast
thus "h \<in> generate G H"
proof (induction arbitrary: h rule: repr.induct)
case One thus ?case using generate.one by auto
next
case Inv thus ?case using generate.simps by force
next
case Leaf thus ?case using generate.simps by force
next
case Mult thus ?case using generate.eng by fastforce
qed
qed
qed
corollary (in group) generate_repr_set:
assumes "H \<subseteq> carrier G"
shows "generate G H = {norm G r | r. (elts r) \<subseteq> H}" (is "?A = ?B")
proof
show "?A \<subseteq> ?B"
proof
fix h assume "h \<in> generate G H" thus "h \<in> {norm G r |r. elts r \<subseteq> H}"
using generate_repr_iff[OF assms] by auto
qed
next
show "?B \<subseteq> ?A"
proof
fix h assume "h \<in> {norm G r |r. elts r \<subseteq> H}" thus "h \<in> generate G H"
using generate_repr_iff[OF assms] by auto
qed
qed
corollary (in group) mono_generate:
assumes "I \<subseteq> J" and "J \<subseteq> carrier G"
shows "generate G I \<subseteq> generate G J"
using assms generate_repr_iff by fastforce
lemma (in group) subgroup_gen_equality:
assumes "subgroup H G" "K \<subseteq> H"
shows "generate G K = generate (G \<lparr> carrier := H \<rparr>) K"
proof -
have "generate G K \<subseteq> H"
by (meson assms generate_min_subgroup1 order.trans subgroup.subset)
have mult_eq: "\<And>k1 k2. \<lbrakk> k1 \<in> generate G K; k2 \<in> generate G K \<rbrakk> \<Longrightarrow>
k1 \<otimes>\<^bsub>G \<lparr> carrier := H \<rparr>\<^esub> k2 = k1 \<otimes> k2"
using \<open>generate G K \<subseteq> H\<close> subgroup_mult_equality by simp
{ fix r assume A: "elts r \<subseteq> K"
hence "norm G r = norm (G \<lparr> carrier := H \<rparr>) r"
proof (induction r rule: repr.induct)
case One thus ?case by simp
next
case (Inv k) hence "k \<in> K" using A by simp
thus ?case using m_inv_consistent[OF assms(1)] assms(2) by auto
next
case (Leaf k) hence "k \<in> K" using A by simp
thus ?case using m_inv_consistent[OF assms(1)] assms(2) by auto
next
case (Mult k1 k2) thus ?case using mult_eq by auto
qed } note aux_lemma = this
show ?thesis
proof
show "generate G K \<subseteq> generate (G\<lparr>carrier := H\<rparr>) K"
proof
fix h assume "h \<in> generate G K" then obtain r where r: "elts r \<subseteq> K" "h = norm G r"
using generate_repr_iff assms by (metis order.trans subgroup.subset)
hence "h = norm (G \<lparr> carrier := H \<rparr>) r" using aux_lemma by simp
thus "h \<in> generate (G\<lparr>carrier := H\<rparr>) K"
using r assms group.generate_repr_iff [of "G \<lparr> carrier := H \<rparr>" K]
subgroup.subgroup_is_group[OF assms(1) is_group] by auto
qed
show "generate (G\<lparr>carrier := H\<rparr>) K \<subseteq> generate G K"
proof
fix h assume "h \<in> generate (G\<lparr>carrier := H\<rparr>) K"
then obtain r where r: "elts r \<subseteq> K" "h = norm (G\<lparr>carrier := H\<rparr>) r"
using group.generate_repr_iff [of "G \<lparr> carrier := H \<rparr>" K]
subgroup.subgroup_is_group[OF assms(1) is_group] assms by auto
hence "h = norm G r" using aux_lemma by simp
thus "h \<in> generate G K"
by (meson assms generate_repr_iff order.trans r(1) subgroup.subset)
qed
qed
qed
corollary (in group) gen_equality_betw_subgroups:
assumes "subgroup I G" "subgroup J G" "K \<subseteq> (I \<inter> J)"
shows "generate (G \<lparr> carrier := I \<rparr>) K = generate (G \<lparr> carrier := J \<rparr>) K"
by (metis Int_subset_iff assms subgroup_gen_equality)
lemma (in group) normal_generateI:
assumes "H \<subseteq> carrier G"
and "\<And>h g. \<lbrakk> h \<in> H; g \<in> carrier G \<rbrakk> \<Longrightarrow> g \<otimes> h \<otimes> (inv g) \<in> H"
shows "generate G H \<lhd> G"
proof (rule normal_invI)
show "subgroup (generate G H) G"
by (simp add: assms(1) generate_is_subgroup)
next
have "\<And>r g. \<lbrakk> elts r \<subseteq> H; g \<in> carrier G \<rbrakk> \<Longrightarrow> (g \<otimes> (norm G r) \<otimes> (inv g)) \<in> (generate G H)"
proof -
fix r g assume "elts r \<subseteq> H" "g \<in> carrier G"
thus "(g \<otimes> (norm G r) \<otimes> (inv g)) \<in> (generate G H)"
proof (induction r rule: repr.induct)
case One thus ?case
by (simp add: generate.one)
next
case (Inv h)
hence "g \<otimes> h \<otimes> (inv g) \<in> H" using assms(2) by simp
moreover have "norm G (Inv (g \<otimes> h \<otimes> (inv g))) = g \<otimes> (inv h) \<otimes> (inv g)"
using Inv.prems(1) Inv.prems(2) assms(1) inv_mult_group m_assoc by auto
ultimately have "\<exists>r. elts r \<subseteq> H \<and> norm G r = g \<otimes> (inv h) \<otimes> (inv g)"
by (metis elts.simps(2) empty_subsetI insert_subset)
thus ?case by (simp add: assms(1) generate_repr_iff)
next
case (Leaf h)
thus ?case using assms(2)[of h g] generate.incl[of "g \<otimes> h \<otimes> inv g" H] by simp
next
case (Mult h1 h2)
hence "elts h1 \<subseteq> H \<and> elts h2 \<subseteq> H" using Mult(3) by simp
hence in_gen: "norm G h1 \<in> generate G H \<and> norm G h2 \<in> generate G H"
using assms(1) generate_repr_iff by auto
have "g \<otimes> norm G (Mult h1 h2) \<otimes> inv g = g \<otimes> (norm G h1 \<otimes> norm G h2) \<otimes> inv g" by simp
also have " ... = g \<otimes> (norm G h1 \<otimes> (inv g \<otimes> g) \<otimes> norm G h2) \<otimes> inv g"
using Mult(4) in_gen assms(1) generate_in_carrier by auto
also have " ... = (g \<otimes> norm G h1 \<otimes> inv g) \<otimes> (g \<otimes> norm G h2 \<otimes> inv g)"
using Mult.prems(2) assms(1) generate_in_carrier in_gen inv_closed m_assoc m_closed by presburger
finally have "g \<otimes> norm G (Mult h1 h2) \<otimes> inv g =
(g \<otimes> norm G h1 \<otimes> inv g) \<otimes> (g \<otimes> norm G h2 \<otimes> inv g)" .
thus ?case
using generate.eng[of "g \<otimes> norm G h1 \<otimes> inv g" G H "g \<otimes> norm G h2 \<otimes> inv g"]
by (simp add: Mult.IH Mult.prems(2) \<open>elts h1 \<subseteq> H \<and> elts h2 \<subseteq> H\<close>)
qed
qed
thus "\<And>x h. x \<in> carrier G \<Longrightarrow> h \<in> generate G H \<Longrightarrow> x \<otimes> h \<otimes> inv x \<in> generate G H"
using assms(1) generate_repr_iff by auto
qed
subsection\<open>Basic Properties of Generated Groups - Second Part\<close>
lemma (in group) generate_pow:
assumes "a \<in> carrier G"
shows "generate G { a } = range (\<lambda>k::int. a [^] k)" (is "?lhs = ?rhs")
proof
show "?lhs \<subseteq> ?rhs"
proof
fix h show "h \<in> generate G { a } \<Longrightarrow> h \<in> range (\<lambda>k::int. a [^] k)"
proof (induction rule: generate.induct)
case one thus ?case
by (metis (full_types) int_pow_0 rangeI)
next
case (incl h) hence "h = a" by auto thus ?case
by (metis \<open>h = a\<close> assms group.int_pow_1 is_group rangeI)
next
case (inv h) hence "h = a" by auto thus ?case
by (metis (mono_tags) rangeI assms group.int_pow_1 int_pow_neg is_group)
next
case (eng h1 h2) thus ?case
using assms is_group by (auto simp: image_iff simp flip: int_pow_mult)
qed
qed
show "?rhs \<subseteq> ?lhs"
proof
{ fix k :: "nat" have "a [^] k \<in> generate G { a }"
proof (induction k)
case 0 thus ?case by (simp add: generate.one)
next
case (Suc k) thus ?case by (simp add: generate.eng generate.incl)
qed } note aux_lemma = this
fix h assume "h \<in> ?rhs"
then obtain k :: "nat" where "h = a [^] k \<or> h = inv (a [^] k)"
by (auto simp: int_pow_def2)
thus "h \<in> generate G { a }" using aux_lemma
using assms generate_m_inv_closed by auto
qed
qed
(* { a [^] k | k. k \<in> (UNIV :: int set) } *)
corollary (in group) generate_one: "generate G { \<one> } = { \<one> }"
using generate_pow[of "\<one>", OF one_closed] by auto
corollary (in group) generate_empty: "generate G {} = { \<one> }"
using mono_generate[of "{}" "{ \<one> }"] generate_one generate.one one_closed by blast
corollary (in group)
assumes "H \<subseteq> carrier G" "h \<in> H"
shows "h [^] (k :: int) \<in> generate G H"
using mono_generate[of "{ h }" H] generate_pow[of h] assms by auto
subsection\<open>Derived Subgroup\<close>
abbreviation derived_set :: "('a, 'b) monoid_scheme \<Rightarrow> 'a set \<Rightarrow> 'a set" where
"derived_set G H \<equiv>
\<Union>h1 \<in> H. (\<Union>h2 \<in> H. { h1 \<otimes>\<^bsub>G\<^esub> h2 \<otimes>\<^bsub>G\<^esub> (inv\<^bsub>G\<^esub> h1) \<otimes>\<^bsub>G\<^esub> (inv\<^bsub>G\<^esub> h2) })"
definition derived :: "('a, 'b) monoid_scheme \<Rightarrow> 'a set \<Rightarrow> 'a set" where
"derived G H = generate G (derived_set G H)"
lemma (in group) derived_set_incl:
assumes "subgroup H G"
shows "derived_set G H \<subseteq> H"
by (auto simp add: m_inv_consistent[OF assms] subgroupE[OF assms])
lemma (in group) derived_incl:
assumes "subgroup H G"
shows "derived G H \<subseteq> H"
unfolding derived_def using derived_set_incl[OF assms] assms
by (meson generate_min_subgroup1 order.trans subgroup.subset)
lemma (in group) subgroup_derived_equality:
assumes "subgroup H G" "K \<subseteq> H"
shows "derived (G \<lparr> carrier := H \<rparr>) K = derived G K"
proof -
have "derived_set G K \<subseteq> H"
proof
fix x assume "x \<in> derived_set G K"
then obtain k1 k2
where k12: "k1 \<in> K" "k2 \<in> K"
and "x = k1 \<otimes> k2 \<otimes> inv k1 \<otimes> inv k2" by blast
thus "x \<in> H" using k12 assms by (meson subgroup_def subsetCE)
qed
moreover have "derived_set (G \<lparr> carrier := H \<rparr>) K = derived_set G K"
proof
show "derived_set G K \<subseteq> derived_set (G\<lparr>carrier := H\<rparr>) K"
proof
fix x assume "x \<in> derived_set G K"
then obtain k1 k2 where k12: "k1 \<in> K" "k2 \<in> K"
and "x = k1 \<otimes> k2 \<otimes> inv k1 \<otimes> inv k2" by blast
hence "x = k1 \<otimes>\<^bsub>G\<lparr>carrier := H\<rparr>\<^esub> k2 \<otimes>\<^bsub>G\<lparr>carrier := H\<rparr>\<^esub> inv\<^bsub>G\<lparr>carrier := H\<rparr>\<^esub> k1 \<otimes>\<^bsub>G\<lparr>carrier := H\<rparr>\<^esub> inv\<^bsub>G\<lparr>carrier := H\<rparr>\<^esub> k2"
using subgroup_mult_equality[OF assms(1)] m_inv_consistent[OF assms(1)] assms(2) k12
by (simp add: subset_iff)
thus "x \<in> derived_set (G\<lparr>carrier := H\<rparr>) K" using k12 by blast
qed
next
show "derived_set (G \<lparr> carrier := H \<rparr>) K \<subseteq> derived_set G K"
proof
fix x assume "x \<in> derived_set (G \<lparr> carrier := H \<rparr>) K"
then obtain k1 k2
where k12: "k1 \<in> K" "k2 \<in> K"
and "x = k1 \<otimes>\<^bsub>G\<lparr>carrier := H\<rparr>\<^esub> k2 \<otimes>\<^bsub>G\<lparr>carrier := H\<rparr>\<^esub> inv\<^bsub>G\<lparr>carrier := H\<rparr>\<^esub> k1 \<otimes>\<^bsub>G\<lparr>carrier := H\<rparr>\<^esub> inv\<^bsub>G\<lparr>carrier := H\<rparr>\<^esub> k2"
by blast
hence "x = k1 \<otimes> k2 \<otimes> inv k1 \<otimes> inv k2"
using subgroup_mult_equality[OF assms(1)] m_inv_consistent[OF assms(1)] assms(2) k12
by (simp add: subset_iff)
thus "x \<in> derived_set G K" using k12 assms by blast
qed
qed
ultimately show ?thesis unfolding derived_def
using subgroup_gen_equality[OF assms(1), of "derived_set (G\<lparr>carrier := H\<rparr>) K"] by simp
qed
lemma (in comm_group) derived_set:
assumes "H \<subseteq> carrier G"
shows "derived G H = { \<one> }"
proof -
have "derived_set G H = {} \<or> derived_set G H = { \<one> }"
proof (cases)
assume "H = {}" thus ?thesis by simp
next
assume "H \<noteq> {}" then obtain h' where h': "h' \<in> H" by blast
have "derived_set G H = { \<one> }"
proof -
{ fix h assume A: "h \<in> derived_set G H"
have "h = \<one>"
proof -
obtain h1 h2 where h1: "h1 \<in> H" and h2: "h2 \<in> H" and h: "h = h1 \<otimes> h2 \<otimes> inv h1 \<otimes> inv h2"
using A by blast
then have "h1 \<in> carrier G" "h2 \<in> carrier G"
using assms by auto
then have "\<one> = h"
by (metis \<open>h1 \<in> carrier G\<close> \<open>h2 \<in> carrier G\<close> h inv_closed inv_mult m_assoc m_closed r_inv)
then show ?thesis
using \<open>h1 \<in> carrier G\<close> \<open>h2 \<in> carrier G\<close> by force
qed } note aux_lemma = this
show ?thesis
proof
show "derived_set G H \<subseteq> { \<one> }" using aux_lemma by blast
next
show "{ \<one> } \<subseteq> derived_set G H"
proof -
have "h' \<otimes> h' \<otimes> inv h' \<otimes> inv h' \<in> derived_set G H" using h' by blast
thus ?thesis using aux_lemma by auto
qed
qed
qed
thus ?thesis by simp
qed
thus ?thesis unfolding derived_def using generate_empty generate_one by presburger
qed
lemma (in group) derived_set_in_carrier:
assumes "H \<subseteq> carrier G"
shows "derived_set G H \<subseteq> carrier G"
proof
fix h assume "h \<in> derived_set G H"
then obtain h1 h2 where "h1 \<in> H" "h2 \<in> H" "h = h1 \<otimes> h2 \<otimes> inv h1 \<otimes> inv h2"
by blast
thus "h \<in> carrier G" using assms by blast
qed
lemma (in group) derived_is_normal:
assumes "H \<lhd> G"
shows "derived G H \<lhd> G" unfolding derived_def
proof (rule normal_generateI)
show "(\<Union>h1 \<in> H. \<Union>h2 \<in> H. { h1 \<otimes> h2 \<otimes> inv h1 \<otimes> inv h2 }) \<subseteq> carrier G"
using subgroup.subset assms normal_invE(1) by blast
next
show "\<And>h g. \<lbrakk> h \<in> derived_set G H; g \<in> carrier G \<rbrakk> \<Longrightarrow> g \<otimes> h \<otimes> inv g \<in> derived_set G H"
proof -
fix h g assume "h \<in> derived_set G H" and g: "g \<in> carrier G"
then obtain h1 h2 where h1: "h1 \<in> H" "h1 \<in> carrier G"
and h2: "h2 \<in> H" "h2 \<in> carrier G"
and h: "h = h1 \<otimes> h2 \<otimes> inv h1 \<otimes> inv h2"
using subgroup.subset assms normal_invE(1) by blast
hence "g \<otimes> h \<otimes> inv g =
g \<otimes> h1 \<otimes> (inv g \<otimes> g) \<otimes> h2 \<otimes> (inv g \<otimes> g) \<otimes> inv h1 \<otimes> (inv g \<otimes> g) \<otimes> inv h2 \<otimes> inv g"
by (simp add: g m_assoc)
also
have " ... =
(g \<otimes> h1 \<otimes> inv g) \<otimes> (g \<otimes> h2 \<otimes> inv g) \<otimes> (g \<otimes> inv h1 \<otimes> inv g) \<otimes> (g \<otimes> inv h2 \<otimes> inv g)"
using g h1 h2 m_assoc inv_closed m_closed by presburger
finally
have "g \<otimes> h \<otimes> inv g =
(g \<otimes> h1 \<otimes> inv g) \<otimes> (g \<otimes> h2 \<otimes> inv g) \<otimes> inv (g \<otimes> h1 \<otimes> inv g) \<otimes> inv (g \<otimes> h2 \<otimes> inv g)"
by (simp add: g h1 h2 inv_mult_group m_assoc)
moreover have "g \<otimes> h1 \<otimes> inv g \<in> H" by (simp add: assms normal_invE(2) g h1)
moreover have "g \<otimes> h2 \<otimes> inv g \<in> H" by (simp add: assms normal_invE(2) g h2)
ultimately show "g \<otimes> h \<otimes> inv g \<in> derived_set G H" by blast
qed
qed
corollary (in group) derived_self_is_normal: "derived G (carrier G) \<lhd> G"
by (simp add: group.derived_is_normal group.normal_invI is_group subgroup_self)
corollary (in group) derived_subgroup_is_normal:
assumes "subgroup H G"
shows "derived G H \<lhd> G \<lparr> carrier := H \<rparr>"
proof -
have "H \<lhd> G \<lparr> carrier := H \<rparr>"
by (metis assms group.coset_join3 group.normalI group.subgroup_self
partial_object.cases_scheme partial_object.select_convs(1) partial_object.update_convs(1)
subgroup.rcos_const subgroup_imp_group)
hence "derived (G \<lparr> carrier := H \<rparr>) H \<lhd> G \<lparr> carrier := H \<rparr>"
using group.derived_is_normal[of "G \<lparr> carrier := H \<rparr>" H] normal_def by blast
thus ?thesis using subgroup_derived_equality[OF assms] by simp
qed
corollary (in group) derived_quot_is_group: "group (G Mod (derived G (carrier G)))"
using derived_self_is_normal normal.factorgroup_is_group by auto
lemma (in group) derived_quot_is_comm:
assumes "H \<in> carrier (G Mod (derived G (carrier G)))"
and "K \<in> carrier (G Mod (derived G (carrier G)))"
shows "H <#> K = K <#> H"
proof -
{ fix H K assume A1: "H \<in> carrier (G Mod (derived G (carrier G)))"
and A2: "K \<in> carrier (G Mod (derived G (carrier G)))"
have "H <#> K \<subseteq> K <#> H"
proof -
obtain h k where hk: "h \<in> carrier G" "k \<in> carrier G"
and H: "H = (derived G (carrier G)) #> h"
and K: "K = (derived G (carrier G)) #> k"
using A1 A2 unfolding FactGroup_def RCOSETS_def by auto
have "H <#> K = (h \<otimes> k) <# (derived G (carrier G))"
using hk H K derived_self_is_normal m_closed normal.coset_eq normal.rcos_sum
by (metis (no_types, lifting))
moreover have "K <#> H = (k \<otimes> h) <# (derived G (carrier G))"
using hk H K derived_self_is_normal m_closed normal.coset_eq normal.rcos_sum
by (metis (no_types, lifting))
moreover have "(h \<otimes> k) <# (derived G (carrier G)) \<subseteq> (k \<otimes> h) <# (derived G (carrier G))"
proof
fix x assume "x \<in> h \<otimes> k <# derived G (carrier G)"
then obtain d where d: "d \<in> derived G (carrier G)" "d \<in> carrier G" "x = h \<otimes> k \<otimes> d"
using generate_is_subgroup[of "derived_set G (carrier G)"]
subgroup.subset[of "derived G (carrier G)" G]
derived_set_in_carrier[of "carrier G"]
unfolding l_coset_def derived_def by auto
hence "x = (k \<otimes> (h \<otimes> inv h) \<otimes> inv k) \<otimes> h \<otimes> k \<otimes> d"
using hk by simp
also have " ... = (k \<otimes> h) \<otimes> (inv h \<otimes> inv k) \<otimes> h \<otimes> k \<otimes> d"
using d(2) hk m_assoc by (metis subgroup_def subgroup_self)
also have " ... = (k \<otimes> h) \<otimes> ((inv h \<otimes> inv k \<otimes> h \<otimes> k) \<otimes> d)"
using d(2) hk m_assoc by simp
finally have "x = (k \<otimes> h) \<otimes> ((inv h \<otimes> inv k \<otimes> h \<otimes> k) \<otimes> d)" .
moreover have "inv h \<otimes> inv k \<otimes> inv (inv h) \<otimes> inv (inv k) \<in> derived_set G (carrier G)"
using inv_closed[OF hk(1)] inv_closed[OF hk(2)] by blast
hence "inv h \<otimes> inv k \<otimes> h \<otimes> k \<in> derived_set G (carrier G)"
by (simp add: hk(1) hk(2))
hence "(inv h \<otimes> inv k \<otimes> h \<otimes> k) \<otimes> d \<in> derived G (carrier G)"
using d(1) unfolding derived_def by (simp add: generate.eng generate.incl)
ultimately show "x \<in> (k \<otimes> h) <# (derived G (carrier G))"
unfolding l_coset_def by blast
qed
ultimately show ?thesis by simp
qed }
thus ?thesis using assms by auto
qed
theorem (in group) derived_quot_is_comm_group:
"comm_group (G Mod (derived G (carrier G)))"
apply (intro group.group_comm_groupI[OF derived_quot_is_group])
using derived_quot_is_comm by simp
corollary (in group) derived_quot_of_subgroup_is_comm_group:
assumes "subgroup H G"
shows "comm_group ((G \<lparr> carrier := H \<rparr>) Mod (derived G H))"
proof -
have "group (G \<lparr> carrier := H \<rparr>)"
using assms subgroup_imp_group by auto
thus ?thesis
using group.derived_quot_is_comm_group subgroup_derived_equality[OF assms] by fastforce
qed
lemma (in group) mono_derived:
assumes "J \<subseteq> carrier G" "I \<subseteq> J"
shows "(derived G ^^ n) I \<subseteq> (derived G ^^ n) J"
proof -
{ fix I J assume A: "J \<subseteq> carrier G" "I \<subseteq> J" have "derived G I \<subseteq> derived G J"
proof -
have "derived_set G I \<subseteq> derived_set G J" using A by blast
thus ?thesis unfolding derived_def using mono_generate A by (simp add: derived_set_in_carrier)
qed } note aux_lemma1 = this
{ fix n I assume A: "I \<subseteq> carrier G" have "(derived G ^^ n) I \<subseteq> carrier G"
proof (induction n)
case 0 thus ?case using A by simp
next
case (Suc n)
with aux_lemma1 have "(derived G ^^ Suc n) I \<subseteq> derived G (carrier G)"
by auto
also have "... \<subseteq> carrier G"
by (simp add: derived_incl subgroup_self)
finally show ?case .
qed } note aux_lemma2 = this
show ?thesis
proof (induction n)
case 0 thus ?case using assms by simp
next
case (Suc n) thus ?case using aux_lemma1 aux_lemma2 assms(1) by auto
qed
qed
lemma (in group) exp_of_derived_in_carrier:
assumes "H \<subseteq> carrier G"
shows "(derived G ^^ n) H \<subseteq> carrier G" using assms
proof (induction n)
case 0 thus ?case by simp
next
case (Suc n)
have "(derived G ^^ Suc n) H = (derived G) ((derived G ^^ n) H)" by simp
also have " ... \<subseteq> (derived G) (carrier G)"
using mono_derived[of "carrier G" "(derived G ^^ n) H" 1] Suc by simp
also have " ... \<subseteq> carrier G" unfolding derived_def
by (simp add: derived_set_incl generate_min_subgroup1 subgroup_self)
finally show ?case .
qed
lemma (in group) exp_of_derived_is_subgroup:
assumes "subgroup H G"
shows "subgroup ((derived G ^^ n) H) G" using assms
proof (induction n)
case 0 thus ?case by simp
next
case (Suc n)
have "(derived G ^^ n) H \<subseteq> carrier G"
by (simp add: Suc.IH assms subgroup.subset)
hence "subgroup ((derived G) ((derived G ^^ n) H)) G"
unfolding derived_def using derived_set_in_carrier generate_is_subgroup by auto
thus ?case by simp
qed
hide_const (open) norm
end