Quellcode-Bibliothek sylow_theorems.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