|
%%-------------------** 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.2 Sekunden
(vorverarbeitet)
¤
|
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.
|
