author  nipkow 
Fri, 13 Nov 2009 14:14:04 +0100  
changeset 33657  a4179bf442d1 
parent 31754  b5260f5272a4 
child 35849  b5522b51cb1e 
permissions  rwrr 
14706  1 
(* Title: HOL/Algebra/Sylow.thy 
13870
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset

2 
ID: $Id$ 
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset

3 
Author: Florian Kammueller, with new proofs by L C Paulson 
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset

4 
*) 
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset

5 

27717
21bbd410ba04
Generalised polynomial lemmas from cring to ring.
ballarin
parents:
26806
diff
changeset

6 
theory Sylow imports Coset Exponent begin 
13870
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset

7 

14706  8 
text {* 
9 
See also \cite{KammuellerPaulson:1999}. 

10 
*} 

11 

13870
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset

12 
text{*The combinatorial argument is in theory Exponent*} 
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset

13 

14747  14 
locale sylow = group + 
13870
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset

15 
fixes p and a and m and calM and RelM 
16663  16 
assumes prime_p: "prime p" 
13870
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset

17 
and order_G: "order(G) = (p^a) * m" 
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset

18 
and finite_G [iff]: "finite (carrier G)" 
14747  19 
defines "calM == {s. s \<subseteq> carrier(G) & card(s) = p^a}" 
13870
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset

