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

theorem Th1: :: VECTSP11:1

for m, n being Nat
for K being Field
for A, B being Matrix of K
for nt being Element of n -tuples_on NAT
for mt being Element of m -tuples_on NAT st [:(rng nt),(rng mt):] c= Indices A holds
Segm ((A + B),nt,mt) = (Segm (A,nt,mt)) + (Segm (B,nt,mt))

proof end;

theorem Th2: :: VECTSP11:2

for n being Nat
for K being Field
for P being finite without_zero Subset of NAT st P c= Seg n holds
Segm ((1. (K,n)),P,P) = 1. (K,(card P))

proof end;

theorem Th3: :: VECTSP11:3

for K being Field
for A, B being Matrix of K
for P, Q being finite without_zero Subset of NAT st [:P,Q:] c= Indices A holds
Segm ((A + B),P,Q) = (Segm (A,P,Q)) + (Segm (B,P,Q))

proof end;

theorem Th4: :: VECTSP11:4

for i, j, n being Nat
for K being Field
for A, B being Matrix of n,K st i in Seg n & j in Seg n holds
Delete ((A + B),i,j) = (Delete (A,i,j)) + (Delete (B,i,j))

proof end;

theorem Th5: :: VECTSP11:5

for i, j, n being Nat
for K being Field
for a being Element of K
for A being Matrix of n,K st i in Seg n & j in Seg n holds
Delete ((a * A),i,j) = a * (Delete (A,i,j))

proof end;

theorem Th6: :: VECTSP11:6

