:: Abelian Group of Matrices
:: by Katarzyna Jankowska
::
:: Received June 8, 1991
:: Copyright (c) 1991-2021 Association of Mizar Users

definition

let K be non empty 1-sorted ;
mode Matrix of K is Matrix of the carrier of K;
let n be Nat;
mode Matrix of n,K is Matrix of n,n, the carrier of K;
let m be Nat;
mode Matrix of n,m,K is Matrix of n,m, the carrier of K;

end;

definition

let K be non empty doubleLoopStr ;
let n be Nat;

func n -Matrices_over K -> set equals :: MATRIX_1:def 1
n -tuples_on (n -tuples_on the carrier of K);

coherence
n -tuples_on (n -tuples_on the carrier of K) is set ;

func 0. (K,n) -> Matrix of n,K equals :: MATRIX_1:def 2
n |-> (n |-> (0. K));

coherence
n |-> (n |-> (0. K)) is Matrix of n,K by MATRIX_0:10;

func 1. (K,n) -> Matrix of n,K means :Def3: :: MATRIX_1:def 3
( ( for i being Nat st [i,i] in Indices it holds
it * (i,i) = 1. K ) & ( for i, j being Nat st [i,j] in Indices it & i <> j holds
it * (i,j) = 0. K ) );

existence
ex b₁ being Matrix of n,K st
( ( for i being Nat st [i,i] in Indices b₁ holds
b₁ * (i,i) = 1. K ) & ( for i, j being Nat st [i,j] in Indices b₁ & i <> j holds
b₁ * (i,j) = 0. K ) )

proof end;

uniqueness
for b₁, b₂ being Matrix of n,K st ( for i being Nat st [i,i] in Indices b₁ holds
b₁ * (i,i) = 1. K ) & ( for i, j being Nat st [i,j] in Indices b₁ & i <> j holds
b₁ * (i,j) = 0. K ) & ( for i being Nat st [i,i] in Indices b₂ holds
b₂ * (i,i) = 1. K ) & ( for i, j being Nat st [i,j] in Indices b₂ & i <> j holds
b₂ * (i,j) = 0. K ) holds
b₁ = b₂

proof end;

let A be Matrix of n,K;

func - A -> Matrix of n,K means :Def4: :: MATRIX_1:def 4
for i, j being Nat st [i,j] in Indices A holds
it * (i,j) = - (A * (i,j));

existence
ex b₁ being Matrix of n,K st
for i, j being Nat st [i,j] in Indices A holds
b₁ * (i,j) = - (A * (i,j))

proof end;

uniqueness
for b₁, b₂ being Matrix of n,K st ( for i, j being Nat st [i,j] in Indices A holds
b₁ * (i,j) = - (A * (i,j)) ) & ( for i, j being Nat st [i,j] in Indices A holds
b₂ * (i,j) = - (A * (i,j)) ) holds
b₁ = b₂

proof end;

let B be Matrix of n,K;

func A + B -> Matrix of n,K means :Def5: :: MATRIX_1:def 5
for i, j being Nat st [i,j] in Indices A holds
it * (i,j) = (A * (i,j)) + (B * (i,j));

existence
ex b₁ being Matrix of n,K st
for i, j being Nat st [i,j] in Indices A holds
b₁ * (i,j) = (A * (i,j)) + (B * (i,j))

proof end;

