--- a/src/HOL/Algebra/Algebra.thy Tue Apr 02 13:15:52 2019 +0200
+++ b/src/HOL/Algebra/Algebra.thy Tue Apr 02 12:56:21 2019 +0100
@@ -1,7 +1,7 @@
(* Title: HOL/Algebra/Algebra.thy *)
theory Algebra
- imports Sylow Chinese_Remainder Zassenhaus Galois_Connection Generated_Fields
+ imports Sylow Chinese_Remainder Zassenhaus Galois_Connection Generated_Fields Elementary_Groups
Divisibility Embedded_Algebras IntRing Sym_Groups Exact_Sequence Polynomials
begin
end
--- a/src/HOL/Algebra/Coset.thy Tue Apr 02 13:15:52 2019 +0200
+++ b/src/HOL/Algebra/Coset.thy Tue Apr 02 12:56:21 2019 +0100
@@ -203,6 +203,10 @@
"\<lbrakk>h \<in> hom G H; group G; group H\<rbrakk> \<Longrightarrow> inj_on h (carrier G) \<longleftrightarrow> (\<forall>x. x \<in> carrier G \<longrightarrow> h x = one H \<longrightarrow> x = one G)"
using group_hom.inj_on_one_iff group_hom.intro group_hom_axioms.intro by blast
+lemma mon_iff_hom_one:
+ "\<lbrakk>group G; group H\<rbrakk> \<Longrightarrow> f \<in> mon G H \<longleftrightarrow> f \<in> hom G H \<and> (\<forall>x. x \<in> carrier G \<and> f x = \<one>\<^bsub>H\<^esub> \<longrightarrow> x = \<one>\<^bsub>G\<^esub>)"
+ by (auto simp: mon_def inj_on_one_iff')
+
lemma (in group_hom) iso_iff: "h \<in> iso G H \<longleftrightarrow> carrier H \<subseteq> h ` carrier G \<and> (\<forall>x\<in>carrier G. h x = \<one>\<^bsub>H\<^esub> \<longrightarrow> x = \<one>)"
by (auto simp: iso_def bij_betw_def inj_on_one_iff)
@@ -374,7 +378,7 @@
subsection \<open>Normal subgroups\<close>
lemma normal_imp_subgroup: "H \<lhd> G \<Longrightarrow> subgroup H G"
- by (simp add: normal_def subgroup_def)
+ by (rule normal.axioms(1))
lemma (in group) normalI:
"subgroup H G \<Longrightarrow> (\<forall>x \<in> carrier G. H #> x = x <# H) \<Longrightarrow> H \<lhd> G"
@@ -396,6 +400,14 @@
shows "x \<otimes> h \<otimes> (inv x) \<in> H"
using assms inv_op_closed1 by (metis inv_closed inv_inv)
+lemma (in comm_group) normal_iff_subgroup:
+ "N \<lhd> G \<longleftrightarrow> subgroup N G"
+proof
+ assume "subgroup N G"
+ then show "N \<lhd> G"
+ by unfold_locales (auto simp: subgroupE subgroup.one_closed l_coset_def r_coset_def m_comm subgroup.mem_carrier)
+qed (simp add: normal_imp_subgroup)
+
text\<open>Alternative characterization of normal subgroups\<close>
lemma (in group) normal_inv_iff:
@@ -925,8 +937,14 @@
apply (auto dest: rcosets_inv_mult_group_eq simp add: setinv_closed)
done
-lemma mult_FactGroup [simp]: "X \<otimes>\<^bsub>(G Mod H)\<^esub> X' = X <#>\<^bsub>G\<^esub> X'"
- by (simp add: FactGroup_def)
+lemma carrier_FactGroup: "carrier(G Mod N) = (\<lambda>x. r_coset G N x) ` carrier G"
+ by (auto simp: FactGroup_def RCOSETS_def)
+
+lemma one_FactGroup [simp]: "one(G Mod N) = N"
+ by (auto simp: FactGroup_def)
+
+lemma mult_FactGroup [simp]: "monoid.mult (G Mod N) = set_mult G"
+ by (auto simp: FactGroup_def)
lemma (in normal) inv_FactGroup:
assumes "X \<in> carrier (G Mod H)"
@@ -951,6 +969,79 @@
by (auto simp add: FactGroup_def RCOSETS_def Pi_def hom_def rcos_sum)
+lemma (in comm_group) set_mult_commute:
+ assumes "N \<subseteq> carrier G" "x \<in> rcosets N" "y \<in> rcosets N"
+ shows "x <#> y = y <#> x"
+ using assms unfolding set_mult_def RCOSETS_def
+ by auto (metis m_comm r_coset_subset_G subsetCE)+
+
+lemma (in comm_group) abelian_FactGroup:
+ assumes "subgroup N G" shows "comm_group(G Mod N)"
+proof (rule group.group_comm_groupI)
+ have "N \<lhd> G"
+ by (simp add: assms normal_iff_subgroup)
+ then show "Group.group (G Mod N)"
+ by (simp add: normal.factorgroup_is_group)
+ fix x :: "'a set" and y :: "'a set"
+ assume "x \<in> carrier (G Mod N)" "y \<in> carrier (G Mod N)"
+ then show "x \<otimes>\<^bsub>G Mod N\<^esub> y = y \<otimes>\<^bsub>G Mod N\<^esub> x"
+ apply (simp add: FactGroup_def subgroup_def)
+ apply (rule set_mult_commute)
+ using assms apply (auto simp: subgroup_def)
+ done
+qed
+
+
+lemma FactGroup_universal:
+ assumes "h \<in> hom G H" "N \<lhd> G"
+ and h: "\<And>x y. \<lbrakk>x \<in> carrier G; y \<in> carrier G; r_coset G N x = r_coset G N y\<rbrakk> \<Longrightarrow> h x = h y"
+ obtains g
+ where "g \<in> hom (G Mod N) H" "\<And>x. x \<in> carrier G \<Longrightarrow> g(r_coset G N x) = h x"
+proof -
+ obtain g where g: "\<And>x. x \<in> carrier G \<Longrightarrow> h x = g(r_coset G N x)"
+ using h function_factors_left_gen [of "\<lambda>x. x \<in> carrier G" "r_coset G N" h] by blast
+ show thesis
+ proof
+ show "g \<in> hom (G Mod N) H"
+ proof (rule homI)
+ show "g (u \<otimes>\<^bsub>G Mod N\<^esub> v) = g u \<otimes>\<^bsub>H\<^esub> g v"
+ if "u \<in> carrier (G Mod N)" "v \<in> carrier (G Mod N)" for u v
+ proof -
+ from that
+ obtain x y where xy: "x \<in> carrier G" "u = r_coset G N x" "y \<in> carrier G" "v = r_coset G N y"
+ by (auto simp: carrier_FactGroup)
+ then have "h (x \<otimes>\<^bsub>G\<^esub> y) = h x \<otimes>\<^bsub>H\<^esub> h y"
+ by (metis hom_mult [OF \<open>h \<in> hom G H\<close>])
+ then show ?thesis
+ by (metis Coset.mult_FactGroup xy \<open>N \<lhd> G\<close> g group.subgroup_self normal.axioms(2) normal.rcos_sum subgroup_def)
+ qed
+ qed (use \<open>h \<in> hom G H\<close> in \<open>auto simp: carrier_FactGroup Pi_iff hom_def simp flip: g\<close>)
+ qed (auto simp flip: g)
+qed
+
+
+lemma (in normal) FactGroup_pow:
+ fixes k::nat
+ assumes "a \<in> carrier G"
+ shows "pow (FactGroup G H) (r_coset G H a) k = r_coset G H (pow G a k)"
+proof (induction k)
+ case 0
+ then show ?case
+ by (simp add: r_coset_def)
+next
+ case (Suc k)
+ then show ?case
+ by (simp add: assms rcos_sum)
+qed
+
+lemma (in normal) FactGroup_int_pow:
+ fixes k::int
+ assumes "a \<in> carrier G"
+ shows "pow (FactGroup G H) (r_coset G H a) k = r_coset G H (pow G a k)"
+ by (metis Group.group.axioms(1) image_eqI is_group monoid.nat_pow_closed int_pow_def2 assms
+ FactGroup_pow carrier_FactGroup inv_FactGroup rcos_inv)
+
+
subsection\<open>The First Isomorphism Theorem\<close>
text\<open>The quotient by the kernel of a homomorphism is isomorphic to the
@@ -983,6 +1074,30 @@
qed
+lemma (in group_hom) FactGroup_universal_kernel:
+ assumes "N \<lhd> G" and h: "N \<subseteq> kernel G H h"
+ obtains g where "g \<in> hom (G Mod N) H" "\<And>x. x \<in> carrier G \<Longrightarrow> g(r_coset G N x) = h x"
+proof -
+ have "h x = h y"
+ if "x \<in> carrier G" "y \<in> carrier G" "r_coset G N x = r_coset G N y" for x y
+ proof -
+ have "x \<otimes>\<^bsub>G\<^esub> inv\<^bsub>G\<^esub> y \<in> N"
+ using \<open>N \<lhd> G\<close> group.rcos_self normal.axioms(2) normal_imp_subgroup
+ subgroup.rcos_module_imp that by fastforce
+ with h have xy: "x \<otimes>\<^bsub>G\<^esub> inv\<^bsub>G\<^esub> y \<in> kernel G H h"
+ by blast
+ have "h x \<otimes>\<^bsub>H\<^esub> inv\<^bsub>H\<^esub>(h y) = h (x \<otimes>\<^bsub>G\<^esub> inv\<^bsub>G\<^esub> y)"
+ by (simp add: that)
+ also have "\<dots> = \<one>\<^bsub>H\<^esub>"
+ using xy by (simp add: kernel_def)
+ finally have "h x \<otimes>\<^bsub>H\<^esub> inv\<^bsub>H\<^esub>(h y) = \<one>\<^bsub>H\<^esub>" .
+ then show ?thesis
+ using H.inv_equality that by fastforce
+ qed
+ with FactGroup_universal [OF homh \<open>N \<lhd> G\<close>] that show thesis
+ by metis
+qed
+
lemma (in group_hom) FactGroup_the_elem_mem:
assumes X: "X \<in> carrier (G Mod (kernel G H h))"
shows "the_elem (h`X) \<in> carrier H"
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Algebra/Elementary_Groups.thy Tue Apr 02 12:56:21 2019 +0100
@@ -0,0 +1,382 @@
+section \<open>Elementary Group Constructions\<close>
+
+(* Title: HOL/Algebra/Elementary_Groups.thy
+ Author: LC Paulson, ported from HOL Light
+*)
+
+theory Elementary_Groups
+imports Generated_Groups
+begin
+
+subsection\<open>Direct sum/product lemmas\<close>
+
+locale group_disjoint_sum = group G + AG: subgroup A G + BG: subgroup B G for G (structure) and A B
+begin
+
+lemma subset_one: "A \<inter> B \<subseteq> {\<one>} \<longleftrightarrow> A \<inter> B = {\<one>}"
+ by auto
+
+lemma sub_id_iff: "A \<inter> B \<subseteq> {\<one>} \<longleftrightarrow> (\<forall>x\<in>A. \<forall>y\<in>B. x \<otimes> y = \<one> \<longrightarrow> x = \<one> \<and> y = \<one>)"
+ (is "?lhs = ?rhs")
+proof -
+ have "?lhs = (\<forall>x\<in>A. \<forall>y\<in>B. x \<otimes> inv y = \<one> \<longrightarrow> x = \<one> \<and> inv y = \<one>)"
+ proof (intro ballI iffI impI)
+ fix x y
+ assume "A \<inter> B \<subseteq> {\<one>}" "x \<in> A" "y \<in> B" "x \<otimes> inv y = \<one>"
+ then have "y = x"
+ using group.inv_equality group_l_invI by fastforce
+ then show "x = \<one> \<and> inv y = \<one>"
+ using \<open>A \<inter> B \<subseteq> {\<one>}\<close> \<open>x \<in> A\<close> \<open>y \<in> B\<close> by fastforce
+ next
+ assume "\<forall>x\<in>A. \<forall>y\<in>B. x \<otimes> inv y = \<one> \<longrightarrow> x = \<one> \<and> inv y = \<one>"
+ then show "A \<inter> B \<subseteq> {\<one>}"
+ by auto
+ qed
+ also have "\<dots> = ?rhs"
+ by (metis BG.mem_carrier BG.subgroup_axioms inv_inv subgroup_def)
+ finally show ?thesis .
+qed
+
+lemma cancel: "A \<inter> B \<subseteq> {\<one>} \<longleftrightarrow> (\<forall>x\<in>A. \<forall>y\<in>B. \<forall>x'\<in>A. \<forall>y'\<in>B. x \<otimes> y = x' \<otimes> y' \<longrightarrow> x = x' \<and> y = y')"
+ (is "?lhs = ?rhs")
+proof -
+ have "(\<forall>x\<in>A. \<forall>y\<in>B. x \<otimes> y = \<one> \<longrightarrow> x = \<one> \<and> y = \<one>) = ?rhs"
+ (is "?med = _")
+ proof (intro ballI iffI impI)
+ fix x y x' y'
+ assume * [rule_format]: "\<forall>x\<in>A. \<forall>y\<in>B. x \<otimes> y = \<one> \<longrightarrow> x = \<one> \<and> y = \<one>"
+ and AB: "x \<in> A" "y \<in> B" "x' \<in> A" "y' \<in> B" and eq: "x \<otimes> y = x' \<otimes> y'"
+ then have carr: "x \<in> carrier G" "x' \<in> carrier G" "y \<in> carrier G" "y' \<in> carrier G"
+ using AG.subset BG.subset by auto
+ then have "inv x' \<otimes> x \<otimes> (y \<otimes> inv y') = inv x' \<otimes> (x \<otimes> y) \<otimes> inv y'"
+ by (simp add: m_assoc)
+ also have "\<dots> = \<one>"
+ using carr by (simp add: eq) (simp add: m_assoc)
+ finally have 1: "inv x' \<otimes> x \<otimes> (y \<otimes> inv y') = \<one>" .
+ show "x = x' \<and> y = y'"
+ using * [OF _ _ 1] AB by simp (metis carr inv_closed inv_inv local.inv_equality)
+ next
+ fix x y
+ assume * [rule_format]: "\<forall>x\<in>A. \<forall>y\<in>B. \<forall>x'\<in>A. \<forall>y'\<in>B. x \<otimes> y = x' \<otimes> y' \<longrightarrow> x = x' \<and> y = y'"
+ and xy: "x \<in> A" "y \<in> B" "x \<otimes> y = \<one>"
+ show "x = \<one> \<and> y = \<one>"
+ by (rule *) (use xy in auto)
+ qed
+ then show ?thesis
+ by (simp add: sub_id_iff)
+qed
+
+lemma commuting_imp_normal1:
+ assumes sub: "carrier G \<subseteq> A <#> B"
+ and mult: "\<And>x y. \<lbrakk>x \<in> A; y \<in> B\<rbrakk> \<Longrightarrow> x \<otimes> y = y \<otimes> x"
+ shows "A \<lhd> G"
+proof -
+ have AB: "A \<subseteq> carrier G \<and> B \<subseteq> carrier G"
+ by (simp add: AG.subset BG.subset)
+ have "A #> x = x <# A"
+ if x: "x \<in> carrier G" for x
+ proof -
+ obtain a b where xeq: "x = a \<otimes> b" and "a \<in> A" "b \<in> B" and carr: "a \<in> carrier G" "b \<in> carrier G"
+ using x sub AB by (force simp: set_mult_def)
+ have Ab: "A <#> {b} = {b} <#> A"
+ using AB \<open>a \<in> A\<close> \<open>b \<in> B\<close> mult
+ by (force simp: set_mult_def m_assoc subset_iff)
+ have "A #> x = A <#> {a \<otimes> b}"
+ by (auto simp: l_coset_eq_set_mult r_coset_eq_set_mult xeq)
+ also have "\<dots> = A <#> {a} <#> {b}"
+ using AB \<open>a \<in> A\<close> \<open>b \<in> B\<close>
+ by (auto simp: set_mult_def m_assoc subset_iff)
+ also have "\<dots> = {a} <#> A <#> {b}"
+ by (metis AG.rcos_const AG.subgroup_axioms \<open>a \<in> A\<close> coset_join3 is_group l_coset_eq_set_mult r_coset_eq_set_mult subgroup.mem_carrier)
+ also have "\<dots> = {a} <#> {b} <#> A"
+ by (simp add: is_group carr group.set_mult_assoc AB Ab)
+ also have "\<dots> = {x} <#> A"
+ by (auto simp: set_mult_def xeq)
+ finally show "A #> x = x <# A"
+ by (simp add: l_coset_eq_set_mult)
+ qed
+ then show ?thesis
+ by (auto simp: normal_def normal_axioms_def AG.subgroup_axioms is_group)
+qed
+
+lemma commuting_imp_normal2:
+ assumes"carrier G \<subseteq> A <#> B" "\<And>x y. \<lbrakk>x \<in> A; y \<in> B\<rbrakk> \<Longrightarrow> x \<otimes> y = y \<otimes> x"
+ shows "B \<lhd> G"
+proof (rule group_disjoint_sum.commuting_imp_normal1)
+ show "group_disjoint_sum G B A"
+ proof qed
+next
+ show "carrier G \<subseteq> B <#> A"
+ using BG.subgroup_axioms assms commut_normal commuting_imp_normal1 by blast
+qed (use assms in auto)
+
+
+lemma (in group) normal_imp_commuting:
+ assumes "A \<lhd> G" "B \<lhd> G" "A \<inter> B \<subseteq> {\<one>}" "x \<in> A" "y \<in> B"
+ shows "x \<otimes> y = y \<otimes> x"
+proof -
+ interpret AG: normal A G
+ using assms by auto
+ interpret BG: normal B G
+ using assms by auto
+ interpret group_disjoint_sum G A B
+ proof qed
+ have * [rule_format]: "(\<forall>x\<in>A. \<forall>y\<in>B. \<forall>x'\<in>A. \<forall>y'\<in>B. x \<otimes> y = x' \<otimes> y' \<longrightarrow> x = x' \<and> y = y')"
+ using cancel assms by (auto simp: normal_def)
+ have carr: "x \<in> carrier G" "y \<in> carrier G"
+ using assms AG.subset BG.subset by auto
+ then show ?thesis
+ using * [of x _ _ y] AG.coset_eq [rule_format, of y] BG.coset_eq [rule_format, of x]
+ by (clarsimp simp: l_coset_def r_coset_def set_eq_iff) (metis \<open>x \<in> A\<close> \<open>y \<in> B\<close>)
+qed
+
+lemma normal_eq_commuting:
+ assumes "carrier G \<subseteq> A <#> B" "A \<inter> B \<subseteq> {\<one>}"
+ shows "A \<lhd> G \<and> B \<lhd> G \<longleftrightarrow> (\<forall>x\<in>A. \<forall>y\<in>B. x \<otimes> y = y \<otimes> x)"
+ by (metis assms commuting_imp_normal1 commuting_imp_normal2 normal_imp_commuting)
+
+lemma (in group) hom_group_mul_rev:
+ assumes "(\<lambda>(x,y). x \<otimes> y) \<in> hom (subgroup_generated G A \<times>\<times> subgroup_generated G B) G"
+ (is "?h \<in> hom ?P G")
+ and "x \<in> carrier G" "y \<in> carrier G" "x \<in> A" "y \<in> B"
+ shows "x \<otimes> y = y \<otimes> x"
+proof -
+ interpret P: group_hom ?P G ?h
+ by (simp add: assms DirProd_group group_hom.intro group_hom_axioms.intro is_group)
+ have xy: "(x,y) \<in> carrier ?P"
+ by (auto simp: assms carrier_subgroup_generated generate.incl)
+ have "x \<otimes> (x \<otimes> (y \<otimes> y)) = x \<otimes> (y \<otimes> (x \<otimes> y))"
+ using P.hom_mult [OF xy xy] by (simp add: m_assoc assms)
+ then have "x \<otimes> (y \<otimes> y) = y \<otimes> (x \<otimes> y)"
+ using assms by simp
+ then show ?thesis
+ by (simp add: assms flip: m_assoc)
+qed
+
+lemma hom_group_mul_eq:
+ "(\<lambda>(x,y). x \<otimes> y) \<in> hom (subgroup_generated G A \<times>\<times> subgroup_generated G B) G
+ \<longleftrightarrow> (\<forall>x\<in>A. \<forall>y\<in>B. x \<otimes> y = y \<otimes> x)"
+ (is "?lhs = ?rhs")
+proof
+ assume ?lhs then show ?rhs
+ using hom_group_mul_rev AG.subset BG.subset by blast
+next
+ assume R: ?rhs
+ have subG: "generate G (carrier G \<inter> A) \<subseteq> carrier G" for A
+ by (simp add: generate_incl)
+ have *: "x \<otimes> u \<otimes> (y \<otimes> v) = x \<otimes> y \<otimes> (u \<otimes> v)"
+ if eq [rule_format]: "\<forall>x\<in>A. \<forall>y\<in>B. x \<otimes> y = y \<otimes> x"
+ and gen: "x \<in> generate G (carrier G \<inter> A)" "y \<in> generate G (carrier G \<inter> B)"
+ "u \<in> generate G (carrier G \<inter> A)" "v \<in> generate G (carrier G \<inter> B)"
+ for x y u v
+ proof -
+ have "u \<otimes> y = y \<otimes> u"
+ by (metis AG.carrier_subgroup_generated_subgroup BG.carrier_subgroup_generated_subgroup carrier_subgroup_generated eq that(3) that(4))
+ then have "x \<otimes> u \<otimes> y = x \<otimes> y \<otimes> u"
+ using gen by (simp add: m_assoc subsetD [OF subG])
+ then show ?thesis
+ using gen by (simp add: subsetD [OF subG] flip: m_assoc)
+ qed
+ show ?lhs
+ using R by (auto simp: hom_def carrier_subgroup_generated subsetD [OF subG] *)
+qed
+
+
+lemma epi_group_mul_eq:
+ "(\<lambda>(x,y). x \<otimes> y) \<in> epi (subgroup_generated G A \<times>\<times> subgroup_generated G B) G
+ \<longleftrightarrow> A <#> B = carrier G \<and> (\<forall>x\<in>A. \<forall>y\<in>B. x \<otimes> y = y \<otimes> x)"
+proof -
+ have subGA: "generate G (carrier G \<inter> A) \<subseteq> A"
+ by (simp add: AG.subgroup_axioms generate_subgroup_incl)
+ have subGB: "generate G (carrier G \<inter> B) \<subseteq> B"
+ by (simp add: BG.subgroup_axioms generate_subgroup_incl)
+ have "(((\<lambda>(x, y). x \<otimes> y) ` (generate G (carrier G \<inter> A) \<times> generate G (carrier G \<inter> B)))) = ((A <#> B))"
+ by (auto simp: set_mult_def generate.incl pair_imageI dest: subsetD [OF subGA] subsetD [OF subGB])
+ then show ?thesis
+ by (auto simp: epi_def hom_group_mul_eq carrier_subgroup_generated)
+qed
+
+lemma mon_group_mul_eq:
+ "(\<lambda>(x,y). x \<otimes> y) \<in> mon (subgroup_generated G A \<times>\<times> subgroup_generated G B) G
+ \<longleftrightarrow> A \<inter> B = {\<one>} \<and> (\<forall>x\<in>A. \<forall>y\<in>B. x \<otimes> y = y \<otimes> x)"
+proof -
+ have subGA: "generate G (carrier G \<inter> A) \<subseteq> A"
+ by (simp add: AG.subgroup_axioms generate_subgroup_incl)
+ have subGB: "generate G (carrier G \<inter> B) \<subseteq> B"
+ by (simp add: BG.subgroup_axioms generate_subgroup_incl)
+ show ?thesis
+ apply (auto simp: mon_def hom_group_mul_eq simp flip: subset_one)
+ apply (simp_all (no_asm_use) add: inj_on_def AG.carrier_subgroup_generated_subgroup BG.carrier_subgroup_generated_subgroup)
+ using cancel apply blast+
+ done
+qed
+
+lemma iso_group_mul_alt:
+ "(\<lambda>(x,y). x \<otimes> y) \<in> iso (subgroup_generated G A \<times>\<times> subgroup_generated G B) G
+ \<longleftrightarrow> A \<inter> B = {\<one>} \<and> A <#> B = carrier G \<and> (\<forall>x\<in>A. \<forall>y\<in>B. x \<otimes> y = y \<otimes> x)"
+ by (auto simp: iso_iff_mon_epi mon_group_mul_eq epi_group_mul_eq)
+
+lemma iso_group_mul_eq:
+ "(\<lambda>(x,y). x \<otimes> y) \<in> iso (subgroup_generated G A \<times>\<times> subgroup_generated G B) G
+ \<longleftrightarrow> A \<inter> B = {\<one>} \<and> A <#> B = carrier G \<and> A \<lhd> G \<and> B \<lhd> G"
+ by (simp add: iso_group_mul_alt normal_eq_commuting cong: conj_cong)
+
+
+lemma (in group) iso_group_mul_gen:
+ assumes "A \<lhd> G" "B \<lhd> G"
+ shows "(\<lambda>(x,y). x \<otimes> y) \<in> iso (subgroup_generated G A \<times>\<times> subgroup_generated G B) G
+ \<longleftrightarrow> A \<inter> B \<subseteq> {\<one>} \<and> A <#> B = carrier G"
+proof -
+ interpret group_disjoint_sum G A B
+ using assms by (auto simp: group_disjoint_sum_def normal_def)
+ show ?thesis
+ by (simp add: subset_one iso_group_mul_eq assms)
+qed
+
+
+lemma iso_group_mul:
+ assumes "comm_group G"
+ shows "((\<lambda>(x,y). x \<otimes> y) \<in> iso (DirProd (subgroup_generated G A) (subgroup_generated G B)) G
+ \<longleftrightarrow> A \<inter> B \<subseteq> {\<one>} \<and> A <#> B = carrier G)"
+proof (rule iso_group_mul_gen)
+ interpret comm_group
+ by (rule assms)
+ show "A \<lhd> G"
+ by (simp add: AG.subgroup_axioms subgroup_imp_normal)
+ show "B \<lhd> G"
+ by (simp add: BG.subgroup_axioms subgroup_imp_normal)
+qed
+
+end
+
+
+subsection\<open>The one-element group on a given object\<close>
+
+definition singleton_group :: "'a \<Rightarrow> 'a monoid"
+ where "singleton_group a = \<lparr>carrier = {a}, monoid.mult = (\<lambda>x y. a), one = a\<rparr>"
+
+lemma singleton_group [simp]: "group (singleton_group a)"
+ unfolding singleton_group_def by (auto intro: groupI)
+
+lemma singleton_abelian_group [simp]: "comm_group (singleton_group a)"
+ by (metis group.group_comm_groupI monoid.simps(1) singleton_group singleton_group_def)
+
+lemma carrier_singleton_group [simp]: "carrier (singleton_group a) = {a}"
+ by (auto simp: singleton_group_def)
+
+lemma (in group) hom_into_singleton_iff [simp]:
+ "h \<in> hom G (singleton_group a) \<longleftrightarrow> h \<in> carrier G \<rightarrow> {a}"
+ by (auto simp: hom_def singleton_group_def)
+
+declare group.hom_into_singleton_iff [simp]
+
+lemma (in group) id_hom_singleton: "id \<in> hom (singleton_group \<one>) G"
+ by (simp add: hom_def singleton_group_def)
+
+subsection\<open>Similarly, trivial groups\<close>
+
+definition trivial_group :: "('a, 'b) monoid_scheme \<Rightarrow> bool"
+ where "trivial_group G \<equiv> group G \<and> carrier G = {one G}"
+
+lemma trivial_imp_finite_group:
+ "trivial_group G \<Longrightarrow> finite(carrier G)"
+ by (simp add: trivial_group_def)
+
+lemma trivial_singleton_group [simp]: "trivial_group(singleton_group a)"
+ by (metis monoid.simps(2) partial_object.simps(1) singleton_group singleton_group_def trivial_group_def)
+
+lemma (in group) trivial_group_subset:
+ "trivial_group G \<longleftrightarrow> carrier G \<subseteq> {one G}"
+ using is_group trivial_group_def by fastforce
+
+lemma (in group) trivial_group: "trivial_group G \<longleftrightarrow> (\<exists>a. carrier G = {a})"
+ unfolding trivial_group_def using one_closed is_group by fastforce
+
+lemma (in group) trivial_group_alt:
+ "trivial_group G \<longleftrightarrow> (\<exists>a. carrier G \<subseteq> {a})"
+ by (auto simp: trivial_group)
+
+lemma (in group) trivial_group_subgroup_generated:
+ assumes "S \<subseteq> {one G}"
+ shows "trivial_group(subgroup_generated G S)"
+proof -
+ have "carrier (subgroup_generated G S) \<subseteq> {\<one>}"
+ using generate_empty generate_one subset_singletonD assms
+ by (fastforce simp add: carrier_subgroup_generated)
+ then show ?thesis
+ by (simp add: group.trivial_group_subset)
+qed
+
+lemma (in group) trivial_group_subgroup_generated_eq:
+ "trivial_group(subgroup_generated G s) \<longleftrightarrow> carrier G \<inter> s \<subseteq> {one G}"
+ apply (rule iffI)
+ apply (force simp: trivial_group_def carrier_subgroup_generated generate.incl)
+ by (metis subgroup_generated_restrict trivial_group_subgroup_generated)
+
+lemma isomorphic_group_triviality1:
+ assumes "G \<cong> H" "group H" "trivial_group G"
+ shows "trivial_group H"
+ using assms
+ by (auto simp: trivial_group_def is_iso_def iso_def group.is_monoid Group.group_def bij_betw_def hom_one)
+
+lemma isomorphic_group_triviality:
+ assumes "G \<cong> H" "group G" "group H"
+ shows "trivial_group G \<longleftrightarrow> trivial_group H"
+ by (meson assms group.iso_sym isomorphic_group_triviality1)
+
+lemma (in group_hom) kernel_from_trivial_group:
+ "trivial_group G \<Longrightarrow> kernel G H h = carrier G"
+ by (auto simp: trivial_group_def kernel_def)
+
+lemma (in group_hom) image_from_trivial_group:
+ "trivial_group G \<Longrightarrow> h ` carrier G = {one H}"
+ by (auto simp: trivial_group_def)
+
+lemma (in group_hom) kernel_to_trivial_group:
+ "trivial_group H \<Longrightarrow> kernel G H h = carrier G"
+ unfolding kernel_def trivial_group_def
+ using hom_closed by blast
+
+
+subsection\<open>The additive group of integers\<close>
+
+definition integer_group
+ where "integer_group = \<lparr>carrier = UNIV, monoid.mult = (+), one = (0::int)\<rparr>"
+
+lemma group_integer_group [simp]: "group integer_group"
+ unfolding integer_group_def
+proof (rule groupI; simp)
+ show "\<And>x::int. \<exists>y. y + x = 0"
+ by presburger
+qed
+
+lemma carrier_integer_group [simp]: "carrier integer_group = UNIV"
+ by (auto simp: integer_group_def)
+
+lemma one_integer_group [simp]: "\<one>\<^bsub>integer_group\<^esub> = 0"
+ by (auto simp: integer_group_def)
+
+lemma mult_integer_group [simp]: "x \<otimes>\<^bsub>integer_group\<^esub> y = x + y"
+ by (auto simp: integer_group_def)
+
+lemma inv_integer_group [simp]: "inv\<^bsub>integer_group\<^esub> x = -x"
+ by (rule group.inv_equality [OF group_integer_group]) (auto simp: integer_group_def)
+
+lemma abelian_integer_group: "comm_group integer_group"
+ by (rule group.group_comm_groupI [OF group_integer_group]) (auto simp: integer_group_def)
+
+lemma group_nat_pow_integer_group [simp]:
+ fixes n::nat and x::int
+ shows "pow integer_group x n = int n * x"
+ by (induction n) (auto simp: integer_group_def algebra_simps)
+
+lemma group_int_pow_integer_group [simp]:
+ fixes n::int and x::int
+ shows "pow integer_group x n = n * x"
+ by (simp add: int_pow_def2)
+
+lemma (in group) hom_integer_group_pow:
+ "x \<in> carrier G \<Longrightarrow> pow G x \<in> hom integer_group G"
+ by (rule homI) (auto simp: int_pow_mult)
+
+end
--- a/src/HOL/Algebra/Generated_Groups.thy Tue Apr 02 13:15:52 2019 +0200
+++ b/src/HOL/Algebra/Generated_Groups.thy Tue Apr 02 12:56:21 2019 +0100
@@ -452,6 +452,19 @@
lemma carrier_subgroup_generated: "carrier (subgroup_generated G S) = generate G (carrier G \<inter> S)"
by (auto simp: subgroup_generated_def)
+lemma (in group) subgroup_generated_subset_carrier_subset:
+ "S \<subseteq> carrier G \<Longrightarrow> S \<subseteq> carrier(subgroup_generated G S)"
+ by (simp add: Int_absorb1 carrier_subgroup_generated generate.incl subsetI)
+
+lemma (in group) subgroup_generated_minimal:
+ "\<lbrakk>subgroup H G; S \<subseteq> H\<rbrakk> \<Longrightarrow> carrier(subgroup_generated G S) \<subseteq> H"
+ by (simp add: carrier_subgroup_generated generate_subgroup_incl le_infI2)
+
+lemma (in group) carrier_subgroup_generated_subset:
+ "carrier (subgroup_generated G A) \<subseteq> 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)
@@ -520,7 +533,6 @@
"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) \<longleftrightarrow> subgroup H G \<and> H \<subseteq> carrier(subgroup_generated G B)"
(is "?lhs = ?rhs")
@@ -542,6 +554,9 @@
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 \<Rightarrow> nat \<Rightarrow> 'a)"
@@ -552,6 +567,19 @@
by force
qed
+lemma (in group) subgroup_generated2 [simp]: "subgroup_generated (subgroup_generated G S) S = subgroup_generated G S"
+proof -
+ have *: "\<And>A. carrier G \<inter> A \<subseteq> carrier (subgroup_generated (subgroup_generated G A) A)"
+ by (metis (no_types, hide_lams) 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, hide_lams) "*" 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 \<in> carrier (subgroup_generated G S)"
@@ -560,7 +588,7 @@
have "x [^] nat (- n) \<in> 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 (simp add: int_pow_def2 pow_subgroup_generated)
+ by (metis group.inv_subgroup_generated int_pow_def2 is_group pow_subgroup_generated)
qed
lemma kernel_from_subgroup_generated [simp]:
--- a/src/HOL/Algebra/Group.thy Tue Apr 02 13:15:52 2019 +0200
+++ b/src/HOL/Algebra/Group.thy Tue Apr 02 12:56:21 2019 +0100
@@ -471,12 +471,12 @@
proof -
have [simp]: "-i - j = -j - i" by simp
show ?thesis
- by (auto simp add: assms int_pow_def2 inv_solve_left inv_solve_right nat_add_distrib [symmetric] nat_pow_mult )
+ by (auto simp: assms int_pow_def2 inv_solve_left inv_solve_right nat_add_distrib [symmetric] nat_pow_mult)
qed
lemma (in group) int_pow_inv:
"x \<in> carrier G \<Longrightarrow> (inv x) [^] (i :: int) = inv (x [^] i)"
- by (simp add: nat_pow_inv int_pow_def2)
+ by (metis int_pow_def2 nat_pow_inv)
lemma (in group) int_pow_pow:
assumes "x \<in> carrier G"
@@ -873,6 +873,10 @@
"[|h \<in> hom G H; i \<in> hom H I|] ==> compose (carrier G) i h \<in> hom G I"
by (fastforce simp add: hom_def compose_def)
+lemma (in group) restrict_hom_iff [simp]:
+ "(\<lambda>x. if x \<in> carrier G then f x else g x) \<in> hom G H \<longleftrightarrow> f \<in> hom G H"
+ by (simp add: hom_def Pi_iff)
+
definition iso :: "_ => _ => ('a => 'b) set"
where "iso G H = {h. h \<in> hom G H \<and> bij_betw h (carrier G) (carrier H)}"
@@ -1582,4 +1586,6 @@
lemma (in group) r_cancel_one' [simp]: "x \<in> carrier G \<Longrightarrow> a \<in> carrier G \<Longrightarrow> x = a \<otimes> x \<longleftrightarrow> a = one G"
using r_cancel_one by fastforce
+declare pow_nat [simp] (*causes looping if added above, especially with int_pow_def2*)
+
end
--- a/src/HOL/Algebra/Multiplicative_Group.thy Tue Apr 02 13:15:52 2019 +0200
+++ b/src/HOL/Algebra/Multiplicative_Group.thy Tue Apr 02 12:56:21 2019 +0100
@@ -448,13 +448,12 @@
proof (cases "k < 0")
assume "\<not> k < 0"
hence "b = a [^] (nat k)"
- by (simp add: int_pow_def2 k)
+ by (simp add: k)
thus ?thesis by blast
next
assume "k < 0"
hence b: "b = inv (a [^] (nat (- k)))"
- using k int_pow_def2[of G] by auto
-
+ using k \<open>a \<in> carrier G\<close> by (auto simp: int_pow_neg)
obtain m where m: "ord a * m \<ge> nat (- k)"
by (metis assms mult.left_neutral mult_le_mono1 ord_ge_1)
hence "a [^] (ord a * m) = \<one>"