Quellcode-Bibliothek

^© Kompilation durch diese Firma

[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]

Datei: Sylow.thy Sprache: Isabelle

Original von: Isabelle^©

(*  Title:      HOL/Algebra/Sylow.thy
    Author:     Florian Kammueller, with new proofs by L C Paulson
*)

theory Sylow
  imports Coset Exponent
begin

text \<open>See also @{cite "Kammueller-Paulson:1999"}.\<close>

text \<open>The combinatorial argument is in theory \<open>Exponent\<close>.\<close>

lemma le_extend_mult: "\0 < c; a \ b\ \ a \ b * c"
  for c :: nat
  by (metis divisors_zero dvd_triv_left leI less_le_trans nat_dvd_not_less zero_less_iff_neq_zero)

locale sylow = group +
  fixes p and a and m and calM and RelM
  assumes prime_p: "prime p"
    and order_G: "order G = (p^a) * m"
    and finite_G[iff]: "finite (carrier G)"
  defines "calM \ {s. s \ carrier G \ card s = p^a}"
    and "RelM \ {(N1, N2). N1 \ calM \ N2 \ calM \ (\g \ carrier G. N1 = N2 #> g)}"
begin

lemma RelM_refl_on: "refl_on calM RelM"
  by (auto simp: refl_on_def RelM_def calM_def) (blast intro!: coset_mult_one [symmetric])

lemma RelM_sym: "sym RelM"
proof (unfold sym_def RelM_def, clarify)
  fix y g
  assume "y \ calM"
    and g: "g \ carrier G"
  then have "y = y #> g #> (inv g)"
    by (simp add: coset_mult_assoc calM_def)
  then show "\g'\carrier G. y = y #> g #> g'"
    by (blast intro: g)
qed

lemma RelM_trans: "trans RelM"
  by (auto simp add: trans_def RelM_def calM_def coset_mult_assoc)

lemma RelM_equiv: "equiv calM RelM"
  unfolding equiv_def by (blast intro: RelM_refl_on RelM_sym RelM_trans)

lemma M_subset_calM_prep: "M' \ calM // RelM \ M' \ calM"
  unfolding RelM_def by (blast elim!: quotientE)

end

subsection \<open>Main Part of the Proof\<close>

locale sylow_central = sylow +
  fixes H and M1 and M
  assumes M_in_quot: "M \ calM // RelM"
    and not_dvd_M: "\ (p ^ Suc (multiplicity p m) dvd card M)"
    and M1_in_M: "M1 \ M"
  defines "H \ {g. g \ carrier G \ M1 #> g = M1}"
begin

lemma M_subset_calM: "M \ calM"
  by (rule M_in_quot [THEN M_subset_calM_prep])

lemma card_M1: "card M1 = p^a"
  using M1_in_M M_subset_calM calM_def by blast

lemma exists_x_in_M1: "\x. x \ M1"
  using prime_p [THEN prime_gt_Suc_0_nat] card_M1
  by (metis Suc_lessD card_eq_0_iff empty_subsetI equalityI gr_implies_not0 nat_zero_less_power_iff subsetI)

lemma M1_subset_G [simp]: "M1 \ carrier G"
  using M1_in_M M_subset_calM calM_def mem_Collect_eq subsetCE by blast

lemma M1_inj_H: "\f \ H\M1. inj_on f H"
proof -
  from exists_x_in_M1 obtain m1 where m1M: "m1 \ M1"..
  have m1: "m1 \ carrier G"
    by (simp add: m1M M1_subset_G [THEN subsetD])
  show ?thesis
  proof
    show "inj_on (\z\H. m1 \ z) H"
      by (simp add: H_def inj_on_def m1)
    show "restrict ((\) m1) H \ H \ M1"
    proof (rule restrictI)
      fix z
      assume zH: "z \ H"
      show "m1 \ z \ M1"
      proof -
        from zH
        have zG: "z \ carrier G" and M1zeq: "M1 #> z = M1"
          by (auto simp add: H_def)
        show ?thesis
          by (rule subst [OF M1zeq]) (simp add: m1M zG rcosI)
      qed
    qed
  qed