20 
and "RelM == {(N1,N2). N1 \<in> calM & N2 \<in> calM & 
14666  21 
(\<exists>g \<in> carrier(G). N1 = (N2 #> g) )}" 
13870
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset

22 

30198  23 
lemma (in sylow) RelM_refl_on: "refl_on calM RelM" 
24 
apply (auto simp add: refl_on_def RelM_def calM_def) 

14666  25 
apply (blast intro!: coset_mult_one [symmetric]) 
13870
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset

26 
done 
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset

27 

cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset

28 
lemma (in sylow) RelM_sym: "sym RelM" 
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset

29 
proof (unfold sym_def RelM_def, clarify) 
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset

30 
fix y g 
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset

31 
assume "y \<in> calM" 
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset

32 
and g: "g \<in> carrier G" 
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset

33 
hence "y = y #> g #> (inv g)" by (simp add: coset_mult_assoc calM_def) 
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset

34 
thus "\<exists>g'\<in>carrier G. y = y #> g #> g'" 
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset

35 
by (blast intro: g inv_closed) 
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset

36 
qed 
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset

37 

cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset

38 
lemma (in sylow) RelM_trans: "trans RelM" 
14666  39 
by (auto simp add: trans_def RelM_def calM_def coset_mult_assoc) 
13870
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset

40 

cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset

41 
lemma (in sylow) RelM_equiv: "equiv calM RelM" 
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset

42 
apply (unfold equiv_def) 
30198  43 
apply (blast intro: RelM_refl_on RelM_sym RelM_trans) 
13870
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset

44 
done 
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset

45 

14747  46 
lemma (in sylow) M_subset_calM_prep: "M' \<in> calM // RelM ==> M' \<subseteq> calM" 
13870
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset

47 
apply (unfold RelM_def) 
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset

48 
apply (blast elim!: quotientE) 
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset

49 
done 
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset

50 

20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
16663
diff
changeset

51 

13870
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset

52 
subsection{*Main Part of the Proof*} 
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset

53 

cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset

54 
locale sylow_central = sylow + 
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset

55 
fixes H and M1 and M 
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset

56 
assumes M_in_quot: "M \<in> calM // RelM" 
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset

57 
and not_dvd_M: "~(p ^ Suc(exponent p m) dvd card(M))" 
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset

58 
and M1_in_M: "M1 \<in> M" 
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset

59 
defines "H == {g. g\<in>carrier G & M1 #> g = M1}" 
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset

60 

14747  61 
lemma (in sylow_central) M_subset_calM: "M \<subseteq> calM" 
13870
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset

62 
by (rule M_in_quot [THEN M_subset_calM_prep]) 
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset

63 

cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset

64 
lemma (in sylow_central) card_M1: "card(M1) = p^a" 
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset

65 
apply (cut_tac M_subset_calM M1_in_M) 
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset

66 
apply (simp add: calM_def, blast) 
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset

67 
done 
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset

68 

cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset

69 
lemma card_nonempty: "0 < card(S) ==> S \<noteq> {}" 
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset

70 
by force 
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset

71 

14666  72 
lemma (in sylow_central) exists_x_in_M1: "\<exists>x. x\<in>M1" 
73 
apply (subgoal_tac "0 < card M1") 

74 
apply (blast dest: card_nonempty) 

13870
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset

75 
apply (cut_tac prime_p [THEN prime_imp_one_less]) 
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset

76 
apply (simp (no_asm_simp) add: card_M1) 
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset

77 
done 
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset

78 

14747  79 
lemma (in sylow_central) M1_subset_G [simp]: "M1 \<subseteq> carrier G" 
13870
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset

80 
apply (rule subsetD [THEN PowD]) 
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset

81 
apply (rule_tac [2] M1_in_M) 
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset

82 
apply (rule M_subset_calM [THEN subset_trans]) 
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset

83 
apply (auto simp add: calM_def) 
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset

84 
done 
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset

85 

cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset

86 
lemma (in sylow_central) M1_inj_H: "\<exists>f \<in> H\<rightarrow>M1. inj_on f H" 
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset

87 
proof  
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset

88 
from exists_x_in_M1 obtain m1 where m1M: "m1 \<in> M1".. 
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset

89 
have m1G: "m1 \<in> carrier G" by (simp add: m1M M1_subset_G [THEN subsetD]) 
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset

90 
show ?thesis 
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset

91 
proof 
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset

92 
show "inj_on (\<lambda>z\<in>H. m1 \<otimes> z) H" 
14666  93 
by (simp add: inj_on_def l_cancel [of m1 x y, THEN iffD1] H_def m1G) 
13870
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset

94 
show "restrict (op \<otimes> m1) H \<in> H \<rightarrow> M1" 
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset

95 
proof (rule restrictI) 
14666  96 
fix z assume zH: "z \<in> H" 
97 
show "m1 \<otimes> z \<in> M1" 

98 
proof  

99 
from zH 

100 
have zG: "z \<in> carrier G" and M1zeq: "M1 #> z = M1" 

101 
by (auto simp add: H_def) 

102 
show ?thesis 

103 
by (rule subst [OF M1zeq], simp add: m1M zG rcosI) 

104 
qed 

13870
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset

105 
qed 
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset

106 
qed 
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset

107 
qed 
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset

108 

cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset

109 

cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset

110 
subsection{*Discharging the Assumptions of @{text sylow_central}*} 
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset

111 

cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset

112 
lemma (in sylow) EmptyNotInEquivSet: "{} \<notin> calM // RelM" 
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset

113 
by (blast elim!: quotientE dest: RelM_equiv [THEN equiv_class_self]) 
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset

114 

cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset

115 
lemma (in sylow) existsM1inM: "M \<in> calM // RelM ==> \<exists>M1. M1 \<in> M" 
14666  116 
apply (subgoal_tac "M \<noteq> {}") 
117 
apply blast 

13870
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset

118 
apply (cut_tac EmptyNotInEquivSet, blast) 
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset

119 
done 
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset

120 

cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset

121 
lemma (in sylow) zero_less_o_G: "0 < order(G)" 
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset

122 
apply (unfold order_def) 
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset

123 
apply (blast intro: one_closed zero_less_card_empty) 
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset

124 
done 
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset

125 

25162  126 
lemma (in sylow) zero_less_m: "m > 0" 
13870
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset

127 
apply (cut_tac zero_less_o_G) 
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset

128 
apply (simp add: order_G) 
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset

129 
done 
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset

130 

cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset

131 
lemma (in sylow) card_calM: "card(calM) = (p^a) * m choose p^a" 
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset

132 
by (simp add: calM_def n_subsets order_G [symmetric] order_def) 
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset

133 

25162  134 
lemma (in sylow) zero_less_card_calM: "card calM > 0" 
13870
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset

135 
by (simp add: card_calM zero_less_binomial le_extend_mult zero_less_m) 
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset

136 

cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset

137 
lemma (in sylow) max_p_div_calM: 
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset

138 
"~ (p ^ Suc(exponent p m) dvd card(calM))" 
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset

139 
apply (subgoal_tac "exponent p m = exponent p (card calM) ") 
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset

140 
apply (cut_tac zero_less_card_calM prime_p) 
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset

141 
apply (force dest: power_Suc_exponent_Not_dvd) 
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset

142 
apply (simp add: card_calM zero_less_m [THEN const_p_fac]) 
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset

143 
done 
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset

144 

cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset

145 
lemma (in sylow) finite_calM: "finite calM" 
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset

146 
apply (unfold calM_def) 
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset

147 
apply (rule_tac B = "Pow (carrier G) " in finite_subset) 
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset

148 
apply auto 
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset

149 
done 
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset

150 

cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset

151 
lemma (in sylow) lemma_A1: 
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset

152 
"\<exists>M \<in> calM // RelM. ~ (p ^ Suc(exponent p m) dvd card(M))" 
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset

153 
apply (rule max_p_div_calM [THEN contrapos_np]) 
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset

154 
apply (simp add: finite_calM equiv_imp_dvd_card [OF _ RelM_equiv]) 
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset

155 
done 
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset

156 

cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset

157 

cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset

158 
subsubsection{*Introduction and Destruct Rules for @{term H}*} 
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset

159 

cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset

160 
lemma (in sylow_central) H_I: "[g \<in> carrier G; M1 #> g = M1] ==> g \<in> H" 
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset

161 
by (simp add: H_def) 
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset

162 

cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset

163 
lemma (in sylow_central) H_into_carrier_G: "x \<in> H ==> x \<in> carrier G" 
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset

164 
by (simp add: H_def) 
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset

165 

cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset

166 
lemma (in sylow_central) in_H_imp_eq: "g : H ==> M1 #> g = M1" 
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset

167 
by (simp add: H_def) 
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset

168 

cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset

169 
lemma (in sylow_central) H_m_closed: "[ x\<in>H; y\<in>H] ==> x \<otimes> y \<in> H" 
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset

170 
apply (unfold H_def) 
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset

171 
apply (simp add: coset_mult_assoc [symmetric] m_closed) 
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset

172 
done 
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset

173 

cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset

174 
lemma (in sylow_central) H_not_empty: "H \<noteq> {}" 
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset

175 
apply (simp add: H_def) 
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset

176 
apply (rule exI [of _ \<one>], simp) 
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset

177 
done 
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset

178 

cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset

179 
lemma (in sylow_central) H_is_subgroup: "subgroup H G" 
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset

180 
apply (rule subgroupI) 
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset

181 
apply (rule subsetI) 
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset

182 
apply (erule H_into_carrier_G) 
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset

183 
apply (rule H_not_empty) 
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset

184 
apply (simp add: H_def, clarify) 
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset

185 
apply (erule_tac P = "%z. ?lhs(z) = M1" in subst) 
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset

186 
apply (simp add: coset_mult_assoc ) 
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset

187 
apply (blast intro: H_m_closed) 
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset

188 
done 
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset

189 

cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset

190 

cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset

191 
lemma (in sylow_central) rcosetGM1g_subset_G: 
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset

192 
"[ g \<in> carrier G; x \<in> M1 #> g ] ==> x \<in> carrier G" 
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset

193 
by (blast intro: M1_subset_G [THEN r_coset_subset_G, THEN subsetD]) 
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset

194 

cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset

195 
lemma (in sylow_central) finite_M1: "finite M1" 
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset

196 
by (rule finite_subset [OF M1_subset_G finite_G]) 
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset

197 

cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset

198 
lemma (in sylow_central) finite_rcosetGM1g: "g\<in>carrier G ==> finite (M1 #> g)" 
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset

199 
apply (rule finite_subset) 
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset

200 
apply (rule subsetI) 
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset

201 
apply (erule rcosetGM1g_subset_G, assumption) 
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset

202 
apply (rule finite_G) 
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset

203 
done 
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset

204 

cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset

205 
lemma (in sylow_central) M1_cardeq_rcosetGM1g: 
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset

206 
"g \<in> carrier G ==> card(M1 #> g) = card(M1)" 
14963  207 
by (simp (no_asm_simp) add: M1_subset_G card_cosets_equal rcosetsI) 
13870
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset

208 

cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset

209 
lemma (in sylow_central) M1_RelM_rcosetGM1g: 
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset

210 
"g \<in> carrier G ==> (M1, M1 #> g) \<in> RelM" 
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset

211 
apply (simp (no_asm) add: RelM_def calM_def card_M1 M1_subset_G) 
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset

212 
apply (rule conjI) 
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset

213 
apply (blast intro: rcosetGM1g_subset_G) 
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset

214 
apply (simp (no_asm_simp) add: card_M1 M1_cardeq_rcosetGM1g) 
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset

215 
apply (rule bexI [of _ "inv g"]) 
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset

216 
apply (simp_all add: coset_mult_assoc M1_subset_G) 
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset

217 
done 
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset

218 

cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset

219 

14963  220 
subsection{*Equal Cardinalities of @{term M} and the Set of Cosets*} 
13870
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset

221 

14963  222 
text{*Injections between @{term M} and @{term "rcosets\<^bsub>G\<^esub> H"} show that 
13870
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset

223 
their cardinalities are equal.*} 
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset

224 

14666  225 
lemma ElemClassEquiv: 
14963  226 
"[ equiv A r; C \<in> A // r ] ==> \<forall>x \<in> C. \<forall>y \<in> C. (x,y)\<in>r" 
227 
by (unfold equiv_def quotient_def sym_def trans_def, blast) 

13870
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset

228 

cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset

229 
lemma (in sylow_central) M_elem_map: 
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset

230 
"M2 \<in> M ==> \<exists>g. g \<in> carrier G & M1 #> g = M2" 
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset

231 
apply (cut_tac M1_in_M M_in_quot [THEN RelM_equiv [THEN ElemClassEquiv]]) 
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset

232 
apply (simp add: RelM_def) 
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset

233 
apply (blast dest!: bspec) 
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset

234 
done 
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset

235 

14666  236 
lemmas (in sylow_central) M_elem_map_carrier = 
237 
M_elem_map [THEN someI_ex, THEN conjunct1] 

13870
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset

238 

cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset

239 
lemmas (in sylow_central) M_elem_map_eq = 
14666  240 
M_elem_map [THEN someI_ex, THEN conjunct2] 
13870
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset

241 

14963  242 
lemma (in sylow_central) M_funcset_rcosets_H: 
243 
"(%x:M. H #> (SOME g. g \<in> carrier G & M1 #> g = x)) \<in> M \<rightarrow> rcosets H" 

244 
apply (rule rcosetsI [THEN restrictI]) 

13870
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset

245 
apply (rule H_is_subgroup [THEN subgroup.subset]) 
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset

246 
apply (erule M_elem_map_carrier) 
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset

247 
done 
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset

248 

14963  249 
lemma (in sylow_central) inj_M_GmodH: "\<exists>f \<in> M\<rightarrow>rcosets H. inj_on f M" 
13870
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset

250 
apply (rule bexI) 
14963  251 
apply (rule_tac [2] M_funcset_rcosets_H) 
13870
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset

252 
apply (rule inj_onI, simp) 
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset

253 
apply (rule trans [OF _ M_elem_map_eq]) 
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset

254 
prefer 2 apply assumption 
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset

255 
apply (rule M_elem_map_eq [symmetric, THEN trans], assumption) 
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset

256 
apply (rule coset_mult_inv1) 
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset

257 
apply (erule_tac [2] M_elem_map_carrier)+ 
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset

258 
apply (rule_tac [2] M1_subset_G) 
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset

259 
apply (rule coset_join1 [THEN in_H_imp_eq]) 
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset

260 
apply (rule_tac [3] H_is_subgroup) 
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset

261 
prefer 2 apply (blast intro: m_closed M_elem_map_carrier inv_closed) 
26806  262 
apply (simp add: coset_mult_inv2 H_def M_elem_map_carrier subset_eq) 
13870
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset

263 
done 
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset

264 

cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset

265 

20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
16663
diff
changeset

266 
subsubsection{*The Opposite Injection*} 
13870
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset

267 

cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset

268 
lemma (in sylow_central) H_elem_map: 
14963  269 
"H1 \<in> rcosets H ==> \<exists>g. g \<in> carrier G & H #> g = H1" 
270 
by (auto simp add: RCOSETS_def) 

13870
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset

271 

14666  272 
lemmas (in sylow_central) H_elem_map_carrier = 
273 
H_elem_map [THEN someI_ex, THEN conjunct1] 

13870
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset

274 

cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset

275 
lemmas (in sylow_central) H_elem_map_eq = 
14666  276 
H_elem_map [THEN someI_ex, THEN conjunct2] 
13870
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset

277 

cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset

278 

14666  279 
lemma EquivElemClass: 
14963  280 
"[equiv A r; M \<in> A//r; M1\<in>M; (M1,M2) \<in> r ] ==> M2 \<in> M" 
281 
by (unfold equiv_def quotient_def sym_def trans_def, blast) 

282 

13870
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset

283 

14963  284 
lemma (in sylow_central) rcosets_H_funcset_M: 
285 
"(\<lambda>C \<in> rcosets H. M1 #> (@g. g \<in> carrier G \<and> H #> g = C)) \<in> rcosets H \<rightarrow> M" 

286 
apply (simp add: RCOSETS_def) 

13870
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset

287 
apply (fast intro: someI2 
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset

288 
intro!: restrictI M1_in_M 
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset

289 
EquivElemClass [OF RelM_equiv M_in_quot _ M1_RelM_rcosetGM1g]) 
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset

290 
done 
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset

291 

cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset

292 
text{*close to a duplicate of @{text inj_M_GmodH}*} 
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset

293 
lemma (in sylow_central) inj_GmodH_M: 
14963  294 
"\<exists>g \<in> rcosets H\<rightarrow>M. inj_on g (rcosets H)" 
13870
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset

295 
apply (rule bexI) 
14963  296 
apply (rule_tac [2] rcosets_H_funcset_M) 
13870
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset

297 
apply (rule inj_onI) 
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset

298 
apply (simp) 
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset

299 
apply (rule trans [OF _ H_elem_map_eq]) 
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset

300 
prefer 2 apply assumption 
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset

301 
apply (rule H_elem_map_eq [symmetric, THEN trans], assumption) 
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset

302 
apply (rule coset_mult_inv1) 
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset

303 
apply (erule_tac [2] H_elem_map_carrier)+ 
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset

304 
apply (rule_tac [2] H_is_subgroup [THEN subgroup.subset]) 
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset

305 
apply (rule coset_join2) 
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset

306 
apply (blast intro: m_closed inv_closed H_elem_map_carrier) 
14666  307 
apply (rule H_is_subgroup) 
13870
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset

308 
apply (simp add: H_I coset_mult_inv2 M1_subset_G H_elem_map_carrier) 
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset

309 
done 
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset

310 

14747  311 
lemma (in sylow_central) calM_subset_PowG: "calM \<subseteq> Pow(carrier G)" 
13870
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset

312 
by (auto simp add: calM_def) 
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset

313 

cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset

314 

cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset

315 
lemma (in sylow_central) finite_M: "finite M" 
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset

316 
apply (rule finite_subset) 
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset

317 
apply (rule M_subset_calM [THEN subset_trans]) 
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset

318 
apply (rule calM_subset_PowG, blast) 
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset

319 
done 
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset

320 

14963  321 
lemma (in sylow_central) cardMeqIndexH: "card(M) = card(rcosets H)" 
14666  322 
apply (insert inj_M_GmodH inj_GmodH_M) 
323 
apply (blast intro: card_bij finite_M H_is_subgroup 

14963  324 
rcosets_subset_PowG [THEN finite_subset] 
13870
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset

325 
finite_Pow_iff [THEN iffD2]) 
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset

326 
done 
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset

327 

cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset

328 
lemma (in sylow_central) index_lem: "card(M) * card(H) = order(G)" 
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset

329 
by (simp add: cardMeqIndexH lagrange H_is_subgroup) 
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset

330 

14747  331 
lemma (in sylow_central) lemma_leq1: "p^a \<le> card(H)" 
13870
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset

332 
apply (rule dvd_imp_le) 
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset

333 
apply (rule div_combine [OF prime_p not_dvd_M]) 
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset

334 
prefer 2 apply (blast intro: subgroup.finite_imp_card_positive H_is_subgroup) 
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset

335 
apply (simp add: index_lem order_G power_add mult_dvd_mono power_exponent_dvd 
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset

336 
zero_less_m) 
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset

337 
done 
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset

338 

14747  339 
lemma (in sylow_central) lemma_leq2: "card(H) \<le> p^a" 
13870
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset

340 
apply (subst card_M1 [symmetric]) 
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset

341 
apply (cut_tac M1_inj_H) 
14666  342 
apply (blast intro!: M1_subset_G intro: 
13870
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset

343 
card_inj H_into_carrier_G finite_subset [OF _ finite_G]) 
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset

344 
done 
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset

345 

cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset

346 
lemma (in sylow_central) card_H_eq: "card(H) = p^a" 
33657  347 
by (blast intro: le_antisym lemma_leq1 lemma_leq2) 
13870
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset

348 

cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset

349 
lemma (in sylow) sylow_thm: "\<exists>H. subgroup H G & card(H) = p^a" 
14666  350 
apply (cut_tac lemma_A1, clarify) 
351 
apply (frule existsM1inM, clarify) 

13870
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset

352 
apply (subgoal_tac "sylow_central G p a m M1 M") 
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset

353 
apply (blast dest: sylow_central.H_is_subgroup sylow_central.card_H_eq) 
14666  354 
apply (simp add: sylow_central_def sylow_central_axioms_def prems) 
13870
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset

355 
done 
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset

356 

cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset

357 
text{*Needed because the locale's automatic definition refers to 
14666  358 
@{term "semigroup G"} and @{term "group_axioms G"} rather than 
13870
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset

359 
simply to @{term "group G"}.*} 
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset

360 
lemma sylow_eq: "sylow G p a m = (group G & sylow_axioms G p a m)" 
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset

361 
by (simp add: sylow_def group_def) 
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset

362 

20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
16663
diff
changeset

363 

0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
16663
diff
changeset

364 
subsection {* Sylow's Theorem *} 
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
16663
diff
changeset

365 

13870
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset

366 
theorem sylow_thm: 
16663  367 
"[ prime p; group(G); order(G) = (p^a) * m; finite (carrier G)] 
13870
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset

368 
==> \<exists>H. subgroup H G & card(H) = p^a" 
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset

369 
apply (rule sylow.sylow_thm [of G p a m]) 
14666  370 
apply (simp add: sylow_eq sylow_axioms_def) 
13870
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset

371 
done 
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset

372 

cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset

373 
end 