:: by Marco Riccardi

::

:: Received August 13, 2007

:: Copyright (c) 2007-2012 Association of Mizar Users

begin

notation

let S be non empty 1-sorted ;

let E be set ;

let A be Action of the carrier of S,E;

let s be Element of S;

synonym A ^ s for S . E;

end;
let E be set ;

let A be Action of the carrier of S,E;

let s be Element of S;

synonym A ^ s for S . E;

definition

let S be non empty 1-sorted ;

let E be set ;

let A be Action of the carrier of S,E;

let s be Element of S;

:: original: ^

redefine func A ^ s -> Function of E,E;

correctness

coherence

^ is Function of E,E;

end;
let E be set ;

let A be Action of the carrier of S,E;

let s be Element of S;

:: original: ^

redefine func A ^ s -> Function of E,E;

correctness

coherence

^ is Function of E,E;

proof end;

definition
end;

:: deftheorem Def1 defines being_left_operation GROUP_10:def 1 :

for S being non empty unital multMagma

for E being set

for A being Action of the carrier of S,E holds

( A is being_left_operation iff ( A ^ (1_ S) = id E & ( for s1, s2 being Element of S holds A ^ (s1 * s2) = (A ^ s1) * (A ^ s2) ) ) );

for S being non empty unital multMagma

for E being set

for A being Action of the carrier of S,E holds

( A is being_left_operation iff ( A ^ (1_ S) = id E & ( for s1, s2 being Element of S holds A ^ (s1 * s2) = (A ^ s1) * (A ^ s2) ) ) );

registration

let S be non empty unital multMagma ;

let E be set ;

existence

ex b_{1} being Action of the carrier of S,E st b_{1} is being_left_operation ;

end;
let E be set ;

cluster Relation-like the carrier of S -defined Funcs (E,E) -valued non empty Function-like total quasi_total being_left_operation for Element of bool [: the carrier of S,(Funcs (E,E)):];

correctness existence

ex b

proof end;

:: ALG I.5.1 DEF 1

definition

let S be non empty unital multMagma ;

let E be set ;

mode LeftOperation of S,E is being_left_operation Action of the carrier of S,E;

end;
let E be set ;

mode LeftOperation of S,E is being_left_operation Action of the carrier of S,E;

scheme :: GROUP_10:sch 1

ExLeftOperation{ F_{1}() -> set , F_{2}() -> non empty Group-like multMagma , F_{3}( Element of F_{2}()) -> Function of F_{1}(),F_{1}() } :