qed

end

subsection \<open>Discharging the Assumptions of \<open>sylow_central\<close>\<close>

context sylow
begin

lemma EmptyNotInEquivSet: "{} \ calM // RelM"
  by (blast elim!: quotientE dest: RelM_equiv [THEN equiv_class_self])

lemma existsM1inM: "M \ calM // RelM \ \M1. M1 \ M"
  using RelM_equiv equiv_Eps_in by blast

lemma zero_less_o_G: "0 < order G"
  by (simp add: order_def card_gt_0_iff carrier_not_empty)

lemma zero_less_m: "m > 0"
  using zero_less_o_G by (simp add: order_G)

lemma card_calM: "card calM = (p^a) * m choose p^a"
  by (simp add: calM_def n_subsets order_G [symmetric] order_def)

lemma zero_less_card_calM: "card calM > 0"
  by (simp add: card_calM zero_less_binomial le_extend_mult zero_less_m)

lemma max_p_div_calM: "\ (p ^ Suc (multiplicity p m) dvd card calM)"
proof
  assume "p ^ Suc (multiplicity p m) dvd card calM"
  with zero_less_card_calM prime_p
  have "Suc (multiplicity p m) \ multiplicity p (card calM)"
    by (intro multiplicity_geI) auto
  then have "multiplicity p m < multiplicity p (card calM)" by simp
  also have "multiplicity p m = multiplicity p (card calM)"
    by (simp add: const_p_fac prime_p zero_less_m card_calM)
  finally show False by simp
qed

lemma finite_calM: "finite calM"
  unfolding calM_def by (rule finite_subset [where B = "Pow (carrier G)"]) auto

lemma lemma_A1: "\M \ calM // RelM. \ (p ^ Suc (multiplicity p m) dvd card M)"
  using RelM_equiv equiv_imp_dvd_card finite_calM max_p_div_calM by blast

end

subsubsection \<open>Introduction and Destruct Rules for \<open>H\<close>\<close>

context sylow_central
begin

lemma H_I: "\g \ carrier G; M1 #> g = M1\ \ g \ H"
  by (simp add: H_def)

lemma H_into_carrier_G: "x \ H \ x \ carrier G"
  by (simp add: H_def)

lemma in_H_imp_eq: "g \ H \ M1 #> g = M1"
  by (simp add: H_def)

lemma H_m_closed: "\x \ H; y \ H\ \ x \ y \ H"
  by (simp add: H_def coset_mult_assoc [symmetric])

lemma H_not_empty: "H \ {}"
  by (force simp add: H_def intro: exI [of _ \<one>])

lemma H_is_subgroup: "subgroup H G"
proof (rule subgroupI)
  show "H \ carrier G"
    using H_into_carrier_G by blast
  show "\a. a \ H \ inv a \ H"
    by (metis H_I H_into_carrier_G H_m_closed M1_subset_G Units_eq Units_inv_closed Units_inv_inv coset_mult_inv1 in_H_imp_eq)
  show "\a b. \a \ H; b \ H\ \ a \ b \ H"
    by (blast intro: H_m_closed)
qed (use H_not_empty in auto)

lemma rcosetGM1g_subset_G: "\g \ carrier G; x \ M1 #> g\ \ x \ carrier G"
  by (blast intro: M1_subset_G [THEN r_coset_subset_G, THEN subsetD])

lemma finite_M1: "finite M1"
  by (rule finite_subset [OF M1_subset_G finite_G])

lemma finite_rcosetGM1g: "g \ carrier G \ finite (M1 #> g)"
  using rcosetGM1g_subset_G finite_G M1_subset_G cosets_finite rcosetsI by blast

lemma M1_cardeq_rcosetGM1g: "g \ carrier G \ card (M1 #> g) = card M1"
  by (metis M1_subset_G card_rcosets_equal rcosetsI)

lemma M1_RelM_rcosetGM1g:
  assumes "g \ carrier G"
  shows "(M1, M1 #> g) \ RelM"
