|
%%-------------------** Cauchy Theorem **-------------------
%%
%% Author : André Luiz Galdino
%% Universidade Federal de Goiás - Brasil
%%
%% Last Modified On: November 28, 2011
%%
%%----------------------------------------------------------
cauchy[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 ints@primes,
algebra@finite_groups,
algebra@finite_cyclic_groups[T,*,one],
group_action,
zp_group,
cauchy_scaf[T]
G: VAR finite_group
p: VAR posnat
fs, fs1, fs2: VAR finseq
n: VAR nat
a: VAR T
fseq_product(fs): RECURSIVE T = IF length(fs) = 0 THEN one
ELSE fs`seq(0)*fseq_product(rest(fs))
ENDIF
MEASURE length(fs)
S(G)(n): set[finseq] = {fs: finseq | length(fs) = n AND
(FORALL (i: below[n]): member(fs`seq(i), G)) AND
fseq_product(fs) = one}
same_element(a, fs):bool = FORALL (i: below[length(fs)]): fs`seq(i) = a
SE(G)(n): set[finseq] = {fs: (S(G)(n)) | EXISTS (a: (G)): same_element(a, fs)}
%%%%% Properties %%%
fseq_product_in: LEMMA (FORALL (i: below[length(fs)]): member(fs`seq(i), G))
IMPLIES member(fseq_product(fs), G)
fseq_product_o: LEMMA (FORALL (i: below[length(fs1)]): member(fs1`seq(i), G)) AND
(FORALL (j: below[length(fs2)]): member(fs2`seq(j), G))
IMPLIES
fseq_product(fs1 o fs2) = fseq_product(fs1) * fseq_product(fs2)
fseq_product_one: LEMMA (FORALL (i: below[length(fs)]): member(fs`seq(i), G))
IMPLIES inv(fseq_product(fs)) * fseq_product(fs) = one
fseq_product_power: LEMMA FORALL (g: (G)): same_element(g, fs) IMPLIES fseq_product(fs) = g^length(fs)
one_in_SE: LEMMA length(fs) = n AND same_element(one, fs) IMPLIES member(fs, SE(G)(n))
order_SE: LEMMA FORALL (g: (G)): prime?(p) AND g /= one AND
same_element(g, fs) AND member(fs, SE(G)(p))
IMPLIES period(G,g) = p
S_bij_set_seq: LEMMA LET A = set_seq(G)(p - 1),
B = S(G)(p) IN
EXISTS (g:[(A)->(B)]): bijective?(g)
S_is_finite:LEMMA is_finite(S(G)(n))
S_card: LEMMA card(S(G)(p)) = card(G)^(p - 1)
%%%%% Group action %%%
F(p, G)(k: (Zn[p]), fs: (S(G)(p))): finseq = (# length := p,
seq := (LAMBDA (i: below[p]):fs`seq(rem(p)(i + k))) #)
F_1(fs)(k: below[length(fs)]): finseq = (# length := length(fs) - k,
seq := (LAMBDA (i: below[length(fs) - k]):
fs`seq(rem(length(fs))(i + k))) #)
F_2(fs)(k: below[length(fs)]): finseq = (# length := k,
seq := (LAMBDA (i: below[k]): fs`seq(i)) #)
F_o_F12: LEMMA FORALL (k: (Zn[p]), fs: (S(G)(p))): F(p,G)(k, fs) = F_1(fs)(k) o F_2(fs)(k)
fs_o_F21: LEMMA FORALL (k: (Zn[p]), fs: (S(G)(p))): fs = F_2(fs)(k) o F_1(fs)(k)
F_in_S: LEMMA FORALL (k: (Zn[p]), fs: (S(G)(p))): member(F(p,G)(k, fs), S(G)(p))
F_is_action: LEMMA group_action?[below(p),++,0,finseq](Zn[p],S(G)(p))(F(p,G))
%%%%% Fixed point subset %%%
Fixed_subset: LEMMA LET H = Zn[p],
X = S(G)(p),
f = F(p, G) IN
Fix[below(p),++,0,finseq](H,X)(f) = SE(G)(p)
%%%%% Cauchy Theorem %%%
cauchy: THEOREM prime?(p) AND divides(p, order(G)) IMPLIES EXISTS (x: (G)): period(G,x) = p
cauchy_cor: COROLLARY prime?(p) AND divides(p, order(G)) IMPLIES EXISTS (H: subgroup(G)): order(H) = p
END cauchy
[ Dauer der Verarbeitung: 0.7 Sekunden
(vorverarbeitet)
]
|
