:: Cayley's Theorem
:: by Artur Korni{\l}owicz
::
:: Received December 29, 2010
:: Copyright (c) 2010-2016 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies RELAT_1, XBOOLE_0, FUNCT_1, SUBSET_1, MSSUBFAM, FUNCT_2, CAYLEY,
ALGSTR_0, GROUP_1, BINOP_1, STRUCT_0, WELLORD1, GROUP_6, NAT_1, FINSEQ_1,
TARSKI, MONOID_0, FINSET_1, FUNCT_5, ZFMISC_1, MATRIX_1;
notations TARSKI, XBOOLE_0, SUBSET_1, RELAT_1, FUNCT_1, RELSET_1, PARTFUN1,
FINSET_1, FUNCT_2, BINOP_1, ORDINAL1, FINSEQ_1, FUNCT_5, PARTIT_2,
STRUCT_0, ALGSTR_0, GROUP_1, GROUP_6, MONOID_0, TOPGRP_1, MATRIX_1;
constructors RELSET_1, GROUP_6, TOPGRP_1, BINOP_1, MATRIX_1, MONOID_0,
WELLORD2, PARTIT_2, FUNCT_5;
registrations XBOOLE_0, FUNCT_1, PARTFUN1, GROUP_2, STRUCT_0, TOPGRP_1,
FUNCT_2, MATRIX_1, RELSET_1, MONOID_0, FINSET_1, FRAENKEL, ZFMISC_1;
requirements SUBSET, BOOLE;
begin
reserve X,Y for set;
reserve G for Group;
reserve n for Nat;
registration
let X;
cluster {}(X,{}) -> onto;
end;
registration
cluster permutational -> functional for set;
end;
definition
let X;
func permutations(X) -> set equals
:: CAYLEY:def 1
the set of all f where f is Permutation of X;
end;
theorem :: CAYLEY:1
for f being set st f in permutations(X) holds f is Permutation of X;
theorem :: CAYLEY:2
permutations(X) c= Funcs(X,X);
theorem :: CAYLEY:3
permutations(Seg n) = Permutations(n);
registration
let X;
cluster permutations(X) -> non empty functional;
end;
registration
let X be finite set;
cluster permutations(X) -> finite;
end;
theorem :: CAYLEY:4
permutations {} = {{}};
definition
let X;
func SymGroup(X) -> strict constituted-Functions multMagma means
:: CAYLEY:def 2
the carrier of it = permutations(X) &
for x,y being Element of it holds x * y = y qua Function * x;
end;
theorem :: CAYLEY:5
for f being Element of SymGroup(X) holds f is Permutation of X;
registration
let X;
cluster SymGroup(X) -> non empty associative Group-like;
end;
theorem :: CAYLEY:6
1_SymGroup(X) = id X;
theorem :: CAYLEY:7
for x being Element of SymGroup(X) holds x" = x qua Function";
registration
let n;
cluster Group_of_Perm(n) -> constituted-Functions;
end;
theorem :: CAYLEY:8
SymGroup(Seg n) = Group_of_Perm(n);
registration
let X be finite set;
cluster SymGroup(X) -> finite;
end;
theorem :: CAYLEY:9
SymGroup({}) = Trivial-multMagma;
registration
cluster SymGroup {} -> trivial;
end;
definition
let X,Y;
let p be Function of X,Y such that
X <> {} & Y <> {} and
p is bijective;
func SymGroupsIso(p) -> Function of SymGroup(X),SymGroup(Y) means
:: CAYLEY:def 3
for x being Element of SymGroup(X) holds it.x = p*x*(p");
end;
theorem :: 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;
theorem :: 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;
theorem :: 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;
theorem :: CAYLEY:13
X,Y are_equipotent implies SymGroup(X),SymGroup(Y) are_isomorphic;
definition
let G;
func CayleyIso(G) -> Function of G,SymGroup(the carrier of G) means
:: CAYLEY:def 4
for g being Element of G holds it.g = *g;
end;
registration
let G;
cluster CayleyIso(G) -> multiplicative;
end;
registration
let G;
cluster CayleyIso(G) -> one-to-one;
end;
::$N Cayley Theorem
theorem :: CAYLEY:14
G, Image CayleyIso(G) are_isomorphic;