:: Cayley's Theorem
:: by Artur Korni{\l}owicz
::
:: Copyright (c) 2010-2021 Association of Mizar Users

registration
let X be set ;
cluster {} (X,{}) -> onto ;
coherence
{} (X,{}) is onto
;
end;

registration
coherence
for b1 being set st b1 is permutational holds
b1 is functional
proof end;
end;

definition
let X be set ;
func permutations X -> set equals :: CAYLEY:def 1
{ f where f is Permutation of X : verum } ;
coherence
{ f where f is Permutation of X : verum } is set
;
end;

:: deftheorem defines permutations CAYLEY:def 1 :
for X being set holds permutations X = { f where f is Permutation of X : verum } ;

theorem Th1: :: CAYLEY:1
for X, f being set st f in permutations X holds
f is Permutation of X
proof end;

theorem Th2: :: CAYLEY:2
for X being set holds permutations X c= Funcs (X,X)
proof end;

theorem Th3: :: CAYLEY:3
for n being Nat holds permutations (Seg n) = Permutations n
proof end;

registration
let X be set ;
coherence
( not permutations X is empty & permutations X is functional )
proof end;
end;

registration
let X be finite set ;
coherence
proof end;
end;

theorem Th4: :: CAYLEY:4
proof end;

definition
let X be set ;
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
ex b1 being strict constituted-Functions multMagma st
( the carrier of b1 = permutations X & ( for x, y being Element of b1 holds x * y = y * x ) )
proof end;
uniqueness
for b1, b2 being strict constituted-Functions multMagma st the carrier of b1 = permutations X & ( for x, y being Element of b1 holds x * y = y * x ) & the carrier of b2 = permutations X & ( for x, y being Element of b2 holds x * y = y * x ) holds
b1 = b2
proof end;
end;

:: deftheorem Def2 defines SymGroup CAYLEY:def 2 :
for X being set
for b2 being strict constituted-Functions multMagma holds
( b2 = SymGroup X iff ( the carrier of b2 = permutations X & ( for x, y being Element of b2 holds x * y = y * x ) ) );

theorem Th5: :: CAYLEY:5
for X being set
for f being Element of () holds f is Permutation of X
proof end;

registration
let X be set ;
coherence
( not SymGroup X is empty & SymGroup X is associative & SymGroup X is Group-like )
proof end;
end;

theorem Th6: :: CAYLEY:6
for X being set holds 1_ () = id X
proof end;

theorem :: CAYLEY:7
for X being set
for x being Element of () holds x " = x "
proof end;

registration
let n be Nat;
coherence
proof end;
end;

theorem :: CAYLEY:8
for n being Nat holds SymGroup (Seg n) = Group_of_Perm n
proof end;

registration
let X be finite set ;
coherence
proof end;
end;

theorem Th9: :: CAYLEY:9
proof end;

registration
coherence by Th9;
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;
func SymGroupsIso p -> Function of (),() means :Def3: :: CAYLEY:def 3
for x being Element of () holds it . x = (p * x) * (p ");
existence
ex b1 being Function of (),() st
for x being Element of () holds b1 . x = (p * x) * (p ")
proof end;
uniqueness
for b1, b2 being Function of (),() st ( for x being Element of () holds b1 . x = (p * x) * (p ") ) & ( for x being Element of () holds b2 . x = (p * x) * (p ") ) holds
b1 = b2
proof end;
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 b4 being Function of (),() holds
( b4 = SymGroupsIso p iff for x being Element of () holds b4 . x = (p * x) * (p ") );

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
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
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
proof end;

theorem :: CAYLEY:13
for X, Y being set st X,Y are_equipotent holds
SymGroup X, SymGroup Y are_isomorphic
proof end;

definition
let G be Group;
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
ex b1 being Function of G,(SymGroup the carrier of G) st
for g being Element of G holds b1 . g = * g
proof end;
uniqueness
for b1, b2 being Function of G,(SymGroup the carrier of G) st ( for g being Element of G holds b1 . g = * g ) & ( for g being Element of G holds b2 . g = * g ) holds
b1 = b2
proof end;
end;

:: deftheorem Def4 defines CayleyIso CAYLEY:def 4 :
for G being Group
for b2 being Function of G,(SymGroup the carrier of G) holds
( b2 = CayleyIso G iff for g being Element of G holds b2 . g = * g );

registration
let G be Group;
coherence
proof end;
end;

registration
let G be Group;
coherence
proof end;
end;

:: Cayley Theorem
theorem :: CAYLEY:14
for G being Group holds G, Image () are_isomorphic by GROUP_6:68;