src/HOL/Algebra/Sylow.thy
author ballarin
Tue, 16 Dec 2008 21:10:53 +0100
changeset 29237 e90d9d51106b
parent 27717 21bbd410ba04
child 30198 922f944f03b2
permissions -rw-r--r--
More porting to new locales.
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
14706
71590b7733b7 tuned document;
wenzelm
parents: 14666
diff changeset
     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
71590b7733b7 tuned document;
wenzelm
parents: 14666
diff changeset
     8
text {*
71590b7733b7 tuned document;
wenzelm
parents: 14666
diff changeset
     9
  See also \cite{Kammueller-Paulson:1999}.
71590b7733b7 tuned document;
wenzelm
parents: 14666
diff changeset
    10
*}
71590b7733b7 tuned document;
wenzelm
parents: 14666
diff changeset
    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
2eaff69d3d10 removal of locale coset
paulson
parents: 14706
diff changeset
    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
13e9c402308b prime is a predicate now.
nipkow
parents: 16417
diff changeset
    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
2eaff69d3d10 removal of locale coset
paulson
parents: 14706
diff changeset
    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
65f8680c3f16 improved notation;
wenzelm
parents: 14651
diff changeset
    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
cf947d1ec5ff moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff changeset
    23
lemma (in sylow) RelM_refl: "refl calM RelM"
14666
65f8680c3f16 improved notation;
wenzelm
parents: 14651
diff changeset
    24
apply (auto simp add: refl_def RelM_def calM_def)
65f8680c3f16 improved notation;
wenzelm
parents: 14651
diff changeset
    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
65f8680c3f16 improved notation;
wenzelm
parents: 14651
diff changeset
    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)
cf947d1ec5ff moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff changeset
    43
apply (blast intro: RelM_refl RelM_sym RelM_trans)
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
2eaff69d3d10 removal of locale coset
paulson
parents: 14706
diff changeset
    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
2eaff69d3d10 removal of locale coset
paulson
parents: 14706
diff changeset
    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
65f8680c3f16 improved notation;
wenzelm
parents: 14651
diff changeset
    72
lemma (in sylow_central) exists_x_in_M1: "\<exists>x. x\<in>M1"
65f8680c3f16 improved notation;
wenzelm
parents: 14651
diff changeset
    73
apply (subgoal_tac "0 < card M1")
65f8680c3f16 improved notation;
wenzelm
parents: 14651
diff changeset
    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
2eaff69d3d10 removal of locale coset
paulson
parents: 14706
diff changeset
    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
65f8680c3f16 improved notation;
wenzelm
parents: 14651
diff changeset
    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
65f8680c3f16 improved notation;
wenzelm
parents: 14651
diff changeset
    96
        fix z assume zH: "z \<in> H"
65f8680c3f16 improved notation;
wenzelm
parents: 14651
diff changeset
    97
        show "m1 \<otimes> z \<in> M1"
65f8680c3f16 improved notation;
wenzelm
parents: 14651
diff changeset
    98
        proof -
65f8680c3f16 improved notation;
wenzelm
parents: 14651
diff changeset
    99
          from zH
65f8680c3f16 improved notation;
wenzelm
parents: 14651
diff changeset
   100
          have zG: "z \<in> carrier G" and M1zeq: "M1 #> z = M1"
65f8680c3f16 improved notation;
wenzelm
parents: 14651
diff changeset
   101
            by (auto simp add: H_def)
65f8680c3f16 improved notation;
wenzelm
parents: 14651
diff changeset
   102
          show ?thesis
65f8680c3f16 improved notation;
wenzelm
parents: 14651
diff changeset
   103
            by (rule subst [OF M1zeq], simp add: m1M zG rcosI)
65f8680c3f16 improved notation;
wenzelm
parents: 14651
diff changeset
   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
65f8680c3f16 improved notation;
wenzelm
parents: 14651
diff changeset
   116
apply (subgoal_tac "M \<noteq> {}")
65f8680c3f16 improved notation;
wenzelm
parents: 14651
diff changeset
   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
ad4d5365d9d8 went back to >0
nipkow
parents: 25134
diff changeset
   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
ad4d5365d9d8 went back to >0
nipkow
parents: 25134
diff changeset
   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
d584e32f7d46 removal of magmas and semigroups
paulson
parents: 14803
diff changeset
   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
d584e32f7d46 removal of magmas and semigroups
paulson
parents: 14803
diff changeset
   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
d584e32f7d46 removal of magmas and semigroups
paulson
parents: 14803
diff changeset
   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
65f8680c3f16 improved notation;
wenzelm
parents: 14651
diff changeset
   225
lemma ElemClassEquiv:
14963
d584e32f7d46 removal of magmas and semigroups
paulson
parents: 14803
diff changeset
   226
     "[| equiv A r; C \<in> A // r |] ==> \<forall>x \<in> C. \<forall>y \<in> C. (x,y)\<in>r"
d584e32f7d46 removal of magmas and semigroups
paulson
parents: 14803
diff changeset
   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
65f8680c3f16 improved notation;
wenzelm
parents: 14651
diff changeset
   236
