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


begin

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}
proofend;

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 ) &amp; ( i + 1 = j implies it * (i,j) = 1_ K ) &amp; ( i <> j &amp; i + 1 <> j implies it * (i,j) = 0. K ) ) ) );
existence
 ex b1 being Matrix of K st
( len b1 = n &amp; width b1 = n &amp; ( for i, j being Nat st [i,j] in Indices b1 holds
( ( i = j implies b1 * (i,j) = L ) &amp; ( i + 1 = j implies b1 * (i,j) = 1_ K ) &amp; ( i <> j &amp; i + 1 <> j implies b1 * (i,j) = 0. K ) ) ) )
proofend;
uniqueness
 for b1, b2 being Matrix of K st len b1 = n &amp; width b1 = n &amp; ( for i, j being Nat st [i,j] in Indices b1 holds
( ( i = j implies b1 * (i,j) = L ) &amp; ( i + 1 = j implies b1 * (i,j) = 1_ K ) &amp; ( i <> j &amp; i + 1 <> j implies b1 * (i,j) = 0. K ) ) ) &amp; len b2 = n &amp; width b2 = n &amp; ( for i, j being Nat st [i,j] in Indices b2 holds
( ( i = j implies b2 * (i,j) = L ) &amp; ( i + 1 = j implies b2 * (i,j) = 1_ K ) &amp; ( i <> j &amp; i + 1 <> j implies b2 * (i,j) = 0. K ) ) ) holds
b1 = b2
proofend;
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 &amp; width b4 = n &amp; ( for i, j being Nat st [i,j] in Indices b4 holds
( ( i = j implies b4 * (i,j) = L ) &amp; ( i + 1 = j implies b4 * (i,j) = 1_ K ) &amp; ( i <> j &amp; 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
proofend;
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
proofend;

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)
proofend;

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 ) )
proofend;

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

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))
proofend;

theorem Th6: :: MATRIXJ2:6
for n, i 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)) ) &amp; ( i = n implies (Line ((Jordan_block (L,n)),i)) "*" F = L * (F /. i) ) )
proofend;

theorem Th7: :: MATRIXJ2:7
for n, i 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) ) &amp; ( i <> 1 implies (Col ((Jordan_block (L,n)),i)) "*" F = (L * (F /. i)) + (F /. (i - 1)) ) )
proofend;

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 &amp; ( for i, j being Nat st [i,j] in Indices M holds
( ( i > j implies M * (i,j) = 0. K ) &amp; ( i <= j implies M * (i,j) = - ((power K) . ((- (L ")),((j -' i) + 1))) ) ) ) )
proofend;

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

begin

definition
let K be Field;
let G be FinSequence of ( the carrier of K *) * ;
attrG 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 V201() 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
proofend;
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
proofend;
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
proofend;

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)
proofend;
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
proofend;

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
proofend;

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 V201() 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
proofend;
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 V201() 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
proofend;
end;

theorem Th12: :: MATRIXJ2:12
for K being Field
for L, a 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
proofend;

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

definition
let K be Field;
let n be Nat;
let J be FinSequence_of_Jordan_block of K;
:: original:|
redefine funcJ | n ->  FinSequence_of_Jordan_block of K;
coherence
 J | n is FinSequence_of_Jordan_block of K
proofend;
:: original:/^
redefine funcJ /^ n ->  FinSequence_of_Jordan_block of K;
coherence
 J /^ n is FinSequence_of_Jordan_block of K
proofend;
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 funcJ1 ^ J2 ->  FinSequence_of_Jordan_block of L,K;
coherence
 J1 ^ J2 is FinSequence_of_Jordan_block of L,K
proofend;
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 funcJ | n ->  FinSequence_of_Jordan_block of L,K;
coherence
 J | n is FinSequence_of_Jordan_block of L,K
proofend;
:: original:/^
redefine funcJ /^ n ->  FinSequence_of_Jordan_block of L,K;
coherence
 J /^ n is FinSequence_of_Jordan_block of L,K
proofend;
end;

begin

definition
let K be doubleLoopStr ;
let V be non empty VectSpStr over K;
let f be Function of V,V;
attrf 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 VectSpStr 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 VectSpStr over K
for f being Function of V,V holds
( f is nilpotent iff ex n being Nat st f |^ n = ZeroMap (V,V) )
proofend;

registration
let K be doubleLoopStr ;
let V be non empty VectSpStr 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
proofend;
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 &amp; b1 is additive &amp; b1 is homogeneous )
proofend;
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))
proofend;

definition
let K be doubleLoopStr ;
let V be non empty VectSpStr 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) &amp; ( for k being Nat st f |^ k = ZeroMap (V,V) holds
it <= k ) );
existence
 ex b1 being Nat st
( f |^ b1 = ZeroMap (V,V) &amp; ( for k being Nat st f |^ k = ZeroMap (V,V) holds
b1 <= k ) )
proofend;
uniqueness
 for b1, b2 being Nat st f |^ b1 = ZeroMap (V,V) &amp; ( for k being Nat st f |^ k = ZeroMap (V,V) holds
b1 <= k ) &amp; f |^ b2 = ZeroMap (V,V) &amp; ( for k being Nat st f |^ k = ZeroMap (V,V) holds
b2 <= k ) holds
b1 = b2
proofend;
end;

:: deftheorem Def5 defines degree_of_nilpotent MATRIXJ2:def_5_:_
 for K being doubleLoopStr
for V being non empty VectSpStr 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) &amp; ( for k being Nat st f |^ k = ZeroMap (V,V) holds
b4 <= k ) ) );

