:: by Artur Korni{\l}owicz

::

:: Received December 29, 2010

:: Copyright (c) 2010-2021 Association of Mizar Users

registration
end;

:: deftheorem defines permutations CAYLEY:def 1 :

for X being set holds permutations X = { f where f is Permutation of X : verum } ;

for X being set holds permutations X = { f where f is Permutation of X : verum } ;

registration
end;

definition

let X be set ;

set c = permutations X;

ex b_{1} being strict constituted-Functions multMagma st

( the carrier of b_{1} = permutations X & ( for x, y being Element of b_{1} holds x * y = y * x ) )

for b_{1}, b_{2} being strict constituted-Functions multMagma st the carrier of b_{1} = permutations X & ( for x, y being Element of b_{1} holds x * y = y * x ) & the carrier of b_{2} = permutations X & ( for x, y being Element of b_{2} holds x * y = y * x ) holds

b_{1} = b_{2}

end;
set c = permutations X;

func SymGroup X -> strict constituted-Functions multMagma means :Def2: :: CAYLEY:def 2

( the carrier of it = permutations X & ( for x, y being Element of it holds x * y = y * x ) );

existence ( the carrier of it = permutations X & ( for x, y being Element of it holds x * y = y * x ) );

ex b

( the carrier of b

proof end;

uniqueness for b

b

proof end;

:: deftheorem Def2 defines SymGroup CAYLEY:def 2 :

for X being set

for b_{2} being strict constituted-Functions multMagma holds

( b_{2} = SymGroup X iff ( the carrier of b_{2} = permutations X & ( for x, y being Element of b_{2} holds x * y = y * x ) ) );

for X being set

for b

( b

registration

let X be set ;

coherence

( not SymGroup X is empty & SymGroup X is associative & SymGroup X is Group-like )

end;
coherence

( not SymGroup X is empty & SymGroup X is associative & SymGroup X is Group-like )

proof end;

definition

let X, Y be set ;

let p be Function of X,Y;

assume that

A1: ( X <> {} & Y <> {} ) and

A2: p is bijective ;

set G = SymGroup X;

set H = SymGroup Y;

ex b_{1} being Function of (SymGroup X),(SymGroup Y) st

for x being Element of (SymGroup X) holds b_{1} . x = (p * x) * (p ")

for b_{1}, b_{2} being Function of (SymGroup X),(SymGroup Y) st ( for x being Element of (SymGroup X) holds b_{1} . x = (p * x) * (p ") ) & ( for x being Element of (SymGroup X) holds b_{2} . x = (p * x) * (p ") ) holds

b_{1} = b_{2}

end;
let p be Function of X,Y;

assume that

A1: ( X <> {} & Y <> {} ) and

A2: p is bijective ;

set G = SymGroup X;

set H = SymGroup Y;

func SymGroupsIso p -> Function of (SymGroup X),(SymGroup Y) means :Def3: :: CAYLEY:def 3

for x being Element of (SymGroup X) holds it . x = (p * x) * (p ");

existence for x being Element of (SymGroup X) holds it . x = (p * x) * (p ");

ex b

for x being Element of (SymGroup X) holds b

proof end;

uniqueness for b

b

proof end;

:: deftheorem Def3 defines SymGroupsIso CAYLEY:def 3 :

for X, Y being set

for p being Function of X,Y st X <> {} & Y <> {} & p is bijective holds

for b_{4} being Function of (SymGroup X),(SymGroup Y) holds

( b_{4} = SymGroupsIso p iff for x being Element of (SymGroup X) holds b_{4} . x = (p * x) * (p ") );

for X, Y being set

for p being Function of X,Y st X <> {} & Y <> {} & p is bijective holds

for b

( b

theorem Th10: :: CAYLEY:10

for X, Y being non empty set

for p being Function of X,Y st p is bijective holds

SymGroupsIso p is multiplicative

for p being Function of X,Y st p is bijective holds

SymGroupsIso p is multiplicative

proof end;

theorem Th11: :: CAYLEY:11

for X, Y being non empty set

for p being Function of X,Y st p is bijective holds

SymGroupsIso p is one-to-one

for p being Function of X,Y st p is bijective holds

SymGroupsIso p is one-to-one

proof end;

theorem Th12: :: CAYLEY:12

for X, Y being non empty set

for p being Function of X,Y st p is bijective holds

SymGroupsIso p is onto

for p being Function of X,Y st p is bijective holds

SymGroupsIso p is onto

proof end;

definition

let G be Group;

ex b_{1} being Function of G,(SymGroup the carrier of G) st

for g being Element of G holds b_{1} . g = * g

for b_{1}, b_{2} being Function of G,(SymGroup the carrier of G) st ( for g being Element of G holds b_{1} . g = * g ) & ( for g being Element of G holds b_{2} . g = * g ) holds

b_{1} = b_{2}

end;
func CayleyIso G -> Function of G,(SymGroup the carrier of G) means :Def4: :: CAYLEY:def 4

for g being Element of G holds it . g = * g;

existence for g being Element of G holds it . g = * g;

ex b

for g being Element of G holds b

proof end;

uniqueness for b

b

proof end;

:: deftheorem Def4 defines CayleyIso CAYLEY:def 4 :

for G being Group

for b_{2} being Function of G,(SymGroup the carrier of G) holds

( b_{2} = CayleyIso G iff for g being Element of G holds b_{2} . g = * g );

for G being Group

for b

( b

registration
end;

:: Cayley Theorem