:: Jordan Matrix Decomposition
:: by Karol P\c{a}k
::
:: Received July 11, 2008
:: Copyright (c) 2008-2021 Association of Mizar Users


Lm1: for x, y being set
for f being Function st f is one-to-one & x in dom f holds
rng (f +* (x,y)) = ((rng f) \ {(f . x)}) \/ {y}
proof end;

definition
let K be Field;
let L be Element of K;
let n be Nat;
func Jordan_block (L,n) -> Matrix of K means :Def1: :: MATRIXJ2:def 1
( len it = n & width it = n & ( for i, j being Nat st [i,j] in Indices it holds
( ( i = j implies it * (i,j) = L ) & ( i + 1 = j implies it * (i,j) = 1_ K ) & ( i <> j & i + 1 <> j implies it * (i,j) = 0. K ) ) ) );
existence
ex b1 being Matrix of K st
( len b1 = n & width b1 = n & ( for i, j being Nat st [i,j] in Indices b1 holds
( ( i = j implies b1 * (i,j) = L ) & ( i + 1 = j implies b1 * (i,j) = 1_ K ) & ( i <> j & i + 1 <> j implies b1 * (i,j) = 0. K ) ) ) )
proof end;
uniqueness
for b1, b2 being Matrix of K st len b1 = n & width b1 = n & ( for i, j being Nat st [i,j] in Indices b1 holds
( ( i = j implies b1 * (i,j) = L ) & ( i + 1 = j implies b1 * (i,j) = 1_ K ) & ( i <> j & i + 1 <> j implies b1 * (i,j) = 0. K ) ) ) & len b2 = n & width b2 = n & ( for i, j being Nat st [i,j] in Indices b2 holds
( ( i = j implies b2 * (i,j) = L ) & ( i + 1 = j implies b2 * (i,j) = 1_ K ) & ( i <> j & i + 1 <> j implies b2 * (i,j) = 0. K ) ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def1 defines Jordan_block MATRIXJ2:def 1 :
for K being Field
for L being Element of K
for n being Nat
for b4 being Matrix of K holds
( b4 = Jordan_block (L,n) iff ( len b4 = n & width b4 = n & ( for i, j being Nat st [i,j] in Indices b4 holds
( ( i = j implies b4 * (i,j) = L ) & ( i + 1 = j implies b4 * (i,j) = 1_ K ) & ( i <> j & i + 1 <> j implies b4 * (i,j) = 0. K ) ) ) ) );

definition
let K be Field;
let L be Element of K;
let n be Nat;
:: original: Jordan_block
redefine func Jordan_block (L,n) -> upper_triangular Matrix of n,K;
coherence
Jordan_block (L,n) is upper_triangular Matrix of n,K
proof end;
end;

theorem Th1: :: MATRIXJ2:1
for n being Nat
for K being Field
for L being Element of K holds diagonal_of_Matrix (Jordan_block (L,n)) = n |-> L
proof end;

theorem Th2: :: MATRIXJ2:2
for n being Nat
for K being Field
for L being Element of K holds Det (Jordan_block (L,n)) = (power K) . (L,n)
proof end;

theorem Th3: :: MATRIXJ2:3
for n being Nat
for K being Field
for L being Element of K holds
( Jordan_block (L,n) is invertible iff ( n = 0 or L <> 0. K ) )
proof end;

theorem Th4: :: MATRIXJ2:4
for i, n being Nat
for K being Field
for L being Element of K st i in Seg n & i <> n holds
Line ((Jordan_block (L,n)),i) = (L * (Line ((1. (K,n)),i))) + (Line ((1. (K,n)),(i + 1)))
proof end;

theorem Th5: :: MATRIXJ2:5
for n being Nat
for K being Field
for L being Element of K holds Line ((Jordan_block (L,n)),n) = L * (Line ((1. (K,n)),n))
proof end;

theorem Th6: :: MATRIXJ2:6
for i, n being Nat
for K being Field
for L being Element of K
for F being Element of n -tuples_on the carrier of K st i in Seg n holds
( ( i <> n implies (Line ((Jordan_block (L,n)),i)) "*" F = (L * (F /. i)) + (F /. (i + 1)) ) & ( i = n implies (Line ((Jordan_block (L,n)),i)) "*" F = L * (F /. i) ) )
proof end;

theorem Th7: :: MATRIXJ2:7
for i, n being Nat
for K being Field
for L being Element of K
for F being Element of n -tuples_on the carrier of K st i in Seg n holds
( ( i = 1 implies (Col ((Jordan_block (L,n)),i)) "*" F = L * (F /. i) ) & ( i <> 1 implies (Col ((Jordan_block (L,n)),i)) "*" F = (L * (F /. i)) + (F /. (i - 1)) ) )
proof end;

theorem :: MATRIXJ2:8
for n being Nat
for K being Field
for L being Element of K st L <> 0. K holds
ex M being Matrix of n,K st
( (Jordan_block (L,n)) ~ = M & ( for i, j being Nat st [i,j] in Indices M holds
( ( i > j implies M * (i,j) = 0. K ) & ( i <= j implies M * (i,j) = - ((power K) . ((- (L ")),((j -' i) + 1))) ) ) ) )
proof end;

theorem Th9: :: MATRIXJ2:9
for n being Nat
for K being Field
for a, L being Element of K holds (Jordan_block (L,n)) + (a * (1. (K,n))) = Jordan_block ((L + a),n)
proof end;

definition
let K be Field;
let G be FinSequence of ( the carrier of K *) * ;
attr G is Jordan-block-yielding means :Def2: :: MATRIXJ2:def 2
 for i being Nat st i in dom G holds
ex L being Element of K ex n being Nat st G . i = Jordan_block (L,n);
end;

:: deftheorem Def2 defines Jordan-block-yielding MATRIXJ2:def 2 :
for K being Field
for G being FinSequence of ( the carrier of K *) * holds
( G is Jordan-block-yielding iff for i being Nat st i in dom G holds
ex L being Element of K ex n being Nat st G . i = Jordan_block (L,n) );

registration
let K be Field;
cluster Relation-like NAT -defined ( the carrier of K *) * -valued Function-like finite FinSequence-like FinSubsequence-like Function-yielding V186() Jordan-block-yielding for FinSequence of ( the carrier of K *) * ;
existence
ex b1 being FinSequence of ( the carrier of K *) * st b1 is Jordan-block-yielding
proof end;
end;

registration
let K be Field;
cluster Jordan-block-yielding -> Square-Matrix-yielding for FinSequence of ( the carrier of K *) * ;
coherence
for b1 being FinSequence of ( the carrier of K *) * st b1 is Jordan-block-yielding holds
b1 is Square-Matrix-yielding
proof end;
end;

definition
let K be Field;
mode FinSequence_of_Jordan_block of K is Jordan-block-yielding FinSequence of ( the carrier of K *) * ;
end;

Lm2: for K being Field holds {} is FinSequence_of_Jordan_block of K
proof end;

definition
let K be Field;
let L be Element of K;
mode FinSequence_of_Jordan_block of L,K -> FinSequence_of_Jordan_block of K means :Def3: :: MATRIXJ2:def 3
 for i being Nat st i in dom it holds
ex n being Nat st it . i = Jordan_block (L,n);
existence
ex b1 being FinSequence_of_Jordan_block of K st
for i being Nat st i in dom b1 holds
ex n being Nat st b1 . i = Jordan_block (L,n)
proof end;
end;

:: deftheorem Def3 defines FinSequence_of_Jordan_block MATRIXJ2:def 3 :
for K being Field
for L being Element of K
for b3 being FinSequence_of_Jordan_block of K holds
( b3 is FinSequence_of_Jordan_block of L,K iff for i being Nat st i in dom b3 holds
ex n being Nat st b3 . i = Jordan_block (L,n) );

theorem Th10: :: MATRIXJ2:10
for K being Field
for L being Element of K holds {} is FinSequence_of_Jordan_block of L,K
proof end;

theorem Th11: :: MATRIXJ2:11
for n being Nat
for K being Field
for L being Element of K holds <*(Jordan_block (L,n))*> is FinSequence_of_Jordan_block of L,K
proof end;

registration
let K be Field;
let L be Element of K;
cluster Relation-like non-empty NAT -defined ( the carrier of K *) * -valued Function-like finite FinSequence-like FinSubsequence-like Function-yielding V186() Matrix-yielding Square-Matrix-yielding Jordan-block-yielding for FinSequence_of_Jordan_block of L,K;
existence
ex b1 being FinSequence_of_Jordan_block of L,K st b1 is non-empty
proof end;
end;

registration
let K be Field;
cluster Relation-like non-empty NAT -defined ( the carrier of K *) * -valued Function-like finite FinSequence-like FinSubsequence-like Function-yielding V186() Matrix-yielding Square-Matrix-yielding Jordan-block-yielding for FinSequence of ( the carrier of K *) * ;
existence
ex b1 being FinSequence_of_Jordan_block of K st b1 is non-empty
proof end;
end;

theorem Th12: :: MATRIXJ2:12
for K being Field
for a, L being Element of K
for J being FinSequence_of_Jordan_block of L,K holds J (+) (mlt (((len J) |-> a),(1. (K,(Len J))))) is FinSequence_of_Jordan_block of L + a,K
proof end;

definition
let K be Field;
let J1, J2 be FinSequence_of_Jordan_block of K;
:: original: ^
redefine func J1 ^ J2 -> FinSequence_of_Jordan_block of K;
coherence
J1 ^ J2 is FinSequence_of_Jordan_block of K
proof end;
end;

definition
let K be Field;
let n be Nat;
let J be FinSequence_of_Jordan_block of K;
:: original: |
redefine func J | n -> FinSequence_of_Jordan_block of K;
coherence
J | n is FinSequence_of_Jordan_block of K
proof end;
:: original: /^
redefine func J /^ n -> FinSequence_of_Jordan_block of K;
coherence
J /^ n is FinSequence_of_Jordan_block of K
proof end;
end;

definition
let K be Field;
let L be Element of K;
let J1, J2 be FinSequence_of_Jordan_block of L,K;
:: original: ^
redefine func J1 ^ J2 -> FinSequence_of_Jordan_block of L,K;
coherence
J1 ^ J2 is FinSequence_of_Jordan_block of L,K
proof end;
end;

definition
let K be Field;
let L be Element of K;
let n be Nat;
let J be FinSequence_of_Jordan_block of L,K;
:: original: |
redefine func J | n -> FinSequence_of_Jordan_block of L,K;
coherence
J | n is FinSequence_of_Jordan_block of L,K
proof end;
:: original: /^
redefine func J /^ n -> FinSequence_of_Jordan_block of L,K;
coherence
J /^ n is FinSequence_of_Jordan_block of L,K
proof end;
end;

definition
let K be doubleLoopStr ;
let V be non empty ModuleStr over K;
let f be Function of V,V;
attr f is nilpotent means :Def4: :: MATRIXJ2:def 4
 ex n being Nat st
for v being Vector of V holds (f |^ n) . v = 0. V;
end;

:: deftheorem Def4 defines nilpotent MATRIXJ2:def 4 :
for K being doubleLoopStr
for V being non empty ModuleStr over K
for f being Function of V,V holds
( f is nilpotent iff ex n being Nat st
for v being Vector of V holds (f |^ n) . v = 0. V );

theorem Th13: :: MATRIXJ2:13
for K being doubleLoopStr
for V being non empty ModuleStr over K
for f being Function of V,V holds
( f is nilpotent iff ex n being Nat st f |^ n = ZeroMap (V,V) )
proof end;

registration
let K be doubleLoopStr ;
let V be non empty ModuleStr over K;
cluster Relation-like the carrier of V -defined the carrier of V -valued Function-like non empty total V18( the carrier of V, the carrier of V) nilpotent for Element of bool [: the carrier of V, the carrier of V:];
existence
ex b1 being Function of V,V st b1 is nilpotent
proof end;
end;

registration
let R be Ring;
let V be LeftMod of R;
cluster Relation-like the carrier of V -defined the carrier of V -valued Function-like non empty total V18( the carrier of V, the carrier of V) additive homogeneous nilpotent for Element of bool [: the carrier of V, the carrier of V:];
existence
ex b1 being Function of V,V st
( b1 is nilpotent & b1 is additive & b1 is homogeneous )
proof end;
end;

theorem Th14: :: MATRIXJ2:14
for n being Nat
for K being Field
for V being VectSp of K
for f being linear-transformation of V,V holds f | (ker (f |^ n)) is nilpotent linear-transformation of (ker (f |^ n)),(ker (f |^ n))
proof end;

definition
let K be doubleLoopStr ;
let V be non empty ModuleStr over K;
let f be nilpotent Function of V,V;
func degree_of_nilpotent f -> Nat means :Def5: :: MATRIXJ2:def 5
( f |^ it = ZeroMap (V,V) & ( for k being Nat st f |^ k = ZeroMap (V,V) holds
it <= k ) );
existence
ex b1 being Nat st
( f |^ b1 = ZeroMap (V,V) & ( for k being Nat st f |^ k = ZeroMap (V,V) holds
b1 <= k ) )
proof end;
uniqueness
for b1, b2 being Nat st f |^ b1 = ZeroMap (V,V) & ( for k being Nat st f |^ k = ZeroMap (V,V) holds
b1 <= k ) & f |^ b2 = ZeroMap (V,V) & ( for k being Nat st f |^ k = ZeroMap (V,V) holds
b2 <= k ) holds
b1 = b2
proof end;
end;

:: deftheorem Def5 defines degree_of_nilpotent MATRIXJ2:def 5 :
for K being doubleLoopStr
for V being non empty ModuleStr over K
for f being nilpotent Function of V,V
for b4 being Nat holds
( b4 = degree_of_nilpotent f iff ( f |^ b4 = ZeroMap (V,V) & ( for k being Nat st f |^ k = ZeroMap (V,V) holds
b4 <= k ) ) );

notation
let K be doubleLoopStr ;
let V be non empty ModuleStr over K;
let f be nilpotent Function of V,V;
synonym deg f for degree_of_nilpotent f;
end;

theorem Th15: :: MATRIXJ2:15
for K being doubleLoopStr
for V being non empty ModuleStr over K
for f being nilpotent Function of V,V holds
( deg f = 0 iff [#] V = {(0. V)} )
proof end;

theorem Th16: :: MATRIXJ2:16
for K being doubleLoopStr
for V being non empty ModuleStr over K
for f being nilpotent Function of V,V ex v being Vector of V st
for i being Nat st i < deg f holds
(f |^ i) . v <> 0. V
proof end;

theorem Th17: :: MATRIXJ2:17
for K being Field
for V being VectSp of K
for W being Subspace of V
for f being nilpotent Function of V,V st f | W is Function of W,W holds
f | W is nilpotent Function of W,W
proof end;

theorem Th18: :: MATRIXJ2:18
for n being Nat
for K being Field
for V being VectSp of K
for W being Subspace of V
for f being nilpotent linear-transformation of V,V
for fI being nilpotent Function of (im (f |^ n)),(im (f |^ n)) st fI = f | (im (f |^ n)) & n <= deg f holds
(deg fI) + n = deg f
proof end;

theorem Th19: :: MATRIXJ2:19
for i being Nat
for K being Field
for V1, V2 being finite-dimensional VectSp of K
for W1, W2 being Subspace of V1
for U1, U2 being Subspace of V2
for b1 being OrdBasis of V1
for B2 being FinSequence of V2
for bw1 being OrdBasis of W1
for bw2 being OrdBasis of W2
for Bu1 being FinSequence of U1
for Bu2 being FinSequence of U2
for M being Matrix of len b1, len B2,K
for M1 being Matrix of len bw1, len Bu1,K
for M2 being Matrix of len bw2, len Bu2,K st b1 = bw1 ^ bw2 & B2 = Bu1 ^ Bu2 & M = block_diagonal (<*M1,M2*>,(0. K)) & width M1 = len Bu1 & width M2 = len Bu2 holds
( ( i in dom bw1 implies (Mx2Tran (M,b1,B2)) . (b1 /. i) = (Mx2Tran (M1,bw1,Bu1)) . (bw1 /. i) ) & ( i in dom bw2 implies (Mx2Tran (M,b1,B2)) . (b1 /. (i + (len bw1))) = (Mx2Tran (M2,bw2,Bu2)) . (bw2 /. i) ) )
proof end;

theorem Th20: :: MATRIXJ2:20
for K being Field
for V1, V2 being finite-dimensional VectSp of K
for b1 being OrdBasis of V1
for B2 being FinSequence of V2
for M being Matrix of len b1, len B2,K
for F being FinSequence_of_Matrix of K st M = block_diagonal (F,(0. K)) holds
for i, m being Nat st i in dom b1 & m = min ((Len F),i) holds
( (Mx2Tran (M,b1,B2)) . (b1 /. i) = Sum (lmlt ((Line ((F . m),(i -' (Sum (Len (F | (m -' 1))))))),((B2 | (Sum (Width (F | m)))) /^ (Sum (Width (F | (m -' 1))))))) & len ((B2 | (Sum (Width (F | m)))) /^ (Sum (Width (F | (m -' 1))))) = width (F . m) )
proof end;

theorem Th21: :: MATRIXJ2:21
for K being Field
for L being Element of K
for V1 being finite-dimensional VectSp of K
for B1 being FinSequence of V1 st len B1 in dom B1 holds
Sum (lmlt ((Line ((Jordan_block (L,(len B1))),(len B1))),B1)) = L * (B1 /. (len B1))
proof end;

theorem Th22: :: MATRIXJ2:22
for i being Nat
for K being Field
for L being Element of K
for V1 being finite-dimensional VectSp of K
for B1 being FinSequence of V1 st i in dom B1 & i <> len B1 holds
Sum (lmlt ((Line ((Jordan_block (L,(len B1))),i)),B1)) = (L * (B1 /. i)) + (B1 /. (i + 1))
proof end;

theorem Th23: :: MATRIXJ2:23
for n being Nat
for K being Field
for L being Element of K
for V1, V2 being finite-dimensional VectSp of K
for b1 being OrdBasis of V1
for B2 being FinSequence of V2
for M being Matrix of len b1, len B2,K st M = Jordan_block (L,n) holds
for i being Nat st i in dom b1 holds
( ( i = len b1 implies (Mx2Tran (M,b1,B2)) . (b1 /. i) = L * (B2 /. i) ) & ( i <> len b1 implies (Mx2Tran (M,b1,B2)) . (b1 /. i) = (L * (B2 /. i)) + (B2 /. (i + 1)) ) )
proof end;

theorem Th24: :: MATRIXJ2:24
for K being Field
for L being Element of K
for V1, V2 being finite-dimensional VectSp of K
for b1 being OrdBasis of V1
for B2 being FinSequence of V2
for J being FinSequence_of_Jordan_block of L,K
for M being Matrix of len b1, len B2,K st M = block_diagonal (J,(0. K)) holds
for i, m being Nat st i in dom b1 & m = min ((Len J),i) holds
( ( i = Sum (Len (J | m)) implies (Mx2Tran (M,b1,B2)) . (b1 /. i) = L * (B2 /. i) ) & ( i <> Sum (Len (J | m)) implies (Mx2Tran (M,b1,B2)) . (b1 /. i) = (L * (B2 /. i)) + (B2 /. (i + 1)) ) )
proof end;

theorem Th25: :: MATRIXJ2:25
for K being Field
for V1 being finite-dimensional VectSp of K
for b1 being OrdBasis of V1
for J being FinSequence_of_Jordan_block of 0. K,K
for M being Matrix of len b1, len b1,K st M = block_diagonal (J,(0. K)) holds
for m being Nat st ( for i being Nat st i in dom J holds
len (J . i) <= m ) holds
(Mx2Tran (M,b1,b1)) |^ m = ZeroMap (V1,V1)
proof end;

Lm3: for n being Nat
for K being Field
for L being Element of K
for V1 being finite-dimensional VectSp of K
for b1 being OrdBasis of V1
for J being FinSequence_of_Jordan_block of L,K
for M being Matrix of len b1, len b1,K st M = block_diagonal (J,(0. K)) & len b1 <> 0 holds
( ((Mx2Tran (M,b1,b1)) |^ n) . (b1 /. (Sum (Len (J | (min ((Len J),(len b1))))))) = ((power K) . (L,n)) * (b1 /. (Sum (Len (J | (min ((Len J),(len b1))))))) & Sum (Len (J | (min ((Len J),(len b1))))) in dom b1 )
proof end;

theorem :: MATRIXJ2:26
for K being Field
for L being Element of K
for V1 being finite-dimensional VectSp of K
for b1 being OrdBasis of V1
for J being FinSequence_of_Jordan_block of L,K
for M being Matrix of len b1, len b1,K st M = block_diagonal (J,(0. K)) holds
( Mx2Tran (M,b1,b1) is nilpotent iff ( len b1 = 0 or L = 0. K ) )
proof end;

theorem :: MATRIXJ2:27
for K being Field
for V1 being finite-dimensional VectSp of K
for b1 being OrdBasis of V1
for J being FinSequence_of_Jordan_block of 0. K,K
for M being Matrix of len b1, len b1,K st M = block_diagonal (J,(0. K)) & len b1 > 0 holds
for F being nilpotent Function of V1,V1 st F = Mx2Tran (M,b1,b1) holds
( ex i being Nat st
( i in dom J & len (J . i) = deg F ) & ( for i being Nat st i in dom J holds
len (J . i) <= deg F ) )
proof end;

Lm4: for K being Field
for V1, V2 being VectSp of K
for f being linear-transformation of V1,V2
for W1 being Subspace of V1
for W2 being Subspace of V2
for F being Function of W1,W2 st F = f | W1 holds
F is linear-transformation of W1,W2
proof end;

theorem Th28: :: MATRIXJ2:28
for K being Field
for V1, V2 being finite-dimensional VectSp of K
for b1 being OrdBasis of V1
for b2 being OrdBasis of V2
for L being Element of K st len b1 = len b2 holds
for F being linear-transformation of V1,V2 st ( for i being Nat holds
( not i in dom b1 or F . (b1 /. i) = L * (b2 /. i) or ( i + 1 in dom b1 & F . (b1 /. i) = (L * (b2 /. i)) + (b2 /. (i + 1)) ) ) ) holds
ex J being non-empty FinSequence_of_Jordan_block of L,K st AutMt (F,b1,b2) = block_diagonal (J,(0. K))
proof end;

theorem Th29: :: MATRIXJ2:29
for K being Field
for V1 being finite-dimensional VectSp of K
for F being nilpotent linear-transformation of V1,V1 ex J being non-empty FinSequence_of_Jordan_block of 0. K,K ex b1 being OrdBasis of V1 st AutMt (F,b1,b1) = block_diagonal (J,(0. K))
proof end;

theorem Th30: :: MATRIXJ2:30
for n being Nat
for K being Field
for L being Element of K
for V being VectSp of K
for F being linear-transformation of V,V
for V1 being finite-dimensional Subspace of V
for F1 being linear-transformation of V1,V1 st V1 = ker ((F + ((- L) * (id V))) |^ n) & F | V1 = F1 holds
ex J being non-empty FinSequence_of_Jordan_block of L,K ex b1 being OrdBasis of V1 st AutMt (F1,b1,b1) = block_diagonal (J,(0. K))
proof end;

theorem Th31: :: MATRIXJ2:31
for K being algebraic-closed Field
for V being non trivial finite-dimensional VectSp of K
for F being linear-transformation of V,V ex J being non-empty FinSequence_of_Jordan_block of K ex b1 being OrdBasis of V st
( AutMt (F,b1,b1) = block_diagonal (J,(0. K)) & ( for L being Scalar of K holds
( L is eigenvalue of F iff ex i being Nat st
( i in dom J & J . i = Jordan_block (L,(len (J . i))) ) ) ) )
proof end;

:: WP: Jordan Matrix Decomposition Theorem
theorem :: MATRIXJ2:32
for n being Nat
for K being algebraic-closed Field
for M being Matrix of n,K ex J being non-empty FinSequence_of_Jordan_block of K ex P being Matrix of n,K st
( Sum (Len J) = n & P is invertible & M = (P * (block_diagonal (J,(0. K)))) * (P ~) )
proof end;