:: Transpose Matrices and Groups of Permutations
:: by Katarzyna Jankowska
::
:: Received May 20, 1992
:: Copyright (c) 1992-2012 Association of Mizar Users


definition
let n be Nat;
let K be Field;
let M be Matrix of n,K;
attr M is upper_triangular means :Def1: :: MATRIX_2:def 1
 for i, j being Nat st [i,j] in Indices M & i > j holds
M * (i,j) = 0. K;
attr M is lower_triangular means :: MATRIX_2:def 2
 for i, j being Nat st [i,j] in Indices M & i < j holds
M * (i,j) = 0. K;
end;

:: deftheorem Def1 defines upper_triangular MATRIX_2:def 1 :
for n being Nat
for K being Field
for M being Matrix of n,K holds
( M is upper_triangular iff for i, j being Nat st [i,j] in Indices M & i > j holds
M * (i,j) = 0. K );

:: deftheorem defines lower_triangular MATRIX_2:def 2 :
for n being Nat
for K being Field
for M being Matrix of n,K holds
( M is lower_triangular iff for i, j being Nat st [i,j] in Indices M & i < j holds
M * (i,j) = 0. K );

registration
let n be Nat;
let K be Field;
cluster tabular V162( the carrier of K,n,n) diagonal -> upper_triangular lower_triangular for FinSequence of the carrier of K * ;
coherence
for b1 being Diagonal of n,K holds
( b1 is upper_triangular & b1 is lower_triangular )
proof end;
end;

registration
let n be Nat;
let K be Field;
cluster Relation-like NAT -defined the carrier of K * -valued Function-like finite FinSequence-like FinSubsequence-like tabular V162( the carrier of K,n,n) upper_triangular lower_triangular for FinSequence of the carrier of K * ;
existence
ex b1 being Matrix of n,K st
( b1 is lower_triangular & b1 is upper_triangular )
proof end;
end;

definition
let n be Nat;
let K be Field;
mode Upper_Triangular_Matrix of n,K is upper_triangular Matrix of n,K;
mode Lower_Triangular_Matrix of n,K is lower_triangular Matrix of n,K;
end;

::$CT
theorem :: MATRIX_2:1
for n being Nat
for K being Field
for a9, b9 being Element of K holds ((n,n) --> a9) + ((n,n) --> b9) = (n,n) --> (a9 + b9)
proof end;

definition
let IT be set ;
attr IT is permutational means :Def3: :: MATRIX_2:def 3
 ex n being Nat st
for x being set st x in IT holds
x is Permutation of (Seg n);
end;

:: deftheorem Def3 defines permutational MATRIX_2:def 3 :
for IT being set holds
( IT is permutational iff ex n being Nat st
for x being set st x in IT holds
x is Permutation of (Seg n) );

registration
cluster non empty permutational for set ;
existence
ex b1 being set st
( b1 is permutational & not b1 is empty )
proof end;
end;

definition
let P be non empty permutational set ;
func len P -> Nat means :Def4: :: MATRIX_2:def 4
 ex s being FinSequence st
( s in P & it = len s );
existence
ex b1 being Nat ex s being FinSequence st
( s in P & b1 = len s )
proof end;
uniqueness
for b1, b2 being Nat st ex s being FinSequence st
( s in P & b1 = len s ) & ex s being FinSequence st
( s in P & b2 = len s ) holds
b1 = b2
proof end;
end;

:: deftheorem Def4 defines len MATRIX_2:def 4 :
for P being non empty permutational set
for b2 being Nat holds
( b2 = len P iff ex s being FinSequence st
( s in P & b2 = len s ) );

definition
let P be non empty permutational set ;
:: original: len
redefine func len P -> Element of NAT ;
coherence
len P is Element of NAT by ORDINAL1:def 12;
end;

definition
let P be non empty permutational set ;
:: original: Element
redefine mode Element of P -> Permutation of (Seg (len P));
coherence
for b1 being Element of P holds b1 is Permutation of (Seg (len P))
proof end;
end;

theorem :: MATRIX_2:2
for n being Nat ex P being non empty permutational set st len P = n
proof end;

definition
let n be Nat;
func Permutations n -> set means :Def5: :: MATRIX_2:def 5
 for x being set holds