for i, n being Nat
for K being Field st i in Seg n holds
Delete ((1. (K,n)),i,i) = 1. (K,(n -' 1))

proof end;

theorem Th7: :: VECTSP11:7

for n being Nat
for K being Field
for A, B being Matrix of n,K ex P being Polynomial of K st
( len P <= n + 1 & ( for x being Element of K holds eval (P,x) = Det (A + (x * B)) ) )

proof end;

:: The Characteristic Polynomials of Square Matrixs

theorem Th8: :: VECTSP11:8

for n being Nat
for K being Field
for A being Matrix of n,K ex P being Polynomial of K st
( len P = n + 1 & ( for x being Element of K holds eval (P,x) = Det (A + (x * (1. (K,n)))) ) )

proof end;

Lm1: 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;

registration

let K be Field;

cluster non empty non trivial right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed finite-dimensional for ModuleStr over K;

existence
ex b₁ being VectSp of K st
( not b₁ is trivial & b₁ is finite-dimensional )

proof end;

end;

definition

let R be non empty doubleLoopStr ;
let V be non empty ModuleStr over R;
let IT be Function of V,V;

attr IT is with_eigenvalues means :: VECTSP11:def 1
ex v being Vector of V ex a being Scalar of R st
( v <> 0. V & IT . v = a * v );

end;

:: deftheorem defines with_eigenvalues VECTSP11:def 1 :
for R being non empty doubleLoopStr
for V being non empty ModuleStr over R
for IT being Function of V,V holds
( IT is with_eigenvalues iff ex v being Vector of V ex a being Scalar of R st
( v <> 0. V & IT . v = a * v ) );

Lm2: for K being Field
for V being non trivial VectSp of K holds
( id V is with_eigenvalues & ex v being Vector of V st
( v <> 0. V & (id V) . v = (1_ K) * v ) )

proof end;

registration

let K be Field;
let V be non trivial VectSp of K;

cluster Relation-like the carrier of V -defined the carrier of V -valued Function-like non empty total quasi_total additive homogeneous with_eigenvalues for Element of bool [: the carrier of V, the carrier of V:];

existence
ex b₁ being linear-transformation of V,V st b₁ is with_eigenvalues

proof end;

end;

definition

let R be non empty doubleLoopStr ;
let V be non empty ModuleStr over R;
let f be Function of V,V;
assume A1: f is with_eigenvalues ;

mode eigenvalue of f -> Element of R means :Def2: :: VECTSP11:def 2
ex v being Vector of V st
( v <> 0. V & f . v = it * v );

existence
ex b₁ being Element of R ex v being Vector of V st
( v <> 0. V & f . v = b₁ * v ) by A1;

end;

:: deftheorem Def2 defines eigenvalue VECTSP11:def 2 :
for R being non empty doubleLoopStr
for V being non empty ModuleStr over R
for f being Function of V,V st f is with_eigenvalues holds
for b₄ being Element of R holds
( b₄ is eigenvalue of f iff ex v being Vector of V st
( v <> 0. V & f . v = b₄ * v ) );

definition

let R be non empty doubleLoopStr ;
let V be non empty ModuleStr over R;
let f be Function of V,V;
let L be Scalar of R;
assume A1: ( f is with_eigenvalues & L is eigenvalue of f ) ;

mode eigenvector of f,L -> Vector of V means :Def3: :: VECTSP11:def 3
f . it = L * it;

existence
ex b₁ being Vector of V st f . b₁ = L * b₁

proof end;

end;

:: deftheorem Def3 defines eigenvector VECTSP11:def 3 :
for R being non empty doubleLoopStr
for V being non empty ModuleStr over R
for f being Function of V,V
for L being Scalar of R st f is with_eigenvalues & L is eigenvalue of f holds
for b₅ being Vector of V holds
( b₅ is eigenvector of f,L iff f . b₅ = L * b₅ );

theorem :: VECTSP11:9

for K being Field
for V being non trivial VectSp of K
for w being Vector of V
for a being Element of K st a <> 0. K holds
for f being with_eigenvalues Function of V,V
for L being eigenvalue of f holds
( a * f is with_eigenvalues & a * L is eigenvalue of a * f & ( w is eigenvector of f,L implies w is eigenvector of a * f,a * L ) & ( w is eigenvector of a * f,a * L implies w is eigenvector of f,L ) )

proof end;

theorem :: VECTSP11:10

for K being Field
for V being non trivial VectSp of K
for f1, f2 being with_eigenvalues Function of V,V
for L1, L2 being Scalar of K st L1 is eigenvalue of f1 & L2 is eigenvalue of f2 & ex v being Vector of V st
( v is eigenvector of f1,L1 & v is eigenvector of f2,L2 & v <> 0. V ) holds
( f1 + f2 is with_eigenvalues & L1 + L2 is eigenvalue of f1 + f2 & ( for w being Vector of V st w is eigenvector of f1,L1 & w is eigenvector of f2,L2 holds
w is eigenvector of f1 + f2,L1 + L2 ) )

proof end;

theorem Th11: :: VECTSP11:11

for K being Field
for V being non trivial VectSp of K holds
( id V is with_eigenvalues & 1_ K is eigenvalue of id V & ( for v being Vector of V holds v is eigenvector of id V, 1_ K ) )

proof end;

theorem :: VECTSP11:12

for K being Field
for V being non trivial VectSp of K
for L being eigenvalue of id V holds L = 1_ K

proof end;

theorem :: VECTSP11:13

for K being Field
for V1 being VectSp of K
for f being linear-transformation of V1,V1 st not ker f is trivial holds
( f is with_eigenvalues & 0. K is eigenvalue of f )

proof end;

theorem Th14: :: VECTSP11:14

for K being Field
for V1 being VectSp of K
for f being linear-transformation of V1,V1
for L being Scalar of K holds
( ( f is with_eigenvalues & L is eigenvalue of f ) iff not ker (f + ((- L) * (id V1))) is trivial )

proof end;

theorem Th15: :: VECTSP11:15

for K being Field
for L being Scalar of K
for V1 being finite-dimensional VectSp of K
for b1, b19 being OrdBasis of V1
for f being linear-transformation of V1,V1 holds
( ( f is with_eigenvalues & L is eigenvalue of f ) iff Det (AutEqMt ((f + ((- L) * (id V1))),b1,b19)) = 0. K )

proof end;

theorem :: VECTSP11:16

for K being algebraic-closed Field
for V1 being non trivial finite-dimensional VectSp of K
for f being linear-transformation of V1,V1 holds f is with_eigenvalues

proof end;

theorem Th17: :: VECTSP11:17

for K being Field
for V1 being VectSp of K
for v1 being Vector of V1
for f being linear-transformation of V1,V1
for L being Scalar of K st f is with_eigenvalues & L is eigenvalue of f holds
( v1 is eigenvector of f,L iff v1 in ker (f + ((- L) * (id V1))) )

proof end;

definition

let S be 1-sorted ;
let F be Function of S,S;
let n be Nat;

func F |^ n -> Function of S,S means :Def4: :: VECTSP11:def 4
for F9 being Element of (GFuncs the carrier of S) st F9 = F holds
it = Product (n |-> F9);

existence
ex b₁ being Function of S,S st
for F9 being Element of (GFuncs the carrier of S) st F9 = F holds
b₁ = Product (n |-> F9)

proof end;

uniqueness
for b₁, b₂ being Function of S,S st ( for F9 being Element of (GFuncs the carrier of S) st F9 = F holds
b₁ = Product (n |-> F9) ) & ( for F9 being Element of (GFuncs the carrier of S) st F9 = F holds
b₂ = Product (n |-> F9) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def4 defines |^ VECTSP11:def 4 :
for S being 1-sorted
for F being Function of S,S
for n being Nat
for b₄ being Function of S,S holds
( b₄ = F |^ n iff for F9 being Element of (GFuncs the carrier of S) st F9 = F holds
b₄ = Product (n |-> F9) );

theorem Th18: :: VECTSP11:18

for S being 1-sorted
for F being Function of S,S holds F |^ 0 = id S

proof end;

theorem Th19: :: VECTSP11:19

for S being 1-sorted
for F being Function of S,S holds F |^ 1 = F

proof end;

theorem Th20: :: VECTSP11:20

for i, j being Nat
for S being 1-sorted
for F being Function of S,S holds F |^ (i + j) = (F |^ j) * (F |^ i)

proof end;

theorem :: VECTSP11:21

for i being Nat
for S being 1-sorted
for F being Function of S,S
for s1, s2 being Element of S
for n, m being Nat st (F |^ m) . s1 = s2 & (F |^ n) . s2 = s2 holds
(F |^ (m + (i * n))) . s1 = s2

proof end;

theorem :: VECTSP11:22

for n being Nat
for K being non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr
for V1 being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr over K
for W being Subspace of V1
for f being Function of V1,V1
for fW being Function of W,W st fW = f | W holds
(f |^ n) | W = fW |^ n

proof end;

registration

let K be Field;
let V1 be VectSp of K;
let f be linear-transformation of V1,V1;
let n be Nat;

cluster f |^ n -> additive homogeneous ;

coherence
( f |^ n is homogeneous & f |^ n is additive )

proof end;

end;

theorem Th23: :: VECTSP11:23

for i, j being Nat
for K being Field
for V1 being VectSp of K
for f being linear-transformation of V1,V1
for v1 being Vector of V1 st (f |^ i) . v1 = 0. V1 holds
(f |^ (i + j)) . v1 = 0. V1

proof end;

definition

let K be Field;
let V1 be VectSp of K;
let f be linear-transformation of V1,V1;

func UnionKers f -> strict Subspace of V1 means :Def5: :: VECTSP11:def 5
the carrier of it = { v where v is Vector of V1 : ex n being Nat st (f |^ n) . v = 0. V1 } ;

existence
ex b₁ being strict Subspace of V1 st the carrier of b₁ = { v where v is Vector of V1 : ex n being Nat st (f |^ n) . v = 0. V1 }

proof end;

uniqueness
for b₁, b₂ being strict Subspace of V1 st the carrier of b₁ = { v where v is Vector of V1 : ex n being Nat st (f |^ n) . v = 0. V1 } & the carrier of b₂ = { v where v is Vector of V1 : ex n being Nat st (f |^ n) . v = 0. V1 } holds
b₁ = b₂ by VECTSP_4:29;

end;

:: deftheorem Def5 defines UnionKers VECTSP11:def 5 :
for K being Field
for V1 being VectSp of K
for f being linear-transformation of V1,V1
for b₄ being strict Subspace of V1 holds
( b₄ = UnionKers f iff the carrier of b₄ = { v where v is Vector of V1 : ex n being Nat st (f |^ n) . v = 0. V1 } );

theorem Th24: :: VECTSP11:24

for K being Field
for V1 being VectSp of K
for f being linear-transformation of V1,V1
for v1 being Vector of V1 holds
( v1 in UnionKers f iff ex n being Nat st (f |^ n) . v1 = 0. V1 )

proof end;

theorem Th25: :: VECTSP11:25

for i being Nat
for K being Field
for V1 being VectSp of K
for f being linear-transformation of V1,V1 holds ker (f |^ i) is Subspace of UnionKers f

proof end;

theorem Th26: :: VECTSP11:26

for i, j being Nat
for K being Field
for V1 being VectSp of K
for f being linear-transformation of V1,V1 holds ker (f |^ i) is Subspace of ker (f |^ (i + j))

proof end;

theorem :: VECTSP11:27

for K being Field
for V being finite-dimensional VectSp of K
for f being linear-transformation of V,V ex n being Nat st UnionKers f = ker (f |^ n)

proof end;

theorem Th28: :: VECTSP11:28

for n being Nat
for K being Field
for V1 being VectSp of K
for f being linear-transformation of V1,V1 holds f | (ker (f |^ n)) is linear-transformation of (ker (f |^ n)),(ker (f |^ n))

proof end;

theorem :: VECTSP11:29

for n being Nat
for K being Field
for V1 being VectSp of K
for f being linear-transformation of V1,V1
for L being Scalar of K holds f | (ker ((f + (L * (id V1))) |^ n)) is linear-transformation of (ker ((f + (L * (id V1))) |^ n)),(ker ((f + (L * (id V1))) |^ n))

proof end;

theorem Th30: :: VECTSP11:30

for K being Field
for V1 being VectSp of K
for f being linear-transformation of V1,V1 holds f | (UnionKers f) is linear-transformation of (UnionKers f),(UnionKers f)

proof end;

theorem Th31: :: VECTSP11:31

for K being Field
for V1 being VectSp of K
for f being linear-transformation of V1,V1
for L being Scalar of K holds f | (UnionKers (f + (L * (id V1)))) is linear-transformation of (UnionKers (f + (L * (id V1)))),(UnionKers (f + (L * (id V1))))

proof end;

theorem Th32: :: VECTSP11:32

for n being Nat
for K being Field
for V1 being VectSp of K
for f being linear-transformation of V1,V1 holds f | (im (f |^ n)) is linear-transformation of (im (f |^ n)),(im (f |^ n))

proof end;

theorem :: VECTSP11:33

for n being Nat
for K being Field
for V1 being VectSp of K
for f being linear-transformation of V1,V1
for L being Scalar of K holds f | (im ((f + (L * (id V1))) |^ n)) is linear-transformation of (im ((f + (L * (id V1))) |^ n)),(im ((f + (L * (id V1))) |^ n))

proof end;

theorem Th34: :: VECTSP11:34

for n being Nat
for K being Field
for V1 being VectSp of K
for f being linear-transformation of V1,V1 st UnionKers f = ker (f |^ n) holds
(ker (f |^ n)) /\ (im (f |^ n)) = (0). V1

proof end;

theorem :: VECTSP11:35

for K being Field
for V being finite-dimensional VectSp of K
for f being linear-transformation of V,V
for n being Nat st UnionKers f = ker (f |^ n) holds
V is_the_direct_sum_of ker (f |^ n), im (f |^ n)

proof end;

theorem Th36: :: VECTSP11:36

for K being Field
for V1 being VectSp of K
for f being linear-transformation of V1,V1
for I being Linear_Compl of UnionKers f holds f | I is one-to-one

proof end;

theorem Th37: :: VECTSP11:37

for K being Field
for V1 being VectSp of K
for f being linear-transformation of V1,V1
for L being Scalar of K
for I being Linear_Compl of UnionKers (f + ((- L) * (id V1)))
for fI being linear-transformation of I,I st fI = f | I holds
for v being Vector of I st fI . v = L * v holds
v = 0. V1

proof end;

Lm3: for K being Field
for V1 being VectSp of K
for f being linear-transformation of V1,V1
for a, b being Scalar of K holds (a * b) * f = a * (b * f)

proof end;

Lm4: for K being Field
for V1 being VectSp of K
for L being Scalar of K
for f, g being Function of V1,V1 holds L * (f * g) = (L * f) * g

proof end;

Lm5: for K being Field
for V1 being VectSp of K
for L being Scalar of K
for f, g being Function of V1,V1 st f is additive & f is homogeneous holds
L * (f * g) = f * (L * g)

proof end;

Lm6: for K being Field
for V1 being VectSp of K
for f1, f2, g being Function of V1,V1 holds (f1 + f2) * g = (f1 * g) + (f2 * g)

proof end;

Lm7: for K being Field
for V1 being VectSp of K
for f1, f2, g being Function of V1,V1 st g is additive & g is homogeneous holds
g * (f1 + f2) = (g * f1) + (g * f2)

proof end;

Lm8: for K being Field
for V1 being VectSp of K
for f1, f2, f3 being Function of V1,V1 holds (f1 + f2) + f3 = f1 + (f2 + f3)

proof end;

Lm9: for n being Nat
for K being Field
for V1 being VectSp of K
for L being Scalar of K holds (L * (id V1)) |^ n = ((power K) . (L,n)) * (id V1)

proof end;

Lm10: for K being Field
for V1 being VectSp of K
for f being linear-transformation of V1,V1
for a, b being Scalar of K holds (a + b) * f = (a * f) + (b * f)

proof end;

theorem Th38: :: VECTSP11:38

for n being Nat
for K being Field
for V1 being VectSp of K
for f being linear-transformation of V1,V1
for L being Scalar of K st n >= 1 holds
ex h being linear-transformation of V1,V1 st
( (f + (L * (id V1))) |^ n = (f * h) + ((L * (id V1)) |^ n) & ( for i being Nat holds (f |^ i) * h = h * (f |^ i) ) )

proof end;

theorem :: VECTSP11:39

for K being Field
for V1 being VectSp of K
for f being linear-transformation of V1,V1
for L1, L2 being Scalar of K st f is with_eigenvalues & L1 <> L2 & L2 is eigenvalue of f holds
for I being Linear_Compl of UnionKers (f + ((- L1) * (id V1)))
for fI being linear-transformation of I,I st fI = f | I holds
( fI is with_eigenvalues & L1 is not eigenvalue of fI & L2 is eigenvalue of fI & UnionKers (f + ((- L2) * (id V1))) is Subspace of I )

proof end;

:: Main Lemmas for Expansion of Matrices of Nilpotent Linear Transformations

theorem :: VECTSP11:40

for K being Field
for V1 being VectSp of K
for U being finite Subset of V1 st U is linearly-independent holds
for u being Vector of V1 st u in U holds
for L being Linear_Combination of U \ {u} holds
( card U = card ((U \ {u}) \/ {(u + (Sum L))}) & (U \ {u}) \/ {(u + (Sum L))} is linearly-independent )

proof end;

theorem Th41: :: VECTSP11:41

for K being Field
for V1, V2 being VectSp of K
for A being Subset of V1
for L being Linear_Combination of V2
for f being linear-transformation of V1,V2 st Carrier L c= f .: A holds
ex M being Linear_Combination of A st f . (Sum M) = Sum L

proof end;

theorem :: VECTSP11:42

for K being Field
for V1, V2 being VectSp of K
for f being linear-transformation of V1,V2
for A being Subset of V1
for B being Subset of V2 st f .: A = B holds
f .: the carrier of (Lin A) = the carrier of (Lin B)

proof end;

theorem Th43: :: VECTSP11:43

for K being Field
for V1, V2 being VectSp of K
for L being Linear_Combination of V1
for F being FinSequence of V1
for f being linear-transformation of V1,V2 st f | ((Carrier L) /\ (rng F)) is one-to-one & rng F c= Carrier L holds
ex Lf being Linear_Combination of V2 st
( Carrier Lf = f .: ((Carrier L) /\ (rng F)) & f * (L (#) F) = Lf (#) (f * F) & ( for v1 being Vector of V1 st v1 in (Carrier L) /\ (rng F) holds
L . v1 = Lf . (f . v1) ) )

proof end;

theorem :: VECTSP11:44

for K being Field
for V1, V2 being VectSp of K
for A, B being Subset of V1
for L being Linear_Combination of V1 st Carrier L c= A \/ B & Sum L = 0. V1 holds
for f being additive homogeneous Function of V1,V2 st f | B is one-to-one & f .: B is linearly-independent Subset of V2 & f .: A c= {(0. V2)} holds
Carrier L c= A

proof end;