uniqueness
for b₁, b₂ being Matrix of n,K st ( for i, j being Nat st [i,j] in Indices A holds
b₁ * (i,j) = (A * (i,j)) + (B * (i,j)) ) & ( for i, j being Nat st [i,j] in Indices A holds
b₂ * (i,j) = (A * (i,j)) + (B * (i,j)) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem defines -Matrices_over MATRIX_1:def 1 :
for K being non empty doubleLoopStr
for n being Nat holds n -Matrices_over K = n -tuples_on (n -tuples_on the carrier of K);

:: deftheorem defines 0. MATRIX_1:def 2 :
for K being non empty doubleLoopStr
for n being Nat holds 0. (K,n) = n |-> (n |-> (0. K));

:: deftheorem Def3 defines 1. MATRIX_1:def 3 :
for K being non empty doubleLoopStr
for n being Nat
for b₃ being Matrix of n,K holds
( b₃ = 1. (K,n) iff ( ( for i being Nat st [i,i] in Indices b₃ holds
b₃ * (i,i) = 1. K ) & ( for i, j being Nat st [i,j] in Indices b₃ & i <> j holds
b₃ * (i,j) = 0. K ) ) );

:: deftheorem Def4 defines - MATRIX_1:def 4 :
for K being non empty doubleLoopStr
for n being Nat
for A, b₄ being Matrix of n,K holds
( b₄ = - A iff for i, j being Nat st [i,j] in Indices A holds
b₄ * (i,j) = - (A * (i,j)) );

:: deftheorem Def5 defines + MATRIX_1:def 5 :
for K being non empty doubleLoopStr
for n being Nat
for A, B, b₅ being Matrix of n,K holds
( b₅ = A + B iff for i, j being Nat st [i,j] in Indices A holds
b₅ * (i,j) = (A * (i,j)) + (B * (i,j)) );

registration

let K be non empty doubleLoopStr ;
let n be Nat;

cluster n -Matrices_over K -> non empty ;

coherence
not n -Matrices_over K is empty ;

end;

theorem Th1: :: MATRIX_1:1

for i, j, n being Nat
for K being non empty doubleLoopStr st [i,j] in Indices (0. (K,n)) holds
(0. (K,n)) * (i,j) = 0. K

proof end;

theorem Th2: :: MATRIX_1:2

for x being object
for n being Nat
for K being non empty doubleLoopStr holds
( x is Element of n -Matrices_over K iff x is Matrix of n,K )

proof end;

definition

let K be non empty ZeroStr ;
let M be Matrix of K;

attr M is diagonal means :def6: :: MATRIX_1:def 6
for i, j being Nat st [i,j] in Indices M & M * (i,j) <> 0. K holds
i = j;

end;

:: deftheorem def6 defines diagonal MATRIX_1:def 6 :
for K being non empty ZeroStr
for M being Matrix of K holds
( M is diagonal iff for i, j being Nat st [i,j] in Indices M & M * (i,j) <> 0. K holds
i = j );

registration

let n be Nat;
let K be non empty doubleLoopStr ;

cluster Relation-like NAT -defined the carrier of K * -valued Function-like finite FinSequence-like FinSubsequence-like tabular V144( the carrier of K,n,n) diagonal for FinSequence of the carrier of K * ;

existence
ex b₁ being Matrix of n,K st b₁ is diagonal

proof end;

end;

theorem Th3: :: MATRIX_1:3

for n being Nat
for F being non empty right_complementable Abelian add-associative right_zeroed doubleLoopStr
for A, B being Matrix of n,F holds A + B = B + A

proof end;

theorem Th4: :: MATRIX_1:4

for n being Nat
for F being non empty right_complementable Abelian add-associative right_zeroed doubleLoopStr
for A, B, C being Matrix of n,F holds (A + B) + C = A + (B + C)

proof end;

theorem Th5: :: MATRIX_1:5

for n being Nat
for F being non empty right_complementable Abelian add-associative right_zeroed doubleLoopStr
for A being Matrix of n,F holds A + (0. (F,n)) = A

proof end;

theorem Th6: :: MATRIX_1:6

for n being Nat
for F being non empty right_complementable Abelian add-associative right_zeroed doubleLoopStr
for A being Matrix of n,F holds A + (- A) = 0. (F,n)

proof end;

definition

let F be non empty right_complementable Abelian add-associative right_zeroed doubleLoopStr ;
let n be Nat;

func n -G_Matrix_over F -> strict AbGroup means :: MATRIX_1:def 7
( the carrier of it = n -Matrices_over F & ( for A, B being Matrix of n,F holds the addF of it . (A,B) = A + B ) & 0. it = 0. (F,n) );

existence
ex b₁ being strict AbGroup st
( the carrier of b₁ = n -Matrices_over F & ( for A, B being Matrix of n,F holds the addF of b₁ . (A,B) = A + B ) & 0. b₁ = 0. (F,n) )

proof end;

uniqueness
for b₁, b₂ being strict AbGroup st the carrier of b₁ = n -Matrices_over F & ( for A, B being Matrix of n,F holds the addF of b₁ . (A,B) = A + B ) & 0. b₁ = 0. (F,n) & the carrier of b₂ = n -Matrices_over F & ( for A, B being Matrix of n,F holds the addF of b₂ . (A,B) = A + B ) & 0. b₂ = 0. (F,n) holds
b₁ = b₂

proof end;

end;

:: deftheorem defines -G_Matrix_over MATRIX_1:def 7 :
for F being non empty right_complementable Abelian add-associative right_zeroed doubleLoopStr
for n being Nat
for b₃ being strict AbGroup holds
( b₃ = n -G_Matrix_over F iff ( the carrier of b₃ = n -Matrices_over F & ( for A, B being Matrix of n,F holds the addF of b₃ . (A,B) = A + B ) & 0. b₃ = 0. (F,n) ) );

definition

let n be Nat;
let K be Field;
let M be Matrix of n,K;

attr M is upper_triangular means :: MATRIX_1:def 8
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_1:def 9
for i, j being Nat st [i,j] in Indices M & i < j holds
M * (i,j) = 0. K;

end;

:: deftheorem defines upper_triangular MATRIX_1:def 8 :
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_1:def 9 :
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 V144( the carrier of K,n,n) diagonal -> diagonal upper_triangular lower_triangular for FinSequence of the carrier of K * ;

coherence
for b₁ being diagonal Matrix of n,K holds
( b₁ is upper_triangular & b₁ is lower_triangular ) by def6;

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 V144( the carrier of K,n,n) upper_triangular lower_triangular for FinSequence of the carrier of K * ;

existence
ex b₁ being Matrix of n,K st
( b₁ is lower_triangular & b₁ is upper_triangular )

proof end;

end;

theorem :: MATRIX_1:7

for n being Nat
for K being Field
for a, b being Element of K holds ((n,n) --> a) + ((n,n) --> b) = (n,n) --> (a + b)

proof end;

definition

let IT be set ;

attr IT is permutational means :Def3: :: MATRIX_1:def 10
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_1:def 10 :
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 b₁ being set st
( b₁ is permutational & not b₁ is empty )

proof end;

end;

definition

let P be non empty permutational set ;

func len P -> Nat means :Def4: :: MATRIX_1:def 11
ex s being FinSequence st
( s in P & it = len s );

existence
ex b₁ being Nat ex s being FinSequence st
( s in P & b₁ = len s )

proof end;

uniqueness
for b₁, b₂ being Nat st ex s being FinSequence st
( s in P & b₁ = len s ) & ex s being FinSequence st
( s in P & b₂ = len s ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def4 defines len MATRIX_1:def 11 :
for P being non empty permutational set
for b₂ being Nat holds
( b₂ = len P iff ex s being FinSequence st
( s in P & b₂ = 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 b₁ being Element of P holds b₁ is Permutation of (Seg (len P))

proof end;

end;

theorem :: MATRIX_1:8

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_1:def 12
for x being set holds
( x in it iff x is Permutation of (Seg n) );

existence
ex b₁ being set st
for x being set holds
( x in b₁ iff x is Permutation of (Seg n) )

proof end;

uniqueness
for b₁, b₂ being set st ( for x being set holds
( x in b₁ iff x is Permutation of (Seg n) ) ) & ( for x being set holds
( x in b₂ iff x is Permutation of (Seg n) ) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def5 defines Permutations MATRIX_1:def 12 :
for n being Nat
for b₂ being set holds
( b₂ = Permutations n iff for x being set holds
( x in b₂ 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_1:9

for n being Nat holds len (Permutations n) = n

proof end;

theorem :: MATRIX_1:10

Permutations 1 = {(idseq 1)}

proof end;

definition

let n be Nat;

func Group_of_Perm n -> strict multMagma means :Def6: :: MATRIX_1:def 13
( 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 b₁ being strict multMagma st
( the carrier of b₁ = Permutations n & ( for q, p being Element of Permutations n holds the multF of b₁ . (q,p) = p * q ) )

proof end;

uniqueness
for b₁, b₂ being strict multMagma st the carrier of b₁ = Permutations n & ( for q, p being Element of Permutations n holds the multF of b₁ . (q,p) = p * q ) & the carrier of b₂ = Permutations n & ( for q, p being Element of Permutations n holds the multF of b₂ . (q,p) = p * q ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def6 defines Group_of_Perm MATRIX_1:def 13 :
for n being Nat
for b₂ being strict multMagma holds
( b₂ = Group_of_Perm n iff ( the carrier of b₂ = Permutations n & ( for q, p being Element of Permutations n holds the multF of b₂ . (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_1:11

for n being Nat holds idseq n is Element of (Group_of_Perm n)

proof end;

theorem Th6: :: MATRIX_1:12

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_1:13

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_1:14

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_1:15

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_1:def 14
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_1:def 14 :
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 :: MATRIX_1:def 15
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 defines even MATRIX_1:def 15 :
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_1:16

for n being Nat holds id (Seg n) is even

proof end;

definition

let K be Ring;
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_1:def 16
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 b₁ being Element of K holds verum;
;

end;

:: deftheorem defines - MATRIX_1:def 16 :
for K being Ring
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 ) );

registration

let n be Nat;

cluster Permutations n -> finite ;

coherence
Permutations n is finite

proof end;

end;