proof -
  have "M1 #> g \ carrier G"
    by (simp add: assms r_coset_subset_G)
  moreover have "card (M1 #> g) = p ^ a"
    using assms by (simp add: card_M1 M1_cardeq_rcosetGM1g)
  moreover have "\h\carrier G. M1 = M1 #> g #> h"
    by (metis assms M1_subset_G coset_mult_assoc coset_mult_one r_inv_ex)
  ultimately show ?thesis
    by (simp add: RelM_def calM_def card_M1)
qed

end

subsection \<open>Equal Cardinalities of \<open>M\<close> and the Set of Cosets\<close>

text \<open>Injections between \<^term>\<open>M\<close> and \<^term>\<open>rcosets\<^bsub>G\<^esub> H\<close> show that
their cardinalities are equal.\<close>

lemma ElemClassEquiv: "\equiv A r; C \ A // r\ \ \x \ C. \y \ C. (x, y) \ r"
  unfolding equiv_def quotient_def sym_def trans_def by blast

context sylow_central
begin

lemma M_elem_map: "M2 \ M \ \g. g \ carrier G \ M1 #> g = M2"
  using M1_in_M M_in_quot [THEN RelM_equiv [THEN ElemClassEquiv]]
  by (simp add: RelM_def) (blast dest!: bspec)

lemmas M_elem_map_carrier = M_elem_map [THEN someI_ex, THEN conjunct1]

lemmas M_elem_map_eq = M_elem_map [THEN someI_ex, THEN conjunct2]

lemma M_funcset_rcosets_H:
  "(\x\M. H #> (SOME g. g \ carrier G \ M1 #> g = x)) \ M \ rcosets H"
  by (metis (lifting) H_is_subgroup M_elem_map_carrier rcosetsI restrictI subgroup.subset)

lemma inj_M_GmodH: "\f \ M \ rcosets H. inj_on f M"
proof
  let ?inv = "\x. SOME g. g \ carrier G \ M1 #> g = x"
  show "inj_on (\x\M. H #> ?inv x) M"
  proof (rule inj_onI, simp)
    fix x y
    assume eq: "H #> ?inv x = H #> ?inv y" and xy: "x \ M" "y \ M"
    have "x = M1 #> ?inv x"
      by (simp add: M_elem_map_eq \<open>x \<in> M\<close>)
    also have "... = M1 #> ?inv y"
    proof (rule coset_mult_inv1 [OF in_H_imp_eq [OF coset_join1]])
      show "H #> ?inv x \ inv (?inv y) = H"
        by (simp add: H_into_carrier_G M_elem_map_carrier xy coset_mult_inv2 eq subsetI)
    qed (simp_all add: H_is_subgroup M_elem_map_carrier xy)
    also have "... = y"
      using M_elem_map_eq \<open>y \<in> M\<close> by simp
    finally show "x=y" .
  qed
  show "(\x\M. H #> ?inv x) \ M \ rcosets H"
    by (rule M_funcset_rcosets_H)
qed

end

subsubsection \<open>The Opposite Injection\<close>

context sylow_central
begin

lemma H_elem_map: "H1 \ rcosets H \ \g. g \ carrier G \ H #> g = H1"
  by (auto simp: RCOSETS_def)

lemmas H_elem_map_carrier = H_elem_map [THEN someI_ex, THEN conjunct1]

lemmas H_elem_map_eq = H_elem_map [THEN someI_ex, THEN conjunct2]

lemma rcosets_H_funcset_M:
  "(\C \ rcosets H. M1 #> (SOME g. g \ carrier G \ H #> g = C)) \ rcosets H \ M"
  using in_quotient_imp_closed [OF RelM_equiv M_in_quot _  M1_RelM_rcosetGM1g]
  by (simp add: M1_in_M H_elem_map_carrier RCOSETS_def)

