begin
:: deftheorem Def1 defines being_left_operation GROUP_10:def 1 :
theorem Th1:
:: deftheorem Def2 defines the_left_operation_of GROUP_10:def 2 :
:: deftheorem defines the_subsets_of_card GROUP_10:def 3 :
theorem Th2:
theorem Th3:
definition
let E be non
empty set ;
let n be
natural number ;
let S be non
empty Group-like multMagma ;
let s be
Element of
S;
let LO be
LeftOperation of
S,
E;
assume A1:
card n c= card E
;
func the_extension_of_left_translation_of n,
s,
LO -> Function of
(the_subsets_of_card n,E),
(the_subsets_of_card n,E) means :
Def4:
for
X being
Element of
the_subsets_of_card n,
E holds
it . X = (LO ^ s) .: X;
existence
ex b1 being Function of (the_subsets_of_card n,E),(the_subsets_of_card n,E) st
for X being Element of the_subsets_of_card n,E holds b1 . X = (LO ^ s) .: X
uniqueness
for b1, b2 being Function of (the_subsets_of_card n,E),(the_subsets_of_card n,E) st ( for X being Element of the_subsets_of_card n,E holds b1 . X = (LO ^ s) .: X ) & ( for X being Element of the_subsets_of_card n,E holds b2 . X = (LO ^ s) .: X ) holds
b1 = b2
end;
:: deftheorem Def4 defines the_extension_of_left_translation_of GROUP_10:def 4 :
definition
let E be non
empty set ;
let n be
natural number ;
let S be non
empty Group-like multMagma ;
let LO be
LeftOperation of
S,
E;
assume A1:
card n c= card E
;
func the_extension_of_left_operation_of n,
LO -> LeftOperation of
S,
(the_subsets_of_card n,E) means :
Def5:
for
s being
Element of
S holds
it . s = the_extension_of_left_translation_of n,
s,
LO;
existence
ex b1 being LeftOperation of S,(the_subsets_of_card n,E) st
for s being Element of S holds b1 . s = the_extension_of_left_translation_of n,s,LO
uniqueness
for b1, b2 being LeftOperation of S,(the_subsets_of_card n,E) st ( for s being Element of S holds b1 . s = the_extension_of_left_translation_of n,s,LO ) & ( for s being Element of S holds b2 . s = the_extension_of_left_translation_of n,s,LO ) holds
b1 = b2
end;
:: deftheorem Def5 defines the_extension_of_left_operation_of GROUP_10:def 5 :
definition
let S be non
empty multMagma ;
let s be
Element of
S;
let Z be non
empty set ;
func the_left_translation_of s,
Z -> Function of
[:the carrier of S,Z:],
[:the carrier of S,Z:] means :
Def6:
for
z1 being
Element of
[:the carrier of S,Z:] ex
z2 being
Element of
[:the carrier of S,Z:] ex
s1,
s2 being
Element of
S ex
z being
Element of
Z st
(
z2 = it . z1 &
s2 = s * s1 &
z1 = [s1,z] &
z2 = [s2,z] );
existence
ex b1 being Function of [:the carrier of S,Z:],[:the carrier of S,Z:] st
for z1 being Element of [:the carrier of S,Z:] ex z2 being Element of [:the carrier of S,Z:] ex s1, s2 being Element of S ex z being Element of Z st
( z2 = b1 . z1 & s2 = s * s1 & z1 = [s1,z] & z2 = [s2,z] )
uniqueness
for b1, b2 being Function of [:the carrier of S,Z:],[:the carrier of S,Z:] st ( for z1 being Element of [:the carrier of S,Z:] ex z2 being Element of [:the carrier of S,Z:] ex s1, s2 being Element of S ex z being Element of Z st
( z2 = b1 . z1 & s2 = s * s1 & z1 = [s1,z] & z2 = [s2,z] ) ) & ( for z1 being Element of [:the carrier of S,Z:] ex z2 being Element of [:the carrier of S,Z:] ex s1, s2 being Element of S ex z being Element of Z st
( z2 = b2 . z1 & s2 = s * s1 & z1 = [s1,z] & z2 = [s2,z] ) ) holds
b1 = b2
end;
:: deftheorem Def6 defines the_left_translation_of GROUP_10:def 6 :
definition
let S be non
empty Group-like associative multMagma ;
let Z be non
empty set ;
func the_left_operation_of S,
Z -> LeftOperation of
S,
[:the carrier of S,Z:] means :
Def7:
for
s being
Element of
S holds
it . s = the_left_translation_of s,
Z;
existence
ex b1 being LeftOperation of S,[:the carrier of S,Z:] st
for s being Element of S holds b1 . s = the_left_translation_of s,Z
uniqueness
for b1, b2 being LeftOperation of S,[:the carrier of S,Z:] st ( for s being Element of S holds b1 . s = the_left_translation_of s,Z ) & ( for s being Element of S holds b2 . s = the_left_translation_of s,Z ) holds
b1 = b2
end;
:: deftheorem Def7 defines the_left_operation_of GROUP_10:def 7 :
definition
let G be
Group;
let H,
P be
Subgroup of
G;
let h be
Element of
H;
func the_left_translation_of h,
P -> Function of
(Left_Cosets P),
(Left_Cosets P) means :
Def8:
for
P1 being
Element of
Left_Cosets P ex
P2 being
Element of
Left_Cosets P ex
A1,
A2 being
Subset of
G ex
g being
Element of
G st
(
P2 = it . P1 &
A2 = g * A1 &
A1 = P1 &
A2 = P2 &
g = h );
existence
ex b1 being Function of (Left_Cosets P),(Left_Cosets P) st
for P1 being Element of Left_Cosets P ex P2 being Element of Left_Cosets P ex A1, A2 being Subset of G ex g being Element of G st
( P2 = b1 . P1 & A2 = g * A1 & A1 = P1 & A2 = P2 & g = h )
uniqueness
for b1, b2 being Function of (Left_Cosets P),(Left_Cosets P) st ( for P1 being Element of Left_Cosets P ex P2 being Element of Left_Cosets P ex A1, A2 being Subset of G ex g being Element of G st
( P2 = b1 . P1 & A2 = g * A1 & A1 = P1 & A2 = P2 & g = h ) ) & ( for P1 being Element of Left_Cosets P ex P2 being Element of Left_Cosets P ex A1, A2 being Subset of G ex g being Element of G st
( P2 = b2 . P1 & A2 = g * A1 & A1 = P1 & A2 = P2 & g = h ) ) holds
b1 = b2
end;
:: deftheorem Def8 defines the_left_translation_of GROUP_10:def 8 :
definition
let G be
Group;
let H,
P be
Subgroup of
G;
func the_left_operation_of H,
P -> LeftOperation of
H,
(Left_Cosets P) means :
Def9:
for
h being
Element of
H holds
it . h = the_left_translation_of h,
P;
existence
ex b1 being LeftOperation of H,(Left_Cosets P) st
for h being Element of H holds b1 . h = the_left_translation_of h,P
uniqueness
for b1, b2 being LeftOperation of H,(Left_Cosets P) st ( for h being Element of H holds b1 . h = the_left_translation_of h,P ) & ( for h being Element of H holds b2 . h = the_left_translation_of h,P ) holds
b1 = b2
end;
:: deftheorem Def9 defines the_left_operation_of GROUP_10:def 9 :
begin
:: deftheorem Def10 defines the_strict_stabilizer_of GROUP_10:def 10 :
:: deftheorem defines the_strict_stabilizer_of GROUP_10:def 11 :
:: deftheorem Def12 defines is_fixed_under GROUP_10:def 12 :
:: deftheorem Def13 defines the_fixed_points_of GROUP_10:def 13 :
:: deftheorem Def14 defines are_conjugated_under GROUP_10:def 14 :
theorem Th4:
theorem Th5:
theorem Th6:
:: deftheorem defines the_orbit_of GROUP_10:def 15 :
theorem Th7:
theorem Th8:
theorem Th9:
theorem Th10:
:: deftheorem defines the_orbits_of GROUP_10:def 16 :
begin
:: deftheorem Def17 defines is_p-group_of_prime GROUP_10:def 17 :
:: deftheorem Def18 defines is_p-group_of_prime GROUP_10:def 18 :
theorem Th11:
begin
:: deftheorem Def19 defines is_Sylow_p-subgroup_of_prime GROUP_10:def 19 :
Lm1:
for n being natural number
for p being natural prime number st n <> 0 holds
ex m, r being natural number st
( n = (p |^ r) * m & not p divides m )
Lm2:
for n being natural number st n > 0 holds
card (INT.Group n) = n
Lm3:
for X, Y being non empty set holds card { [:X,{y}:] where y is Element of Y : verum } = card Y
Lm4:
for G being finite Group
for E, T being non empty set
for LO being LeftOperation of G,E
for n being natural number st LO = the_left_operation_of G,T & n = card G & E = [:the carrier of G,T:] & card n c= card E holds
the_fixed_points_of (the_extension_of_left_operation_of n,LO) = { [:the carrier of G,{t}:] where t is Element of T : verum }
Lm5:
for n, m, r being natural number
for p being natural prime number st n = (p |^ r) * m & not p divides m holds
(n choose (p |^ r)) mod p <> 0
Lm6:
for r, n, m1, m2 being natural number
for p being natural prime number st (p |^ r) * n = m1 * m2 & not p divides n & not p divides m2 holds
p |^ r divides m1
Lm7:
for G being Group
for A being non empty Subset of G
for x being Element of G holds card A = card (A * x)
theorem Th12:
Lm8:
for n, r being natural number
for p being natural prime number st n divides p |^ r & n > 1 holds
p divides n
theorem
theorem Th14:
:: deftheorem defines the_sylow_p-subgroups_of_prime GROUP_10:def 20 :
definition
let G be
finite Group;
let p be
natural prime number ;
let H be
Subgroup of
G;
let h be
Element of
H;
func the_left_translation_of h,
p -> Function of
(the_sylow_p-subgroups_of_prime p,G),
(the_sylow_p-subgroups_of_prime p,G) means :
Def21:
for
P1 being
Element of
the_sylow_p-subgroups_of_prime p,
G ex
P2 being
Element of
the_sylow_p-subgroups_of_prime p,
G ex
H1,
H2 being
strict Subgroup of
G ex
g being
Element of
G st
(
P2 = it . P1 &
P1 = H1 &
P2 = H2 &
h " = g &
H2 = H1 |^ g );
existence
ex b1 being Function of (the_sylow_p-subgroups_of_prime p,G),(the_sylow_p-subgroups_of_prime p,G) st
for P1 being Element of the_sylow_p-subgroups_of_prime p,G ex P2 being Element of the_sylow_p-subgroups_of_prime p,G ex H1, H2 being strict Subgroup of G ex g being Element of G st
( P2 = b1 . P1 & P1 = H1 & P2 = H2 & h " = g & H2 = H1 |^ g )
uniqueness
for b1, b2 being Function of (the_sylow_p-subgroups_of_prime p,G),(the_sylow_p-subgroups_of_prime p,G) st ( for P1 being Element of the_sylow_p-subgroups_of_prime p,G ex P2 being Element of the_sylow_p-subgroups_of_prime p,G ex H1, H2 being strict Subgroup of G ex g being Element of G st
( P2 = b1 . P1 & P1 = H1 & P2 = H2 & h " = g & H2 = H1 |^ g ) ) & ( for P1 being Element of the_sylow_p-subgroups_of_prime p,G ex P2 being Element of the_sylow_p-subgroups_of_prime p,G ex H1, H2 being strict Subgroup of G ex g being Element of G st
( P2 = b2 . P1 & P1 = H1 & P2 = H2 & h " = g & H2 = H1 |^ g ) ) holds
b1 = b2
end;
:: deftheorem Def21 defines the_left_translation_of GROUP_10:def 21 :
definition
let G be
finite Group;
let p be
natural prime number ;
let H be
Subgroup of
G;
func the_left_operation_of H,
p -> LeftOperation of
H,
(the_sylow_p-subgroups_of_prime p,G) means :
Def22:
for
h being
Element of
H holds
it . h = the_left_translation_of h,
p;
existence
ex b1 being LeftOperation of H,(the_sylow_p-subgroups_of_prime p,G) st
for h being Element of H holds b1 . h = the_left_translation_of h,p
uniqueness
for b1, b2 being LeftOperation of H,(the_sylow_p-subgroups_of_prime p,G) st ( for h being Element of H holds b1 . h = the_left_translation_of h,p ) & ( for h being Element of H holds b2 . h = the_left_translation_of h,p ) holds
b1 = b2
end;
:: deftheorem Def22 defines the_left_operation_of GROUP_10:def 22 :
Lm9:
for G, H being finite Group
for p being natural prime number
for I being Subgroup of G
for P being Subgroup of H st I = P & I is_Sylow_p-subgroup_of_prime p & H is Subgroup of G holds
P is_Sylow_p-subgroup_of_prime p
theorem
begin
theorem
theorem
theorem
theorem