lemmas (in sylow_central) M_elem_map_carrier =
65f8680c3f16 improved notation;
wenzelm
parents: 14651
diff changeset
   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
65f8680c3f16 improved notation;
wenzelm
parents: 14651
diff changeset
   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
d584e32f7d46 removal of magmas and semigroups
paulson
parents: 14803
diff changeset
   242
lemma (in sylow_central) M_funcset_rcosets_H:
d584e32f7d46 removal of magmas and semigroups
paulson
parents: 14803
diff changeset
   243
     "(%x:M. H #> (SOME g. g \<in> carrier G & M1 #> g = x)) \<in> M \<rightarrow> rcosets H"
d584e32f7d46 removal of magmas and semigroups
paulson
parents: 14803
diff changeset
   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
d584e32f7d46 removal of magmas and semigroups
paulson
parents: 14803
diff changeset
   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
d584e32f7d46 removal of magmas and semigroups
paulson
parents: 14803
diff changeset
   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
40b411ec05aa Adapted to encoding of sets as predicates
berghofe
parents: 25162
diff changeset
   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
d584e32f7d46 removal of magmas and semigroups
paulson
parents: 14803
diff changeset
   269
     "H1 \<in> rcosets H ==> \<exists>g. g \<in> carrier G & H #> g = H1"
d584e32f7d46 removal of magmas and semigroups
paulson
parents: 14803
diff changeset
   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
65f8680c3f16 improved notation;
wenzelm
parents: 14651
diff changeset
   272
lemmas (in sylow_central) H_elem_map_carrier =
65f8680c3f16 improved notation;
wenzelm
parents: 14651
diff changeset
   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
65f8680c3f16 improved notation;
wenzelm
parents: 14651
diff changeset
   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
65f8680c3f16 improved notation;
wenzelm
parents: 14651
diff changeset
   279
lemma EquivElemClass:
14963
d584e32f7d46 removal of magmas and semigroups
paulson
parents: 14803
diff changeset
   280
     "[|equiv A r; M \<in> A//r; M1\<in>M; (M1,M2) \<in> r |] ==> M2 \<in> M"
d584e32f7d46 removal of magmas and semigroups
paulson
parents: 14803
diff changeset
   281
by (unfold equiv_def quotient_def sym_def trans_def, blast)
d584e32f7d46 removal of magmas and semigroups
paulson
parents: 14803
diff changeset
   282
13870
cf947d1ec5ff moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff changeset
   283
14963
d584e32f7d46 removal of magmas and semigroups
paulson
parents: 14803
diff changeset
   284
lemma (in sylow_central) rcosets_H_funcset_M:
d584e32f7d46 removal of magmas and semigroups
paulson
parents: 14803
diff changeset
   285
  "(\<lambda>C \<in> rcosets H. M1 #> (@g. g \<in> carrier G \<and> H #> g = C)) \<in> rcosets H \<rightarrow> M"
d584e32f7d46 removal of magmas and semigroups
paulson
parents: 14803
diff changeset
   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
d584e32f7d46 removal of magmas and semigroups
paulson
parents: 14803
diff changeset
   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
d584e32f7d46 removal of magmas and semigroups
paulson
parents: 14803
diff changeset
   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
65f8680c3f16 improved notation;
wenzelm
parents: 14651
diff changeset
   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
2eaff69d3d10 removal of locale coset
paulson
parents: 14706
diff changeset
   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
d584e32f7d46 removal of magmas and semigroups
paulson
parents: 14803
diff changeset
   321
lemma (in sylow_central) cardMeqIndexH: "card(M) = card(rcosets H)"
14666
65f8680c3f16 improved notation;
wenzelm
parents: 14651
diff changeset
   322
apply (insert inj_M_GmodH inj_GmodH_M)
65f8680c3f16 improved notation;
wenzelm
parents: 14651
diff changeset
   323
apply (blast intro: card_bij finite_M H_is_subgroup
14963
d584e32f7d46 removal of magmas and semigroups
paulson
parents: 14803
diff changeset
   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
2eaff69d3d10 removal of locale coset
paulson
parents: 14706
diff changeset
   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
2eaff69d3d10 removal of locale coset
paulson
parents: 14706
diff changeset
   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
65f8680c3f16 improved notation;
wenzelm
parents: 14651
diff changeset
   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"
cf947d1ec5ff moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff changeset
   347
by (blast intro: le_anti_sym lemma_leq1 lemma_leq2)
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
65f8680c3f16 improved notation;
wenzelm
parents: 14651
diff changeset
   350
apply (cut_tac lemma_A1, clarify)
65f8680c3f16 improved notation;
wenzelm
parents: 14651
diff changeset
   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
65f8680c3f16 improved notation;
wenzelm
parents: 14651
diff changeset
   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
65f8680c3f16 improved notation;
wenzelm
parents: 14651
diff changeset
   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
13e9c402308b prime is a predicate now.
nipkow
parents: 16417
diff changeset
   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
65f8680c3f16 improved notation;
wenzelm
parents: 14651
diff changeset
   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
14963
d584e32f7d46 removal of magmas and semigroups
paulson
parents: 14803
diff changeset
   374