src/HOL/Algebra/More_Group.thy
 author wenzelm Tue Oct 10 19:23:03 2017 +0200 (2017-10-10) changeset 66831 29ea2b900a05 parent 66760 d44ea023ac09 child 67341 df79ef3b3a41 permissions -rw-r--r--
tuned: each session has at most one defining entry;
1 (*  Title:      HOL/Algebra/More_Group.thy
2     Author:     Jeremy Avigad
3 *)
5 section \<open>More on groups\<close>
7 theory More_Group
8   imports Ring
9 begin
11 text \<open>
12   Show that the units in any monoid give rise to a group.
14   The file Residues.thy provides some infrastructure to use
15   facts about the unit group within the ring locale.
16 \<close>
18 definition units_of :: "('a, 'b) monoid_scheme \<Rightarrow> 'a monoid"
19   where "units_of G =
20     \<lparr>carrier = Units G, Group.monoid.mult = Group.monoid.mult G, one  = one G\<rparr>"
22 lemma (in monoid) units_group: "group (units_of G)"
23   apply (unfold units_of_def)
24   apply (rule groupI)
25       apply auto
26    apply (subst m_assoc)
27       apply auto
28   apply (rule_tac x = "inv x" in bexI)
29    apply auto
30   done
32 lemma (in comm_monoid) units_comm_group: "comm_group (units_of G)"
33   apply (rule group.group_comm_groupI)
34    apply (rule units_group)
35   apply (insert comm_monoid_axioms)
36   apply (unfold units_of_def Units_def comm_monoid_def comm_monoid_axioms_def)
37   apply auto
38   done
40 lemma units_of_carrier: "carrier (units_of G) = Units G"
41   by (auto simp: units_of_def)
43 lemma units_of_mult: "mult (units_of G) = mult G"
44   by (auto simp: units_of_def)
46 lemma units_of_one: "one (units_of G) = one G"
47   by (auto simp: units_of_def)
49 lemma (in monoid) units_of_inv: "x \<in> Units G \<Longrightarrow> m_inv (units_of G) x = m_inv G x"
50   apply (rule sym)
51   apply (subst m_inv_def)
52   apply (rule the1_equality)
53    apply (rule ex_ex1I)
54     apply (subst (asm) Units_def)
55     apply auto
56      apply (erule inv_unique)
57         apply auto
58     apply (rule Units_closed)
59     apply (simp_all only: units_of_carrier [symmetric])
60     apply (insert units_group)
61     apply auto
62    apply (subst units_of_mult [symmetric])
63    apply (subst units_of_one [symmetric])
64    apply (erule group.r_inv, assumption)
65   apply (subst units_of_mult [symmetric])
66   apply (subst units_of_one [symmetric])
67   apply (erule group.l_inv, assumption)
68   done
70 lemma (in group) inj_on_const_mult: "a \<in> carrier G \<Longrightarrow> inj_on (\<lambda>x. a \<otimes> x) (carrier G)"
71   unfolding inj_on_def by auto
73 lemma (in group) surj_const_mult: "a \<in> carrier G \<Longrightarrow> (\<lambda>x. a \<otimes> x) ` carrier G = carrier G"
74   apply (auto simp add: image_def)
75   apply (rule_tac x = "(m_inv G a) \<otimes> x" in bexI)
76   apply auto
77 (* auto should get this. I suppose we need "comm_monoid_simprules"
78    for ac_simps rewriting. *)
79   apply (subst m_assoc [symmetric])
80   apply auto
81   done
83 lemma (in group) l_cancel_one [simp]: "x \<in> carrier G \<Longrightarrow> a \<in> carrier G \<Longrightarrow> x \<otimes> a = x \<longleftrightarrow> a = one G"
84   apply auto
85   apply (subst l_cancel [symmetric])
86      prefer 4
87      apply (erule ssubst)
88      apply auto
89   done
91 lemma (in group) r_cancel_one [simp]: "x \<in> carrier G \<Longrightarrow> a \<in> carrier G \<Longrightarrow> a \<otimes> x = x \<longleftrightarrow> a = one G"
92   apply auto
93   apply (subst r_cancel [symmetric])
94      prefer 4
95      apply (erule ssubst)
96      apply auto
97   done
99 (* Is there a better way to do this? *)
100 lemma (in group) l_cancel_one' [simp]: "x \<in> carrier G \<Longrightarrow> a \<in> carrier G \<Longrightarrow> x = x \<otimes> a \<longleftrightarrow> a = one G"
101   apply (subst eq_commute)
102   apply simp
103   done
105 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"
106   apply (subst eq_commute)
107   apply simp
108   done
110 (* This should be generalized to arbitrary groups, not just commutative
111    ones, using Lagrange's theorem. *)
113 lemma (in comm_group) power_order_eq_one:
114   assumes fin [simp]: "finite (carrier G)"
115     and a [simp]: "a \<in> carrier G"
116   shows "a (^) card(carrier G) = one G"
117 proof -
118   have "(\<Otimes>x\<in>carrier G. x) = (\<Otimes>x\<in>carrier G. a \<otimes> x)"
119     by (subst (2) finprod_reindex [symmetric],
120       auto simp add: Pi_def inj_on_const_mult surj_const_mult)
121   also have "\<dots> = (\<Otimes>x\<in>carrier G. a) \<otimes> (\<Otimes>x\<in>carrier G. x)"
122     by (auto simp add: finprod_multf Pi_def)
123   also have "(\<Otimes>x\<in>carrier G. a) = a (^) card(carrier G)"
124     by (auto simp add: finprod_const)
125   finally show ?thesis
126 (* uses the preceeding lemma *)
127     by auto
128 qed
130 end