|
%%-------------------** p-Groups and Burside Theorem **-------------------
%%
%% Author : André Luiz Galdino
%% Universidade Federal de Goiás - Brasil
%%
%% Last Modified On: November 28, 2011
%%
%%------------------------------------------------------------------------
p_groups[T:Type, *:[T,T->T], one:T]: THEORY
BEGIN
ASSUMING IMPORTING algebra@group_def[T,*,one]
fullset_is_group: ASSUMPTION group?(fullset[T])
ENDASSUMING
IMPORTING algebra@finite_cyclic_groups,
algebra@finite_groups[T,*,one],
normalizer_centralizer[T,*,one],
cauchy[T, *, one]
G, H, K: VAR group[T,*,one]
p: VAR posnat
n: VAR nat
%%%%% Definitions %%%%%
p_group?(G:finite_group, p: {p:posnat | prime?(p)} ): bool = FORALL (a:(G)):
(EXISTS (n: nat): period(G,a) = p^n)
alt(G:group,H: subgroup(G),K: subgroup(G))(h:(H), A: (left_cosets(G,K))): set[T] = h*A
; %%%%% Properties and results %%%%%
alt_is_action: LEMMA FORALL (H, K: subgroup(G)):
group_action?(H, left_cosets(G,K))(alt(G,H,K))
Fix_iff_subset: LEMMA FORALL (H, K: subgroup(G), g: (G)):
member(g*K, Fix(H,left_cosets(G,K))(alt(G,H,K))) IFF subset?(H, g*K*inv(g))
Fix_iff_subset_cor: LEMMA FORALL (G:finite_group, H, K: subgroup(G), g: (G)):
member(g*H, Fix(H,left_cosets(G,H))(alt(G,H,H))) IFF H = g*H*inv(g)
subgroup_is_p_group: LEMMA FORALL (G:finite_group,H: subgroup(G)):
prime?(p) AND p_group?(G,p) IMPLIES p_group?(H,p)
p_group_iff_power: LEMMA FORALL (G:finite_group):
prime?(p) IMPLIES (p_group?(G,p) IFF (EXISTS (m:nat): order(G) = p^m))
p_divides_index: LEMMA FORALL (G:finite_group, H:subgroup(G)):
prime?(p) AND p_group?(G,p) AND H /= G IMPLIES divides(p, index(G,H))
factor_cyclic: LEMMA cyclic?(G/center(G)) IMPLIES abelian_group?(G)
normalizer_index: LEMMA FORALL (G:finite_group, H:subgroup(G)):
prime?(p) AND p_group?(H,p) AND divides(p, index(G,H))
IMPLIES divides(p, index(normalizer(G,H), H))
subgroup_proper: LEMMA FORALL (G:finite_group, H:subgroup(G)):
prime?(p) AND p_group?(G,p) AND H /= G
IMPLIES H /= normalizer(G,H)
%%%%% Burside Theorem %%%%%
burside_theorem: THEOREM FORALL (G:finite_group):
order(G) > 1 AND prime?(p) AND p_group?(G,p)
IMPLIES order(center(G)) >= p
p_square_is_abelian: LEMMA FORALL (G:finite_group): prime?(p) AND order(G) = p^2
IMPLIES abelian_group?(G)
END p_groups
¤ Dauer der Verarbeitung: 0.18 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.
|