ExLeftOperation{ F

ex T being LeftOperation of F_{2}(),F_{1}() st

for s being Element of F_{2}() holds T . s = F_{3}(s)

providedfor s being Element of F

A1:
F_{3}((1_ F_{2}())) = id F_{1}()
and

A2: for s1, s2 being Element of F_{2}() holds F_{3}((s1 * s2)) = F_{3}(s1) * F_{3}(s2)

A2: for s1, s2 being Element of F

proof end;

registration

let E be non empty set ;

let S be non empty Group-like multMagma ;

let s be Element of S;

let LO be LeftOperation of S,E;

coherence

for b_{1} being Function of E,E st b_{1} = LO ^ s holds

b_{1} is one-to-one

end;
let S be non empty Group-like multMagma ;

let s be Element of S;

let LO be LeftOperation of S,E;

coherence

for b

b

proof end;

notation
end;

definition

let S be non empty Group-like associative multMagma ;

ex b_{1} being LeftOperation of S, the carrier of S st

for s being Element of S holds b_{1} . s = the_left_translation_of s

for b_{1}, b_{2} being LeftOperation of S, the carrier of S st ( for s being Element of S holds b_{1} . s = the_left_translation_of s ) & ( for s being Element of S holds b_{2} . s = the_left_translation_of s ) holds

b_{1} = b_{2}

end;
func the_left_operation_of S -> LeftOperation of S, the carrier of S means :Def2: :: GROUP_10:def 2

for s being Element of S holds it . s = the_left_translation_of s;

existence for s being Element of S holds it . s = the_left_translation_of s;

ex b

for s being Element of S holds b

proof end;

uniqueness for b

b

proof end;

:: deftheorem Def2 defines the_left_operation_of GROUP_10:def 2 :

for S being non empty Group-like associative multMagma

for b_{2} being LeftOperation of S, the carrier of S holds

( b_{2} = the_left_operation_of S iff for s being Element of S holds b_{2} . s = the_left_translation_of s );

for S being non empty Group-like associative multMagma

for b

( b

definition

let E, n be set ;

coherence

{ X where X is Subset of E : card X = n } is Subset-Family of E;

end;
func the_subsets_of_card (n,E) -> Subset-Family of E equals :: GROUP_10:def 3

{ X where X is Subset of E : card X = n } ;

correctness { X where X is Subset of E : card X = n } ;

coherence

{ X where X is Subset of E : card X = n } is Subset-Family of E;

proof end;

:: deftheorem defines the_subsets_of_card GROUP_10:def 3 :

for E, n being set holds the_subsets_of_card (n,E) = { X where X is Subset of E : card X = n } ;

for E, n being set holds the_subsets_of_card (n,E) = { X where X is Subset of E : card X = n } ;

registration
end;

theorem Th1: :: GROUP_10:1

for n being Nat

for E being non empty set st card n c= card E holds

not the_subsets_of_card (n,E) is empty

for E being non empty set st card n c= card E holds

not the_subsets_of_card (n,E) is empty

proof end;

theorem Th2: :: GROUP_10:2

for E being non empty finite set

for k being Element of NAT

for x1, x2 being set st x1 <> x2 holds

card (Choose (E,k,x1,x2)) = card (the_subsets_of_card (k,E))

for k being Element of NAT

for x1, x2 being set st x1 <> x2 holds

card (Choose (E,k,x1,x2)) = card (the_subsets_of_card (k,E))

proof end;

definition

let E be non empty set ;

let n be Nat;

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 ;

ex b_{1} 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 b_{1} . X = (LO ^ s) .: X

for b_{1}, b_{2} 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 b_{1} . X = (LO ^ s) .: X ) & ( for X being Element of the_subsets_of_card (n,E) holds b_{2} . X = (LO ^ s) .: X ) holds

b_{1} = b_{2}

end;
let n be Nat;

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: :: GROUP_10:def 4

for X being Element of the_subsets_of_card (n,E) holds it . X = (LO ^ s) .: X;

existence for X being Element of the_subsets_of_card (n,E) holds it . X = (LO ^ s) .: X;

ex b

for X being Element of the_subsets_of_card (n,E) holds b

proof end;

uniqueness for b

b

proof end;

:: deftheorem Def4 defines the_extension_of_left_translation_of GROUP_10:def 4 :

for E being non empty set

for n being Nat

for S being non empty Group-like multMagma

for s being Element of S

for LO being LeftOperation of S,E st card n c= card E holds

for b_{6} being Function of (the_subsets_of_card (n,E)),(the_subsets_of_card (n,E)) holds

( b_{6} = the_extension_of_left_translation_of (n,s,LO) iff for X being Element of the_subsets_of_card (n,E) holds b_{6} . X = (LO ^ s) .: X );

for E being non empty set

for n being Nat

for S being non empty Group-like multMagma

for s being Element of S

for LO being LeftOperation of S,E st card n c= card E holds

for b

( b

definition

let E be non empty set ;

let n be Nat;

let S be non empty Group-like multMagma ;

let LO be LeftOperation of S,E;

assume A1: card n c= card E ;

ex b_{1} being LeftOperation of S,(the_subsets_of_card (n,E)) st

for s being Element of S holds b_{1} . s = the_extension_of_left_translation_of (n,s,LO)

for b_{1}, b_{2} being LeftOperation of S,(the_subsets_of_card (n,E)) st ( for s being Element of S holds b_{1} . s = the_extension_of_left_translation_of (n,s,LO) ) & ( for s being Element of S holds b_{2} . s = the_extension_of_left_translation_of (n,s,LO) ) holds

b_{1} = b_{2}

end;
let n be Nat;

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: :: GROUP_10:def 5

for s being Element of S holds it . s = the_extension_of_left_translation_of (n,s,LO);

existence for s being Element of S holds it . s = the_extension_of_left_translation_of (n,s,LO);

ex b

for s being Element of S holds b

proof end;

uniqueness for b

b

proof end;

:: deftheorem Def5 defines the_extension_of_left_operation_of GROUP_10:def 5 :

for E being non empty set

for n being Nat

for S being non empty Group-like multMagma

for LO being LeftOperation of S,E st card n c= card E holds

for b_{5} being LeftOperation of S,(the_subsets_of_card (n,E)) holds

( b_{5} = the_extension_of_left_operation_of (n,LO) iff for s being Element of S holds b_{5} . s = the_extension_of_left_translation_of (n,s,LO) );

for E being non empty set

for n being Nat

for S being non empty Group-like multMagma

for LO being LeftOperation of S,E st card n c= card E holds

for b

( b

definition

let S be non empty multMagma ;

let s be Element of S;

let Z be non empty set ;

ex b_{1} 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 = b_{1} . z1 & s2 = s * s1 & z1 = [s1,z] & z2 = [s2,z] )

for b_{1}, b_{2} 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 = b_{1} . 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 = b_{2} . z1 & s2 = s * s1 & z1 = [s1,z] & z2 = [s2,z] ) ) holds

