:: Isomorphism Theorem on Vector Spaces over a Ring
:: by Yuichi Futa and Yasunari Shidama
::
:: Received August 30, 2017
:: Copyright (c) 2017-2021 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies VECTSP_1, TARSKI, XBOOLE_0, SUBSET_1, RELAT_1, FUNCT_1, FUNCT_2,
FUNCSDOM, FINSET_1, CARD_1, CARD_3, ARYTM_3, ARYTM_1, MOD_3, FINSEQ_1,
VALUED_1, SUPINF_2, MSSUBFAM, STRUCT_0, RLSUB_1, RLSUB_2, RLVECT_2,
SETWISEO, ORDINAL4, RLVECT_3, UNIALG_1, RANKNULL, UPROOTS, VECTSP10,
ZMODUL05, QC_LANG1, RLVECT_5, ALGSTR_0, VECTSP12, GROUP_2, PRVECT_1,
PRVECT_2, BINOP_1, NUMBERS, RLVECT_1, ZFMISC_1, NAT_1, FUNCT_6, FINSEQOP,
MESFUNC1, PRVECT_3;
notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, RELAT_1, FUNCT_1, RELSET_1,
FUNCT_2, BINOP_1, FINSET_1, CARD_1, ORDINAL1, CARD_3, XCMPLX_0, NUMBERS,
FINSEQ_1, FINSEQOP, STRUCT_0, SETWISEO, ALGSTR_0, RLVECT_1, VECTSP_1,
MOD_2, RLVECT_2, VECTSP_4, VECTSP_5, VECTSP_6, MATRLIN, VECTSP_7,
VECTSP_9, VECTSP10, PRVECT_1, PRVECT_2, PRVECT_3, RANKNULL, ZMODUL05,
ZMODUL07;
constructors RELSET_1, REALSET1, FINSEQOP, RLVECT_2, VECTSP_9, WELLORD2,
SETWISEO, PRVECT_2, ZMODUL05, ZMODUL07, PRVECT_3;
registrations XBOOLE_0, RELAT_1, FUNCT_1, ORDINAL1, RELSET_1, FINSET_1,
RLVECT_1, CARD_3, FINSEQ_1, PRVECT_1, PRVECT_2, XREAL_0, STRUCT_0,
MATRLIN, RANKNULL, VECTSP_9, VECTSP_1, FUNCT_2, ALGSTR_0, PRVECT_3;
requirements BOOLE, SUBSET, NUMERALS;
begin :: 1. Bijective linear transformation
reserve K,F for Ring;
reserve V,W for VectSp of K;
reserve l for Linear_Combination of V;
reserve T for linear-transformation of V,W;
theorem :: VECTSP12:1
for K being Field,
V,W being finite-dimensional VectSp of K,
A being Subset of V,
B being Basis of V,
T being linear-transformation of V, W,
l being Linear_Combination of B \ A
st A is Basis of ker T & A c= B holds T.(Sum l) = Sum(T@*l);
theorem :: VECTSP12:2
for F being Field, X, Y being VectSp of F,
T being linear-transformation of X, Y,
A being Subset of X st T is bijective holds
A is Basis of X iff T.: A is Basis of Y;
theorem :: VECTSP12:3
for F being Field, X, Y being VectSp of F,
T being linear-transformation of X, Y
st T is bijective holds
X is finite-dimensional iff Y is finite-dimensional;
theorem :: VECTSP12:4
for F being Field, X being finite-dimensional VectSp of F,
Y being VectSp of F,
T being linear-transformation of X, Y
st T is bijective holds
Y is finite-dimensional & dim(X) = dim(Y);
theorem :: VECTSP12:5
for F being Field, X, Y being VectSp of F,
l being Linear_Combination of X,
T being linear-transformation of X, Y
st T is one-to-one holds
T @ l = T @* l;
begin :: 2. Properties of linear combinations on modules over a ring
theorem :: VECTSP12:6
for K being Field,V being VectSp of K, W1, W2 being Subspace of V,
I1 being Basis of W1, I2 being Basis of W2 st V is_the_direct_sum_of W1,W2
holds I1 /\ I2 = {};
theorem :: VECTSP12:7
for K being Field,V being VectSp of K, W1, W2 being Subspace of V,
I1 being Basis of W1, I2 being Basis of W2, I being Subset of V
st V is_the_direct_sum_of W1,W2 & I = I1 \/ I2
holds Lin(I) = the ModuleStr of V;
theorem :: VECTSP12:8
for K being Field,V being VectSp of K, W1, W2 being Subspace of V,
I1 being Basis of W1, I2 being Basis of W2, I being Subset of V
st V is_the_direct_sum_of W1,W2 & I = I1 \/ I2
holds I is linearly-independent;
theorem :: VECTSP12:9
for K being Field,V being VectSp of K,
W1, W2 being Subspace of V,
I1 being Basis of W1,I2 being Basis of W2
st W1 /\ W2 = (0).V holds
I1 \/ I2 is Basis of W1+W2;
begin :: 3. 1st isomorphism theorem
theorem :: VECTSP12:10
for K being Field
for V being finite-dimensional VectSp of K,
W being Subspace of V holds
ex S being Linear_Compl of W,
T being linear-transformation of S, VectQuot(V,W)
st T is bijective &
for v being Vector of V st v in S holds T.v = v+ W;
theorem :: VECTSP12:11
for K being Field
for V being finite-dimensional VectSp of K, W being Subspace of V holds
VectQuot(V,W) is finite-dimensional &
dim VectQuot(V,W) + dim W = dim V;
definition
let K be Ring;
let V,U be VectSp of K;
let W be Subspace of V;
let f be linear-transformation of V,U;
assume
the carrier of W c= the carrier of ker f;
func QFunctional(f,W) -> linear-transformation of VectQuot(V,W),U means
:: VECTSP12:def 1
for A being Vector of VectQuot(V,W), a being Vector of V st A = a+W
holds it.A = f.a;
end;
definition
let K be Ring;
let V,U be VectSp of K;
let f be linear-transformation of V,U;
func CQFunctional(f) -> linear-transformation of VectQuot(V,ker f),U
equals
:: VECTSP12:def 2
QFunctional(f,ker f);
end;
registration let K be Ring;
let V,U be VectSp of K, f be linear-transformation of V,U;
cluster CQFunctional(f) -> one-to-one;
end;
:: 1st isomorphism theorem
theorem :: VECTSP12:12
for K being Ring,
V, U being VectSp of K, f being linear-transformation of V,U holds
ex T being linear-transformation of VectQuot(V,ker f), im f
st T = CQFunctional(f) & T is bijective;
definition
let K be Ring, V, U, W be VectSp of K,
f be linear-transformation of V, U,
g be linear-transformation of U, W;
redefine func g*f -> linear-transformation of V, W;
end;
begin :: 4. The product space of vector spaces
definition
let K be Ring;
mode VectorSpace-Sequence of K -> non empty FinSequence means
:: VECTSP12:def 3
for S be set st S in rng it holds S is VectSp of K;
end;
registration let K be Ring;
cluster -> AbGroup-yielding for VectorSpace-Sequence of K;
end;
definition
let K be Ring;
let G be VectorSpace-Sequence of K;
let j be Element of dom G;
redefine func G.j -> VectSp of K;
end;
definition
let K be Ring,
G be VectorSpace-Sequence of K,
j be Element of dom carr G;
redefine func G.j -> VectSp of K;
end;
definition
let K be Ring,
G be VectorSpace-Sequence of K;
func multop G -> MultOps of the carrier of K,carr G means
:: VECTSP12:def 4
len it = len carr G &
for j being Element of dom carr G holds it.j = the lmult of G.j;
end;
definition
let K be Ring,
G be VectorSpace-Sequence of K;
func product G -> strict non empty ModuleStr over K equals
:: VECTSP12:def 5
ModuleStr (# product carr G, [: addop G :], zeros G, [: multop G :] #);
end;
registration
let K be Ring,
G be VectorSpace-Sequence of K;
cluster product G -> Abelian add-associative right_zeroed
right_complementable vector-distributive scalar-distributive
scalar-associative scalar-unital;
end;
begin :: 5. Cartesian product of vector spaces
reserve K for Ring;
definition
let K be Ring,
G,F be non empty ModuleStr over K;
func prod_MLT(G,F) -> Function of
[:the carrier of K ,
[:the carrier of G,the carrier of F:] :],
[:the carrier of G,the carrier of F:] means
:: VECTSP12:def 6
for r being Element of K, g be Vector of G, f being Vector of F
holds it.(r,[g,f]) = [r*g,r*f];
end;
definition
let K be Ring;
let G,F be non empty ModuleStr over K;
func [:G,F:] -> strict non empty ModuleStr over K equals
:: VECTSP12:def 7
ModuleStr (# [:the carrier of G,the carrier of F:],
prod_ADD(G,F), prod_ZERO(G,F), prod_MLT(G,F) #);
end;
registration
let K be Ring;
let G,F be Abelian non empty ModuleStr over K;
cluster [:G,F:] -> Abelian;
end;
registration
let K be Ring;
let G,F be add-associative non empty ModuleStr over K;
cluster [:G,F:] -> add-associative;
end;
registration
let K be Ring;
let G, F be right_zeroed non empty ModuleStr over K;
cluster [:G,F:] -> right_zeroed;
end;
registration
let K be Ring;
let G,F be right_complementable non empty ModuleStr over K;
cluster [:G,F:] -> right_complementable;
end;
theorem :: VECTSP12:13
for G, F being non empty ModuleStr over K holds
( for x being set holds (x is Vector of [:G,F:]
iff ex x1 being Vector of G, x2 being Vector of F st x=[x1,x2]) )
& ( for x, y being Vector of [:G,F:],
x1, y1 being Vector of G, x2, y2 being Vector of F
st x = [x1,x2] & y = [y1,y2] holds x+y = [x1+y1,x2+y2] )
& 0.[:G,F:] = [0.G,0.F]
& ( for x being Vector of [:G,F:], x1 being Vector of G, x2 be Vector of F,
a being Element of K
st x = [x1,x2] holds a*x = [a*x1,a*x2] );
theorem :: VECTSP12:14
for G,F being add-associative right_zeroed
right_complementable non empty ModuleStr over K,
x being Vector of [:G,F:], x1 being Vector of G, x2 be Vector of F
st x = [x1,x2] holds -x = [-x1,-x2];
registration
let K be Ring;
let G, F be vector-distributive non empty ModuleStr over K;
cluster [:G,F:] -> vector-distributive;
end;
registration
let K be Ring;
let G, F be scalar-distributive non empty ModuleStr over K;
cluster [:G,F:] -> scalar-distributive;
end;
registration
let K be Ring;
let G,F be scalar-associative non empty ModuleStr over K;
cluster [:G,F:] -> scalar-associative;
end;
registration
let K be Ring;
let G, F be scalar-unital non empty ModuleStr over K;
cluster [:G,F:] -> scalar-unital;
end;
definition
let K be Ring;
let G be VectSp of K;
redefine func <* G *> -> VectorSpace-Sequence of K;
end;
definition
let K be Ring;
let G, F be VectSp of K;
redefine func <* G,F *> -> VectorSpace-Sequence of K;
end;
theorem :: VECTSP12:15
for X being VectSp of K holds
ex I being Function of X, product <*X*>
st I is one-to-one onto
& ( for x being Vector of X holds I.x = <*x*> )
& ( for v, w being Vector of X holds I.(v+w) = I.v + I.w )
& ( for v being Vector of X, r being Element of the carrier of K
holds I.(r*v) = r*(I.v) )
& I.(0.X) = 0.product <*X*>;
definition
let K be Ring;
let G, F be VectorSpace-Sequence of K;
redefine func G^F -> VectorSpace-Sequence of K;
end;
theorem :: VECTSP12:16
for X, Y being VectSp of K holds
ex I being Function of [:X,Y:],product <*X,Y*>
st I is one-to-one onto
& ( for x being Vector of X, y be Vector of Y holds I.(x,y) = <*x,y*> )
& ( for v, w being Vector of [:X,Y:] holds I.(v+w)=(I.v) + (I.w) )
& ( for v being Vector of [:X,Y:], r being Element of K
holds I.(r*v) = r*(I.v) )
& I.(0.[:X,Y:]) = 0.product <*X,Y*>;
theorem :: VECTSP12:17
for X, Y being VectorSpace-Sequence of K
holds ex I being Function of [:product X,product Y:],product (X^Y)
st I is one-to-one onto
& ( for x being Vector of product X, y being Vector of product Y
holds ex x1, y1 being FinSequence st x = x1 & y = y1 & I.(x,y) = x1^y1 )
& ( for v, w being Vector of [:product X,product Y:]
holds I.(v+w) = I.v + I.w )
& ( for v being Vector of [:product X,product Y:],
r be Element of the carrier of K
holds I.(r*v) = r*(I.v) )
& I.(0.[:product X,product Y:]) = 0.product (X^Y);
theorem :: VECTSP12:18
for G, F being VectSp of K holds
( for x being set holds
( x is Vector of product <*G,F*>
iff ex x1 being Vector of G, x2 being Vector of F st x=<* x1,x2 *> ) )
& ( for x, y being Vector of product <*G,F*>,
x1, y1 being Vector of G, x2, y2 being Vector of F
st x = <*x1,x2*> & y = <*y1,y2*>
holds x+y = <*x1+y1,x2+y2*> )
& 0.(product <*G,F*>) = <* 0.G,0.F *>
& ( for x being Vector of product <*G,F*>,
x1 being Vector of G, x2 being Vector of F
st x = <* x1,x2 *> holds -x = <* -x1,-x2 *> )
& ( for x being Vector of product <*G,F*>,
x1 being Vector of G, x2 being Vector of F,
a being Element of K
st x = <*x1,x2*> holds a*x = <* a*x1,a*x2 *> );