lemma inj_GmodH_M: "\g \ rcosets H\M. inj_on g (rcosets H)"
proof
  let ?inv = "\x. SOME g. g \ carrier G \ H #> g = x"
  show "inj_on (\C\rcosets H. M1 #> ?inv C) (rcosets H)"
  proof (rule inj_onI, simp)
    fix x y
    assume eq: "M1 #> ?inv x = M1 #> ?inv y" and xy: "x \ rcosets H" "y \ rcosets H"
    have "x = H #> ?inv x"
      by (simp add: H_elem_map_eq \<open>x \<in> rcosets H\<close>)
    also have "... = H #> ?inv y"
    proof (rule coset_mult_inv1 [OF coset_join2])
      show "?inv x \ inv (?inv y) \ carrier G"
        by (simp add: H_elem_map_carrier \<open>x \<in> rcosets H\<close> \<open>y \<in> rcosets H\<close>)
      then show "(?inv x) \ inv (?inv y) \ H"
        by (simp add: H_I H_elem_map_carrier xy coset_mult_inv2 eq)
      show "H \ carrier G"
        by (simp add: H_is_subgroup subgroup.subset)
    qed (simp_all add: H_is_subgroup H_elem_map_carrier xy)
    also have "... = y"
      by (simp add: H_elem_map_eq \<open>y \<in> rcosets H\<close>)
    finally show "x=y" .
  qed
  show "(\C\rcosets H. M1 #> ?inv C) \ rcosets H \ M"
    using rcosets_H_funcset_M by blast
qed

lemma calM_subset_PowG: "calM \ Pow (carrier G)"
  by (auto simp: calM_def)

lemma finite_M: "finite M"
  by (metis M_subset_calM finite_calM rev_finite_subset)

lemma cardMeqIndexH: "card M = card (rcosets H)"
  using inj_M_GmodH inj_GmodH_M
  by (blast intro: card_bij finite_M H_is_subgroup rcosets_subset_PowG [THEN finite_subset])

lemma index_lem: "card M * card H = order G"
  by (simp add: cardMeqIndexH lagrange H_is_subgroup)

lemma card_H_eq: "card H = p^a"
proof (rule antisym)
  show "p^a \ card H"
  proof (rule dvd_imp_le)
    show "p ^ a dvd card H"
      apply (rule div_combine [OF prime_imp_prime_elem[OF prime_p] not_dvd_M])
      by (simp add: index_lem multiplicity_dvd order_G power_add)
    show "0 < card H"
      by (blast intro: subgroup.finite_imp_card_positive H_is_subgroup)
  qed
next
  show "card H \ p^a"
    using M1_inj_H card_M1 card_inj finite_M1 by fastforce
qed

end

lemma (in sylow) sylow_thm: "\H. subgroup H G \ card H = p^a"
proof -
  obtain M where M: "M \ calM // RelM" "\ (p ^ Suc (multiplicity p m) dvd card M)"
    using lemma_A1 by blast
  then obtain M1 where "M1 \ M"
    by (metis existsM1inM)
  define H where "H \ {g. g \ carrier G \ M1 #> g = M1}"
  with M \<open>M1 \<in> M\<close>
  interpret sylow_central G p a m calM RelM H M1 M
    by unfold_locales (auto simp add: H_def calM_def RelM_def)
  show ?thesis
    using H_is_subgroup card_H_eq by blast
qed

text \<open>Needed because the locale's automatic definition refers to
  \<^term>\<open>semigroup G\<close> and \<^term>\<open>group_axioms G\<close> rather than
  simply to \<^term>\<open>group G\<close>.\<close>
lemma sylow_eq: "sylow G p a m \ group G \ sylow_axioms G p a m"
  by (simp add: sylow_def group_def)

subsection \<open>Sylow's Theorem\<close>

theorem sylow_thm:
  "\prime p; group G; order G = (p^a) * m; finite (carrier G)\
    \<Longrightarrow> \<exists>H. subgroup H G \<and> card H = p^a"
  by (rule sylow.sylow_thm [of G p a m]) (simp add: sylow_eq sylow_axioms_def)

end

¤ Dauer der Verarbeitung: 0.0 Sekunden (vorverarbeitet) ¤

Download des Quellennavigators
Download des sprechenden Kalenders
in der Quellcodebibliothek suchen

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.