b_{1} = b_{2}

end;
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: :: GROUP_10:def 6

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 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] );

ex b

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 = b

proof end;

uniqueness for b

( z2 = b

( z2 = b

b

proof end;

:: deftheorem Def6 defines the_left_translation_of GROUP_10:def 6 :

for S being non empty multMagma

for s being Element of S

for Z being non empty set

for b_{4} being Function of [: the carrier of S,Z:],[: the carrier of S,Z:] holds

( b_{4} = the_left_translation_of (s,Z) iff 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 = b_{4} . z1 & s2 = s * s1 & z1 = [s1,z] & z2 = [s2,z] ) );

for S being non empty multMagma

for s being Element of S

for Z being non empty set

for b

( b

( z2 = b

definition

let S be non empty Group-like associative multMagma ;

let Z be non empty set ;

ex b_{1} being LeftOperation of S,[: the carrier of S,Z:] st

for s being Element of S holds b_{1} . s = the_left_translation_of (s,Z)

for b_{1}, b_{2} being LeftOperation of S,[: the carrier of S,Z:] st ( for s being Element of S holds b_{1} . s = the_left_translation_of (s,Z) ) & ( for s being Element of S holds b_{2} . s = the_left_translation_of (s,Z) ) holds

b_{1} = b_{2}

end;
let Z be non empty set ;

func the_left_operation_of (S,Z) -> LeftOperation of S,[: the carrier of S,Z:] means :Def7: :: GROUP_10:def 7

for s being Element of S holds it . s = the_left_translation_of (s,Z);

existence for s being Element of S holds it . s = the_left_translation_of (s,Z);

ex b

for s being Element of S holds b

proof end;

uniqueness for b

b

proof end;

:: deftheorem Def7 defines the_left_operation_of GROUP_10:def 7 :

for S being non empty Group-like associative multMagma

for Z being non empty set

for b_{3} being LeftOperation of S,[: the carrier of S,Z:] holds

( b_{3} = the_left_operation_of (S,Z) iff for s being Element of S holds b_{3} . s = the_left_translation_of (s,Z) );

for S being non empty Group-like associative multMagma

for Z being non empty set

for b

( b

definition

let G be Group;

let H, P be Subgroup of G;

let h be Element of H;

ex b_{1} 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 = b_{1} . P1 & A2 = g * A1 & A1 = P1 & A2 = P2 & g = h )

for b_{1}, b_{2} 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 = b_{1} . 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 = b_{2} . P1 & A2 = g * A1 & A1 = P1 & A2 = P2 & g = h ) ) holds

b_{1} = b_{2}

end;
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: :: GROUP_10:def 8

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 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 );

ex b

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 = b

proof end;

uniqueness for b

