:: Cayley's Theorem
:: by Artur Korni{\l}owicz
::
:: Received December 29, 2010
:: Copyright (c) 2010-2011 Association of Mizar Users


begin

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

registration
cluster permutational -> functional set ;
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 ;
cluster permutations X -> non empty functional ;
coherence
( not permutations X is empty & permutations X is functional )
proof end;
end;

registration
let X be finite set ;
cluster permutations X -> finite ;
coherence
permutations X is finite
proof end;
end;

theorem Th4: :: CAYLEY:4
permutations {} = 1
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 (SymGroup X) holds f is Permutation of X
proof end;

registration
let X be set ;
cluster SymGroup X -> non empty strict Group-like associative constituted-Functions ;
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_ (SymGroup X) = id X
proof end;

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

registration
let n be Nat;
cluster Group_of_Perm n -> constituted-Functions ;
coherence
Group_of_Perm n is constituted-Functions
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 ;
cluster SymGroup X -> finite strict constituted-Functions ;
coherence
SymGroup X is finite
proof end;
end;

theorem Th9: :: CAYLEY:9
SymGroup {} = Trivial-multMagma
proof end;

registration
cluster SymGroup {} -> trivial strict constituted-Functions ;
coherence
SymGroup {} is trivial
by Th9, CARD_1:87;
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 (SymGroup X),(SymGroup Y) means :Def3: :: CAYLEY:def 3
for x being Element of (SymGroup X) holds it . x = (p * x) * (p ");
existence
ex b1 being Function of (SymGroup X),(SymGroup Y) st
for x being Element of (SymGroup X) holds b1 . x = (p * x) * (p ")
proof end;
uniqueness
for b1, b2 being Function of (SymGroup X),(SymGroup Y) st ( for x being Element of (SymGroup X) holds b1 . x = (p * x) * (p ") ) & ( for x being Element of (SymGroup X) 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 (SymGroup X),(SymGroup Y) holds
( b4 = SymGroupsIso p iff for x being Element of (SymGroup X) 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;
cluster CayleyIso G -> multiplicative ;
coherence
CayleyIso G is multiplicative
proof end;
end;

registration
let G be Group;
cluster CayleyIso G -> one-to-one ;
coherence
CayleyIso G is one-to-one
proof end;
end;

theorem :: CAYLEY:14
for G being Group holds G, Image (CayleyIso G) are_isomorphic by GROUP_6:79;