:: 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 b₁ being set st b₁ is permutational holds
b₁ 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 b₁ being strict constituted-Functions multMagma st
( the carrier of b₁ = permutations X & ( for x, y being Element of b₁ holds x * y = y * x ) )

proof end;

uniqueness
for b₁, b₂ being strict constituted-Functions multMagma st the carrier of b₁ = permutations X & ( for x, y being Element of b₁ holds x * y = y * x ) & the carrier of b₂ = permutations X & ( for x, y being Element of b₂ holds x * y = y * x ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def2 defines SymGroup CAYLEY:def 2 :
for X being set
for b₂ being strict constituted-Functions multMagma holds
( b₂ = SymGroup X iff ( the carrier of b₂ = permutations X & ( for x, y being Element of b₂ 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 b₁ being Function of (SymGroup X),(SymGroup Y) st
for x being Element of (SymGroup X) holds b₁ . x = (p * x) * (p ")

proof end;

uniqueness
for b₁, b₂ being Function of (SymGroup X),(SymGroup Y) st ( for x being Element of (SymGroup X) holds b₁ . x = (p * x) * (p ") ) & ( for x being Element of (SymGroup X) holds b₂ . x = (p * x) * (p ") ) holds
b₁ = b₂

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 b₄ being Function of (SymGroup X),(SymGroup Y) holds
( b₄ = SymGroupsIso p iff for x being Element of (SymGroup X) holds b₄ . 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 b₁ being Function of G,(SymGroup the carrier of G) st
for g being Element of G holds b₁ . g = * g

proof end;

uniqueness
for b₁, b₂ being Function of G,(SymGroup the carrier of G) st ( for g being Element of G holds b₁ . g = * g ) & ( for g being Element of G holds b₂ . g = * g ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def4 defines CayleyIso CAYLEY:def 4 :
for G being Group
for b₂ being Function of G,(SymGroup the carrier of G) holds
( b₂ = CayleyIso G iff for g being Element of G holds b₂ . 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;