( P2 = b

( P2 = b

b

proof end;

:: deftheorem Def8 defines the_left_translation_of GROUP_10:def 8 :

for G being Group

for H, P being Subgroup of G

for h being Element of H

for b_{5} being Function of (Left_Cosets P),(Left_Cosets P) holds

( b_{5} = the_left_translation_of (h,P) iff 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 = b_{5} . P1 & A2 = g * A1 & A1 = P1 & A2 = P2 & g = h ) );

for G being Group

for H, P being Subgroup of G

for h being Element of H

for b

( b

( P2 = b

definition

let G be Group;

let H, P be Subgroup of G;

ex b_{1} being LeftOperation of H,(Left_Cosets P) st

for h being Element of H holds b_{1} . h = the_left_translation_of (h,P)

for b_{1}, b_{2} being LeftOperation of H,(Left_Cosets P) st ( for h being Element of H holds b_{1} . h = the_left_translation_of (h,P) ) & ( for h being Element of H holds b_{2} . h = the_left_translation_of (h,P) ) holds

b_{1} = b_{2}

end;
let H, P be Subgroup of G;

func the_left_operation_of (H,P) -> LeftOperation of H,(Left_Cosets P) means :Def9: :: GROUP_10:def 9

for h being Element of H holds it . h = the_left_translation_of (h,P);

existence for h being Element of H holds it . h = the_left_translation_of (h,P);

ex b

for h being Element of H holds b

proof end;

uniqueness for b

b

proof end;

:: deftheorem Def9 defines the_left_operation_of GROUP_10:def 9 :

for G being Group

for H, P being Subgroup of G

for b_{4} being LeftOperation of H,(Left_Cosets P) holds

( b_{4} = the_left_operation_of (H,P) iff for h being Element of H holds b_{4} . h = the_left_translation_of (h,P) );

for G being Group

for H, P being Subgroup of G

for b

( b

begin

:: stabilizer

:: ALG I.5.2 Definition 3

:: ALG I.5.2 Definition 3

definition

let G be Group;

let E be non empty set ;

let T be LeftOperation of G,E;

let A be Subset of E;

ex b_{1} being strict Subgroup of G st the carrier of b_{1} = { g where g is Element of G : (T ^ g) .: A = A }

for b_{1}, b_{2} being strict Subgroup of G st the carrier of b_{1} = { g where g is Element of G : (T ^ g) .: A = A } & the carrier of b_{2} = { g where g is Element of G : (T ^ g) .: A = A } holds

b_{1} = b_{2}
by GROUP_2:59;

end;
let E be non empty set ;

let T be LeftOperation of G,E;

let A be Subset of E;

func the_strict_stabilizer_of (A,T) -> strict Subgroup of G means :Def10: :: GROUP_10:def 10

the carrier of it = { g where g is Element of G : (T ^ g) .: A = A } ;

existence the carrier of it = { g where g is Element of G : (T ^ g) .: A = A } ;

ex b

proof end;

uniqueness for b

b

:: deftheorem Def10 defines the_strict_stabilizer_of GROUP_10:def 10 :

for G being Group

for E being non empty set

for T being LeftOperation of G,E

for A being Subset of E

for b_{5} being strict Subgroup of G holds

( b_{5} = the_strict_stabilizer_of (A,T) iff the carrier of b_{5} = { g where g is Element of G : (T ^ g) .: A = A } );

for G being Group

for E being non empty set

for T being LeftOperation of G,E

for A being Subset of E

for b

( b

definition

let G be Group;

let E be non empty set ;

let T be LeftOperation of G,E;

let x be Element of E;

coherence

the_strict_stabilizer_of ({x},T) is strict Subgroup of G;

;

end;
let E be non empty set ;

let T be LeftOperation of G,E;

let x be Element of E;

func the_strict_stabilizer_of (x,T) -> strict Subgroup of G equals :: GROUP_10:def 11

the_strict_stabilizer_of ({x},T);

correctness the_strict_stabilizer_of ({x},T);

coherence

the_strict_stabilizer_of ({x},T) is strict Subgroup of G;

;

:: deftheorem defines the_strict_stabilizer_of GROUP_10:def 11 :

for G being Group

for E being non empty set

for T being LeftOperation of G,E

for x being Element of E holds the_strict_stabilizer_of (x,T) = the_strict_stabilizer_of ({x},T);

for G being Group

for E being non empty set

for T being LeftOperation of G,E

for x being Element of E holds the_strict_stabilizer_of (x,T) = the_strict_stabilizer_of ({x},T);

definition

let S be non empty unital multMagma ;

let E be set ;

let T be LeftOperation of S,E;

let x be Element of E;

end;
let E be set ;

let T be LeftOperation of S,E;

let x be Element of E;

pred x is_fixed_under T means :Def12: :: GROUP_10:def 12

for s being Element of S holds x = (T ^ s) . x;

for s being Element of S holds x = (T ^ s) . x;

:: deftheorem Def12 defines is_fixed_under GROUP_10:def 12 :

for S being non empty unital multMagma

for E being set

for T being LeftOperation of S,E

for x being Element of E holds

( x is_fixed_under T iff for s being Element of S holds x = (T ^ s) . x );

for S being non empty unital multMagma

for E being set

for T being LeftOperation of S,E

for x being Element of E holds

( x is_fixed_under T iff for s being Element of S holds x = (T ^ s) . x );

definition

let S be non empty unital multMagma ;

let E be set ;

let T be LeftOperation of S,E;

coherence

( ( not E is empty implies { x where x is Element of E : x is_fixed_under T } is Subset of E ) & ( E is empty implies {} E is Subset of E ) );

consistency

for b_{1} being Subset of E holds verum;

end;
let E be set ;

let T be LeftOperation of S,E;

func the_fixed_points_of T -> Subset of E equals :Def13: :: GROUP_10:def 13

{ x where x is Element of E : x is_fixed_under T } if not E is empty

otherwise {} E;

correctness { x where x is Element of E : x is_fixed_under T } if not E is empty

otherwise {} E;

coherence

( ( not E is empty implies { x where x is Element of E : x is_fixed_under T } is Subset of E ) & ( E is empty implies {} E is Subset of E ) );

consistency

for b

proof end;

:: deftheorem Def13 defines the_fixed_points_of GROUP_10:def 13 :

for S being non empty unital multMagma

for E being set

for T being LeftOperation of S,E holds

( ( not E is empty implies the_fixed_points_of T = { x where x is Element of E : x is_fixed_under T } ) & ( E is empty implies the_fixed_points_of T = {} E ) );

for S being non empty unital multMagma

for E being set

for T being LeftOperation of S,E holds

( ( not E is empty implies the_fixed_points_of T = { x where x is Element of E : x is_fixed_under T } ) & ( E is empty implies the_fixed_points_of T = {} E ) );

:: ALG I.5.4 Definition 5

definition

let S be non empty unital multMagma ;

let E be set ;

let T be LeftOperation of S,E;

let x, y be Element of E;

end;
let E be set ;

let T be LeftOperation of S,E;

let x, y be Element of E;

pred x,y are_conjugated_under T means :Def14: :: GROUP_10:def 14

ex s being Element of S st y = (T ^ s) . x;

ex s being Element of S st y = (T ^ s) . x;

:: deftheorem Def14 defines are_conjugated_under GROUP_10:def 14 :

for S being non empty unital multMagma

for E being set

for T being LeftOperation of S,E

for x, y being Element of E holds

( x,y are_conjugated_under T iff ex s being Element of S st y = (T ^ s) . x );

for S being non empty unital multMagma

for E being set

for T being LeftOperation of S,E

for x, y being Element of E holds

( x,y are_conjugated_under T iff ex s being Element of S st y = (T ^ s) . x );

theorem Th3: :: GROUP_10:3

for S being non empty unital multMagma

for E being non empty set

for x being Element of E

for T being LeftOperation of S,E holds x,x are_conjugated_under T

for E being non empty set

for x being Element of E

for T being LeftOperation of S,E holds x,x are_conjugated_under T

proof end;

theorem Th4: :: GROUP_10:4

for G being Group

for E being non empty set

for x, y being Element of E

for T being LeftOperation of G,E st x,y are_conjugated_under T holds

y,x are_conjugated_under T

for E being non empty set

for x, y being Element of E

for T being LeftOperation of G,E st x,y are_conjugated_under T holds

y,x are_conjugated_under T

proof end;

theorem Th5: :: GROUP_10:5

for S being non empty unital multMagma

for E being non empty set

for x, y, z being Element of E

for T being LeftOperation of S,E st x,y are_conjugated_under T & y,z are_conjugated_under T holds

x,z are_conjugated_under T

for E being non empty set

for x, y, z being Element of E

for T being LeftOperation of S,E st x,y are_conjugated_under T & y,z are_conjugated_under T holds

x,z are_conjugated_under T

proof end;

definition

let S be non empty unital multMagma ;

let E be non empty set ;

let T be LeftOperation of S,E;

let x be Element of E;

coherence

{ y where y is Element of E : x,y are_conjugated_under T } is Subset of E;

end;
let E be non empty set ;

let T be LeftOperation of S,E;

let x be Element of E;

func the_orbit_of (x,T) -> Subset of E equals :: GROUP_10:def 15

{ y where y is Element of E : x,y are_conjugated_under T } ;

correctness { y where y is Element of E : x,y are_conjugated_under T } ;

coherence

{ y where y is Element of E : x,y are_conjugated_under T } is Subset of E;

proof end;

:: deftheorem defines the_orbit_of GROUP_10:def 15 :

for S being non empty unital multMagma

for E being non empty set

for T being LeftOperation of S,E

for x being Element of E holds the_orbit_of (x,T) = { y where y is Element of E : x,y are_conjugated_under T } ;

for S being non empty unital multMagma

for E being non empty set

for T being LeftOperation of S,E

for x being Element of E holds the_orbit_of (x,T) = { y where y is Element of E : x,y are_conjugated_under T } ;

registration

let S be non empty unital multMagma ;

let E be non empty set ;

let x be Element of E;

let T be LeftOperation of S,E;

coherence

not the_orbit_of (x,T) is empty

end;
let E be non empty set ;

let x be Element of E;

let T be LeftOperation of S,E;

coherence

not the_orbit_of (x,T) is empty

proof end;

theorem Th6: :: GROUP_10:6

for G being Group

for E being non empty set

for x, y being Element of E

for T being LeftOperation of G,E holds

( the_orbit_of (x,T) misses the_orbit_of (y,T) or the_orbit_of (x,T) = the_orbit_of (y,T) )

for E being non empty set

for x, y being Element of E

for T being LeftOperation of G,E holds

( the_orbit_of (x,T) misses the_orbit_of (y,T) or the_orbit_of (x,T) = the_orbit_of (y,T) )

proof end;

theorem Th7: :: GROUP_10:7

for S being non empty unital multMagma

for E being non empty finite set

for x being Element of E

for T being LeftOperation of S,E st x is_fixed_under T holds

the_orbit_of (x,T) = {x}

for E being non empty finite set

for x being Element of E

for T being LeftOperation of S,E st x is_fixed_under T holds

the_orbit_of (x,T) = {x}

proof end;

:: the orbit-stabilizer theorem

theorem Th8: :: GROUP_10:8

for G being Group

for E being non empty set

for a being Element of E

for T being LeftOperation of G,E holds card (the_orbit_of (a,T)) = Index (the_strict_stabilizer_of (a,T))

for E being non empty set

for a being Element of E

for T being LeftOperation of G,E holds card (the_orbit_of (a,T)) = Index (the_strict_stabilizer_of (a,T))

proof end;

definition

let G be Group;

let E be non empty set ;

let T be LeftOperation of G,E;

coherence

{ X where X is Subset of E : ex x being Element of E st X = the_orbit_of (x,T) } is a_partition of E;

end;
let E be non empty set ;

let T be LeftOperation of G,E;

func the_orbits_of T -> a_partition of E equals :: GROUP_10:def 16

{ X where X is Subset of E : ex x being Element of E st X = the_orbit_of (x,T) } ;

correctness { X where X is Subset of E : ex x being Element of E st X = the_orbit_of (x,T) } ;

coherence

{ X where X is Subset of E : ex x being Element of E st X = the_orbit_of (x,T) } is a_partition of E;

proof end;

:: deftheorem defines the_orbits_of GROUP_10:def 16 :

for G being Group

for E being non empty set

for T being LeftOperation of G,E holds the_orbits_of T = { X where X is Subset of E : ex x being Element of E st X = the_orbit_of (x,T) } ;

for G being Group

for E being non empty set

for T being LeftOperation of G,E holds the_orbits_of T = { X where X is Subset of E : ex x being Element of E st X = the_orbit_of (x,T) } ;

begin

:: ALG I.6.5 Definition 9

:: deftheorem Def17 defines -group GROUP_10:def 17 :

for p being Nat

for G being Group holds

( G is p -group iff ex r being Nat st card G = p |^ r );

for p being Nat

for G being Group holds

( G is p -group iff ex r being Nat st card G = p |^ r );

Lm1: for n being non zero Nat holds card (INT.Group n) = n

proof end;

registration

let p be non zero Nat;

ex b_{1} being Group st

( b_{1} is p -group & b_{1} is finite & b_{1} is cyclic & b_{1} is commutative & b_{1} is strict )

end;
cluster non empty finite strict unital Group-like associative commutative cyclic p -group for multMagma ;

existence ex b

( b

proof end;

:: like WEDDWITT:39

:: ALG I.6.5 PRO 11

:: ALG I.6.5 PRO 11

theorem Th9: :: GROUP_10:9

for E being non empty finite set

for G being finite Group

for p being prime Nat

for T being LeftOperation of G,E st G is p -group holds

(card (the_fixed_points_of T)) mod p = (card E) mod p

for G being finite Group

for p being prime Nat

for T being LeftOperation of G,E st G is p -group holds

(card (the_fixed_points_of T)) mod p = (card E) mod p

proof end;

begin

:: ALG I.6.6 Definition 10

definition

let p be Nat;

let G be Group;

let P be Subgroup of G;

end;
let G be Group;

let P be Subgroup of G;

pred P is_Sylow_p-subgroup_of_prime p means :Def18: :: GROUP_10:def 18

( P is p -group & not p divides index P );

( P is p -group & not p divides index P );

:: deftheorem Def18 defines is_Sylow_p-subgroup_of_prime GROUP_10:def 18 :

for p being Nat

for G being Group

for P being Subgroup of G holds

( P is_Sylow_p-subgroup_of_prime p iff ( P is p -group & not p divides index P ) );

for p being Nat

for G being Group

for P being Subgroup of G holds

( P is_Sylow_p-subgroup_of_prime p iff ( P is p -group & not p divides index P ) );

Lm2: for n being Nat

for p being prime Nat st n <> 0 holds

ex m, r being Nat st

( n = (p |^ r) * m & not p divides m )

proof end;

Lm3: for X, Y being non empty set holds card { [:X,{y}:] where y is Element of Y : verum } = card Y

proof end;

Lm4: for G being finite Group

for E, T being non empty set

for LO being LeftOperation of G,E

for n being Nat 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 }

proof end;

Lm5: for n, m, r being Nat

for p being prime Nat st n = (p |^ r) * m & not p divides m holds

(n choose (p |^ r)) mod p <> 0

proof end;

Lm6: for r, n, m1, m2 being Nat

for p being prime Nat st (p |^ r) * n = m1 * m2 & not p divides n & not p divides m2 holds

p |^ r divides m1

proof end;

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)

proof end;

theorem Th10: :: GROUP_10:10

for G being finite Group

for p being prime Nat ex P being strict Subgroup of G st P is_Sylow_p-subgroup_of_prime p

for p being prime Nat ex P being strict Subgroup of G st P is_Sylow_p-subgroup_of_prime p

proof end;

Lm8: for n, r being Nat

for p being prime Nat st n divides p |^ r & n > 1 holds

p divides n

proof end;

:: ALG I.6.6 Corollary

:: The Cauchy theorem

:: The Cauchy theorem

theorem :: GROUP_10:11

for G being finite Group

for p being prime Nat st p divides card G holds

ex g being Element of G st ord g = p

for p being prime Nat st p divides card G holds

ex g being Element of G st ord g = p

proof end;

theorem Th12: :: GROUP_10:12

for G being finite Group

for p being prime Nat holds

( ( for H being Subgroup of G st H is p -group holds

ex P being Subgroup of G st

( P is_Sylow_p-subgroup_of_prime p & H is Subgroup of P ) ) & ( for P1, P2 being Subgroup of G st P1 is_Sylow_p-subgroup_of_prime p & P2 is_Sylow_p-subgroup_of_prime p holds

P1,P2 are_conjugated ) )

for p being prime Nat holds

( ( for H being Subgroup of G st H is p -group holds

ex P being Subgroup of G st

( P is_Sylow_p-subgroup_of_prime p & H is Subgroup of P ) ) & ( for P1, P2 being Subgroup of G st P1 is_Sylow_p-subgroup_of_prime p & P2 is_Sylow_p-subgroup_of_prime p holds

P1,P2 are_conjugated ) )

proof end;

definition

let G be Group;

let p be Nat;

coherence

{ H where H is Element of Subgroups G : ex P being strict Subgroup of G st

( P = H & P is_Sylow_p-subgroup_of_prime p ) } is Subset of (Subgroups G);

end;
let p be Nat;

func the_sylow_p-subgroups_of_prime (p,G) -> Subset of (Subgroups G) equals :: GROUP_10:def 19

{ H where H is Element of Subgroups G : ex P being strict Subgroup of G st

( P = H & P is_Sylow_p-subgroup_of_prime p ) } ;

correctness { H where H is Element of Subgroups G : ex P being strict Subgroup of G st

( P = H & P is_Sylow_p-subgroup_of_prime p ) } ;

coherence

{ H where H is Element of Subgroups G : ex P being strict Subgroup of G st

( P = H & P is_Sylow_p-subgroup_of_prime p ) } is Subset of (Subgroups G);

proof end;

:: deftheorem defines the_sylow_p-subgroups_of_prime GROUP_10:def 19 :

for G being Group

for p being Nat holds the_sylow_p-subgroups_of_prime (p,G) = { H where H is Element of Subgroups G : ex P being strict Subgroup of G st

( P = H & P is_Sylow_p-subgroup_of_prime p ) } ;

for G being Group

for p being Nat holds the_sylow_p-subgroups_of_prime (p,G) = { H where H is Element of Subgroups G : ex P being strict Subgroup of G st

( P = H & P is_Sylow_p-subgroup_of_prime p ) } ;

registration

let G be finite Group;

let p be prime Nat;

correctness

coherence

( not the_sylow_p-subgroups_of_prime (p,G) is empty & the_sylow_p-subgroups_of_prime (p,G) is finite );

end;
let p be prime Nat;

correctness

coherence

( not the_sylow_p-subgroups_of_prime (p,G) is empty & the_sylow_p-subgroups_of_prime (p,G) is finite );

proof end;

definition

let G be finite Group;

let p be prime Nat;

let H be Subgroup of G;

let h be Element of H;

ex b_{1} 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 = b_{1} . P1 & P1 = H1 & P2 = H2 & h " = g & H2 = H1 |^ g )

for b_{1}, b_{2} 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 = b_{1} . 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 = b_{2} . P1 & P1 = H1 & P2 = H2 & h " = g & H2 = H1 |^ g ) ) holds

b_{1} = b_{2}

end;
let p be prime Nat;

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 :Def20: :: GROUP_10:def 20

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 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 );

ex b

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 = b

proof end;

uniqueness for b

( P2 = b

( P2 = b

b

proof end;

:: deftheorem Def20 defines the_left_translation_of GROUP_10:def 20 :

for G being finite Group

for p being prime Nat

for H being Subgroup of G

for h being Element of H

for b_{5} being Function of (the_sylow_p-subgroups_of_prime (p,G)),(the_sylow_p-subgroups_of_prime (p,G)) holds

( b_{5} = the_left_translation_of (h,p) iff 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 = b_{5} . P1 & P1 = H1 & P2 = H2 & h " = g & H2 = H1 |^ g ) );

for G being finite Group

for p being prime Nat

for H being Subgroup of G

for h being Element of H

for b

( b

( P2 = b

definition

let G be finite Group;

let p be prime Nat;

let H be Subgroup of G;

ex b_{1} being LeftOperation of H,(the_sylow_p-subgroups_of_prime (p,G)) st

for h being Element of H holds b_{1} . h = the_left_translation_of (h,p)

for b_{1}, b_{2} being LeftOperation of H,(the_sylow_p-subgroups_of_prime (p,G)) st ( for h being Element of H holds b_{1} . h = the_left_translation_of (h,p) ) & ( for h being Element of H holds b_{2} . h = the_left_translation_of (h,p) ) holds

b_{1} = b_{2}

end;
let p be prime Nat;

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 :Def21: :: GROUP_10:def 21

for h being Element of H holds it . h = the_left_translation_of (h,p);

existence for h being Element of H holds it . h = the_left_translation_of (h,p);

ex b

for h being Element of H holds b

proof end;

uniqueness for b

b

proof end;

:: deftheorem Def21 defines the_left_operation_of GROUP_10:def 21 :

for G being finite Group

for p being prime Nat

for H being Subgroup of G

for b_{4} being LeftOperation of H,(the_sylow_p-subgroups_of_prime (p,G)) holds

( b_{4} = the_left_operation_of (H,p) iff for h being Element of H holds b_{4} . h = the_left_translation_of (h,p) );

for G being finite Group

for p being prime Nat

for H being Subgroup of G

for b

( b

Lm9: for G, H being finite Group

for p being prime Nat

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

proof end;

theorem :: GROUP_10:13

for G being finite Group

for p being prime Nat holds

( (card (the_sylow_p-subgroups_of_prime (p,G))) mod p = 1 & card (the_sylow_p-subgroups_of_prime (p,G)) divides card G )

for p being prime Nat holds

( (card (the_sylow_p-subgroups_of_prime (p,G))) mod p = 1 & card (the_sylow_p-subgroups_of_prime (p,G)) divides card G )

proof end;

begin

theorem :: GROUP_10:14

theorem :: GROUP_10:15

theorem :: GROUP_10:17