( x in it iff x is Permutation of (Seg n) );
existence
ex b1 being set st
for x being set holds
( x in b1 iff x is Permutation of (Seg n) )
proof end;
uniqueness
for b1, b2 being set st ( for x being set holds
( x in b1 iff x is Permutation of (Seg n) ) ) & ( for x being set holds
( x in b2 iff x is Permutation of (Seg n) ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def5 defines Permutations MATRIX_2:def 5 :
for n being Nat
for b2 being set holds
( b2 = Permutations n iff for x being set holds
( x in b2 iff x is Permutation of (Seg n) ) );

registration
let n be Nat;
cluster Permutations n -> non empty permutational ;
coherence
( Permutations n is permutational & not Permutations n is empty )
proof end;
end;

theorem :: MATRIX_2:3
for n being Nat holds len (Permutations n) = n
proof end;

theorem :: MATRIX_2:4
Permutations 1 = {(idseq 1)}
proof end;

definition
let n be Nat;
func Group_of_Perm n -> strict multMagma means :Def6: :: MATRIX_2:def 6
( the carrier of it = Permutations n & ( for q, p being Element of Permutations n holds the multF of it . (q,p) = p * q ) );
existence
ex b1 being strict multMagma st
( the carrier of b1 = Permutations n & ( for q, p being Element of Permutations n holds the multF of b1 . (q,p) = p * q ) )
proof end;
uniqueness
for b1, b2 being strict multMagma st the carrier of b1 = Permutations n & ( for q, p being Element of Permutations n holds the multF of b1 . (q,p) = p * q ) & the carrier of b2 = Permutations n & ( for q, p being Element of Permutations n holds the multF of b2 . (q,p) = p * q ) holds
b1 = b2
proof end;
end;

:: deftheorem Def6 defines Group_of_Perm MATRIX_2:def 6 :
for n being Nat
for b2 being strict multMagma holds
( b2 = Group_of_Perm n iff ( the carrier of b2 = Permutations n & ( for q, p being Element of Permutations n holds the multF of b2 . (q,p) = p * q ) ) );

registration
let n be Nat;
cluster Group_of_Perm n -> non empty strict ;
coherence
not Group_of_Perm n is empty
proof end;
end;

theorem Th5: :: MATRIX_2:5
for n being Nat holds idseq n is Element of (Group_of_Perm n)
proof end;

theorem Th6: :: MATRIX_2:6
for n being Nat
for p being Element of Permutations n holds
( p * (idseq n) = p & (idseq n) * p = p )
proof end;

theorem Th7: :: MATRIX_2:7
for n being Nat
for p being Element of Permutations n holds
( p * (p ") = idseq n & (p ") * p = idseq n )
proof end;

theorem Th8: :: MATRIX_2:8
for n being Nat
for p being Element of Permutations n holds p " is Element of (Group_of_Perm n)
proof end;

registration
let n be Nat;
cluster Group_of_Perm n -> strict Group-like associative ;
coherence
( Group_of_Perm n is associative & Group_of_Perm n is Group-like )
proof end;
end;

theorem Th9: :: MATRIX_2:9
for n being Nat holds idseq n = 1_ (Group_of_Perm n)
proof end;

definition
let n be Nat;
let p be Permutation of (Seg n);
attr p is being_transposition means :: MATRIX_2:def 7
 ex i, j being Nat st
( i in dom p & j in dom p & i <> j & p . i = j & p . j = i & ( for k being Nat st k <> i & k <> j & k in dom p holds
p . k = k ) );
end;

:: deftheorem defines being_transposition MATRIX_2:def 7 :
for n being Nat
for p being Permutation of (Seg n) holds
( p is being_transposition iff ex i, j being Nat st
( i in dom p & j in dom p & i <> j & p . i = j & p . j = i & ( for k being Nat st k <> i & k <> j & k in dom p holds
p . k = k ) ) );

definition
let n be Nat;
let IT be Permutation of (Seg n);
attr IT is even means :Def8: :: MATRIX_2:def 8
 ex l being FinSequence of (Group_of_Perm n) st
( (len l) mod 2 = 0 & IT = Product l & ( for i being Nat st i in dom l holds
ex q being Element of Permutations n st
( l . i = q & q is being_transposition ) ) );
end;

:: deftheorem Def8 defines even MATRIX_2:def 8 :
for n being Nat
for IT being Permutation of (Seg n) holds
( IT is even iff ex l being FinSequence of (Group_of_Perm n) st
( (len l) mod 2 = 0 & IT = Product l & ( for i being Nat st i in dom l holds
ex q being Element of Permutations n st
( l . i = q & q is being_transposition ) ) ) );

notation
let n be Nat;
let IT be Permutation of (Seg n);
antonym odd IT for even ;
end;

theorem :: MATRIX_2:10
for n being Nat holds id (Seg n) is even
proof end;

definition
let K be Field;
let n be Nat;
let x be Element of K;
let p be Element of Permutations n;
func - (x,p) -> Element of K equals :: MATRIX_2:def 9
x if p is even
otherwise - x;
correctness
coherence
( ( p is even implies x is Element of K ) & ( not p is even implies - x is Element of K ) );
consistency
for b1 being Element of K holds verum;
;
end;

:: deftheorem defines - MATRIX_2:def 9 :
for K being Field
for n being Nat
for x being Element of K
for p being Element of Permutations n holds
( ( p is even implies - (x,p) = x ) & ( not p is even implies - (x,p) = - x ) );

definition
let X be set ;
assume A1: X is finite ;
func FinOmega X -> Element of Fin X equals :: MATRIX_2:def 10
X;
coherence
X is Element of Fin X by A1, FINSUB_1:def 5;
end;

:: deftheorem defines FinOmega MATRIX_2:def 10 :
for X being set st X is finite holds
FinOmega X = X;

theorem :: MATRIX_2:11
for n being Nat holds Permutations n is finite
proof end;