Quellcode-Bibliothek

^© Kompilation durch diese Firma

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

Datei: complex_field.pvs Sprache: PVS

Original von: PVS^©

%%-------------------** Sylow Theorems **-------------------
%%
%% Author          : André Luiz Galdino
%%                   Universidade Federal de Goiás - Brasil
%%
%% Last Modified On: November 28, 2011
%%
%%----------------------------------------------------------

sylow_theorems[T: TYPE, *: [T,T -> T], one: T]: THEORY

BEGIN

   ASSUMING IMPORTING algebra@group_def

       T_is_group: ASSUMPTION group?[T,*,one](fullset[T])

   ENDASSUMING

   IMPORTING algebra@finite_groups[T,*,one],
             isomorphism_theorems,
             p_groups

             G: VAR group[T,*,one]
             X: VAR setofsets[T]
    p, n, m, i: VAR posnat

%%%%% Definitions %%%%%

   p_subgroup_sylow?(G:finite_group, p:{p: posnat | prime?(p)})(P:subgroup(G)): bool =
      p_group?[T,*,one](P,p) AND
     (FORALL (H: subgroup(G)): p_group?[T,*,one](H,p) AND subgroup?(P,H) IMPLIES P = H)

   p_subgroup_sylow(G:finite_group, p:{p: posnat | prime?(p)}): setofsets[T] =
                                                                {P: subgroup(G) | p_subgroup_sylow?(G,p)(P)}

   is_conjugate(G:finite_group,H:subgroup(G))(S:subgroup(G)): bool = EXISTS (a: (G)): S = a*H*inv(a)

   action_by_c(G:finite_group, X)(a:(G), P:(X)): set[T] = a*P*inv(a)

%%%%% Quotient subgroups %%%%%

   subgroup_is_factor: LEMMA FORALL (N: normal_subgroup(G), S: subgroup(G/N)):
                                      EXISTS (H: subgroup(G)): subgroup?(N,H) AND S = H/N

%%%%% First Sylow Theorem %%%%%

   First_Sylow_Theorem: THEOREM
            FORALL (G:finite_group): prime?(p) AND order(G) = p^(n)*m AND gcd(p,m) = 1 AND i <= n
               IMPLIES
                     (EXISTS (H: subgroup(G)): order(H) = p^i)
                                      AND
                     (FORALL (S: subgroup(G)): order(S) = p^(i - 1)
                        IMPLIES
                           EXISTS (K: subgroup(G)): order(K) = p^i AND normal_subgroup?(S,K))

   p_group_is_subgroup: COROLLARY
               FORALL (G:finite_group, H: subgroup(G)):
                 prime?(p) AND gcd(p,m) = 1 AND i <= n AND order(G) = p^(n)*m  AND order(H) = p^(n - i)
                  IMPLIES
                     EXISTS (K: subgroup(G)): order(K) = p^(n) AND subgroup?(H,K)

   p_subgroup_sylow_order: COROLLARY FORALL (G:finite_group, P:subgroup(G)):
                                        prime?(p) AND order(G) = p^(n)*m AND gcd(p,m) = 1
                                            IMPLIES
                                                (p_subgroup_sylow?(G,p)(P) IFF order(P) = p^(n))

   conjugate_is_p_subgroup_sylow: COROLLARY  FORALL (G:finite_group, P:subgroup(G)):
                                        prime?(p) AND order(G) = p^(n)*m AND gcd(p,m) = 1 AND
                                        p_subgroup_sylow?(G,p)(P)
                                            IMPLIES
                                                FORALL (a:(G)): p_subgroup_sylow?(G,p)(a*P*inv(a))

   unique_is_normal: COROLLARY  FORALL (G:finite_group, P:subgroup(G)):
                                        prime?(p) AND order(G) = p^(n)*m AND gcd(p,m) = 1 AND
                                        p_subgroup_sylow(G,p) = singleton(P)
                                            IMPLIES
                                                normal_subgroup?(P,G)

%%%%% Second Sylow Theorem %%%%%

   Second_Sylow_Theorem: THEOREM
            FORALL (G:finite_group, P, K:subgroup(G)):
               prime?(p) AND order(G) = p^(n)*m AND gcd(p,m) = 1 AND
               p_subgroup_sylow?(G,p)(P) AND p_group?[T,*,one](K,p)
                  IMPLIES
                     EXISTS (a:(G)): subgroup?(K,a*P*inv(a))
                                      AND
                     (p_subgroup_sylow?(G,p)(K) IMPLIES is_conjugate(G,P)(K))

%%%%% Third Sylow Theorem %%%%%

   Third_Sylow_Theorem: THEOREM
            FORALL (G:finite_group, P:subgroup(G)):
               prime?(p) AND order(G) = p^(n)*m AND gcd(p,m) = 1 AND
               p_subgroup_sylow?(G,p)(P)
                   IMPLIES
                     LET np = card(p_subgroup_sylow(G,p)) IN
                     np = index(G, normalizer(G,P)) AND divides(np,m) AND divides(p, np -1)

END sylow_theorems

¤ Dauer der Verarbeitung: 0.0 Sekunden (vorverarbeitet) ¤

Druckansicht unsichere Verbindung
Druckansicht 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.