notation
let K be doubleLoopStr ;
let V be non empty VectSpStr 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 VectSpStr over K
for f being nilpotent Function of V,V holds
( deg f = 0 iff [#] V = {(0. V)} )
proofend;

theorem Th16: :: MATRIXJ2:16
for K being doubleLoopStr
for V being non empty VectSpStr 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
proofend;

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
proofend;

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)) &amp; n <= deg f holds
(deg fI) + n = deg f
proofend;

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 &amp; B2 = Bu1 ^ Bu2 &amp; M = block_diagonal (<*M1,M2*>,(0. K)) &amp; width M1 = len Bu1 &amp; width M2 = len Bu2 holds
( ( i in dom bw1 implies (Mx2Tran (M,b1,B2)) . (b1 /. i) = (Mx2Tran (M1,bw1,Bu1)) . (bw1 /. i) ) &amp; ( i in dom bw2 implies (Mx2Tran (M,b1,B2)) . (b1 /. (i + (len bw1))) = (Mx2Tran (M2,bw2,Bu2)) . (bw2 /. i) ) )
proofend;

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 &amp; 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))))))) &amp; len ((B2 | (Sum (Width (F | m)))) /^ (Sum (Width (F | (m -' 1))))) = width (F . m) )
proofend;

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))
proofend;

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 &amp; i <> len B1 holds
Sum (lmlt ((Line ((Jordan_block (L,(len B1))),i)),B1)) = (L * (B1 /. i)) + (B1 /. (i + 1))
proofend;

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) ) &amp; ( i <> len b1 implies (Mx2Tran (M,b1,B2)) . (b1 /. i) = (L * (B2 /. i)) + (B2 /. (i + 1)) ) )
proofend;

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 &amp; m = min ((Len J),i) holds
( ( i = Sum (Len (J | m)) implies (Mx2Tran (M,b1,B2)) . (b1 /. i) = L * (B2 /. i) ) &amp; ( i <> Sum (Len (J | m)) implies (Mx2Tran (M,b1,B2)) . (b1 /. i) = (L * (B2 /. i)) + (B2 /. (i + 1)) ) )
proofend;

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)
proofend;

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)) &amp; 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))))))) &amp; Sum (Len (J | (min ((Len J),(len b1))))) in dom b1 )
proofend;

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 ) )
proofend;

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)) &amp; 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 &amp; len (J . i) = deg F ) &amp; ( for i being Nat st i in dom J holds
len (J . i) <= deg F ) )
proofend;

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
proofend;

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 &amp; 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))
proofend;

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))
proofend;

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) &amp; 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))
proofend;

begin

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)) &amp; ( for L being Scalar of K holds
( L is eigenvalue of F iff ex i being Nat st
( i in dom J &amp; J . i = Jordan_block (L,(len (J . i))) ) ) ) )
proofend;

:: [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 &amp; P is invertible &amp; M = (P * (block_diagonal (J,(0. K)))) * (P ~) )
proofend;