ZMODUL04: Submodule of free $\mathbb Z$-module

:: Submodule of free $\mathbb Z$-module
:: by Yuichi Futa , Hiroyuki Okazaki and Yasunari Shidama
::
:: Received December 31, 2013
:: Copyright (c) 2013-2021 Association of Mizar Users

Lem1: for i being Integer holds i in the carrier of INT.Ring
by INT_1:def 2;

theorem :: ZMODUL04:1

for R being Ring
for V being LeftMod of R
for W1, W2 being Subspace of V
for WW1, WW2 being Subspace of W1 + W2 st WW1 = W1 & WW2 = W2 holds
W1 + W2 = WW1 + WW2

proof end;

theorem :: ZMODUL04:2

for R being Ring
for V being LeftMod of R
for W1, W2 being Subspace of V
for WW1, WW2 being Subspace of W1 + W2 st WW1 = W1 & WW2 = W2 holds
W1 /\ W2 = WW1 /\ WW2

proof end;

Lm19: for A, B being set st ( for z being object st z in A holds
ex x, y being object st z = [x,y] ) & ( for z being object st z in B holds
ex x, y being object st z = [x,y] ) & ( for x, y being object holds
( [x,y] in A iff [x,y] in B ) ) holds
A = B

proof end;

registration

let V be Z_Module;

cluster [: the carrier of V,(INT \ {0}):] -> non empty ;

proof end;

end;

definition

let V be Z_Module;
assume AS: V is Mult-cancelable ;

func EQRZM V -> Equivalence_Relation of [: the carrier of V,(INT \ {0}):] means :defEQRZM: :: ZMODUL04:def 1
for S, T being object holds
( [S,T] in it iff ( S in [: the carrier of V,(INT \ {0}):] & T in [: the carrier of V,(INT \ {0}):] & ex z1, z2 being Element of V ex i1, i2 being Element of INT.Ring st
( S = [z1,i1] & T = [z2,i2] & i1 <> 0 & i2 <> 0 & i2 * z1 = i1 * z2 ) ) );

proof end;

proof end;

end;

:: deftheorem defEQRZM defines EQRZM ZMODUL04:def 1 :

theorem LMEQR001: :: ZMODUL04:3

for V being Z_Module
for z1, z2 being Element of V
for i1, i2 being Element of INT.Ring st V is Mult-cancelable holds
( [[z1,i1],[z2,i2]] in EQRZM V iff ( i1 <> 0 & i2 <> 0 & i2 * z1 = i1 * z2 ) )

proof end;

definition

let V be Z_Module;
assume AS: V is Mult-cancelable ;

func addCoset V -> BinOp of (Class (EQRZM V)) means :DefaddCoset: :: ZMODUL04:def 2
for A, B being object st A in Class (EQRZM V) & B in Class (EQRZM V) holds
for z1, z2 being Element of V
for i1, i2 being Element of INT.Ring st i1 <> 0. INT.Ring & i2 <> 0. INT.Ring & A = Class ((EQRZM V),[z1,i1]) & B = Class ((EQRZM V),[z2,i2]) holds
it . (A,B) = Class ((EQRZM V),[((i2 * z1) + (i1 * z2)),(i1 * i2)]);

proof end;

proof end;

end;

:: deftheorem DefaddCoset defines addCoset ZMODUL04:def 2 :

definition

let V be Z_Module;
assume AS: V is Mult-cancelable ;

func zeroCoset V -> Element of Class (EQRZM V) means :defZero: :: ZMODUL04:def 3
for i being Integer st i <> 0 holds
it = Class ((EQRZM V),[(0. V),i]);

proof end;

proof end;

end;

:: deftheorem defZero defines zeroCoset ZMODUL04:def 3 :

definition

let V be Z_Module;
assume AS: V is Mult-cancelable ;

func lmultCoset V -> Function of [: the carrier of F_Rat,(Class (EQRZM V)):],(Class (EQRZM V)) means :DeflmultCoset: :: ZMODUL04:def 4
for q, A being object st q in RAT & A in Class (EQRZM V) holds
for m, n, i being Integer
for mm being Element of INT.Ring
for z being Element of V st m = mm & n <> 0 & q = m / n & i <> 0 & A = Class ((EQRZM V),[z,i]) holds
it . (q,A) = Class ((EQRZM V),[(mm * z),(n * i)]);

proof end;

proof end;

end;

:: deftheorem DeflmultCoset defines lmultCoset ZMODUL04:def 4 :

theorem LMEQR003: :: ZMODUL04:4

for V being Z_Module
for z being Element of V
for i, n being Element of INT.Ring st i <> 0. INT.Ring & n <> 0. INT.Ring & V is Mult-cancelable holds
Class ((EQRZM V),[z,i]) = Class ((EQRZM V),[(n * z),(n * i)])

proof end;

theorem LMEQRZM1: :: ZMODUL04:5

for V being Z_Module
for v being Element of ModuleStr(# (Class (EQRZM V)),(addCoset V),(zeroCoset V),(lmultCoset V) #) st V is Mult-cancelable holds
ex i being Element of INT.Ring ex z being Element of V st
( i <> 0. INT.Ring & v = Class ((EQRZM V),[z,i]) )

proof end;

ThEQRZMV1: for V being Z_Module st V is Mult-cancelable holds
ModuleStr(# (Class (EQRZM V)),(addCoset V),(zeroCoset V),(lmultCoset V) #) is VectSp of F_Rat

proof end;

definition

let V be Z_Module;
assume AS: V is Mult-cancelable ;

func Z_MQ_VectSp V -> VectSp of F_Rat equals :defZMQVSp: :: ZMODUL04:def 5
ModuleStr(# (Class (EQRZM V)),(addCoset V),(zeroCoset V),(lmultCoset V) #);

correctness by ThEQRZMV1, AS;

end;

:: deftheorem defZMQVSp defines Z_MQ_VectSp ZMODUL04:def 5 :

ThEQRZMV2: for V being Z_Module st V is Mult-cancelable holds
ex I being Function of V,(Z_MQ_VectSp V) st
( I is one-to-one & ( for v being Element of V holds I . v = Class ((EQRZM V),[v,1]) ) & ( for v, w being Element of V holds I . (v + w) = (I . v) + (I . w) ) & ( for v being Element of V
for i being Element of INT.Ring
for q being Element of F_Rat st i = q holds
I . (i * v) = q * (I . v) ) & I . (0. V) = 0. (Z_MQ_VectSp V) )

proof end;

definition

let V be Z_Module;
assume AS: V is Mult-cancelable ;

func MorphsZQ V -> Function of V,(Z_MQ_VectSp V) means :defMorph: :: ZMODUL04:def 6
( it is one-to-one & ( for v being Element of V holds it . v = Class ((EQRZM V),[v,1]) ) & ( for v, w being Element of V holds it . (v + w) = (it . v) + (it . w) ) & ( for v being Element of V
for i being Element of INT.Ring
for q being Element of F_Rat st i = q holds
it . (i * v) = q * (it . v) ) & it . (0. V) = 0. (Z_MQ_VectSp V) );

existence by ThEQRZMV2, AS;
uniqueness

proof end;

end;

:: deftheorem defMorph defines MorphsZQ ZMODUL04:def 6 :

theorem XThSum: :: ZMODUL04:6

for V being Z_Module st V is Mult-cancelable holds
for s being FinSequence of V
for t being FinSequence of (Z_MQ_VectSp V) st len s = len t & ( for i being Element of NAT st i in dom s holds
ex si being Vector of V st
( si = s . i & t . i = (MorphsZQ V) . si ) ) holds
Sum t = (MorphsZQ V) . (Sum s)

proof end;

theorem XThSum1: :: ZMODUL04:7

for V being Z_Module
for I being Subset of V
for IQ being Subset of (Z_MQ_VectSp V)
for l being Linear_Combination of I
for lq being Linear_Combination of IQ st V is Mult-cancelable & IQ = (MorphsZQ V) .: I & l = lq * (MorphsZQ V) holds
Sum lq = (MorphsZQ V) . (Sum l)

proof end;

theorem ThEQRZMV3A: :: ZMODUL04:8

for V being Z_Module
for IQ being Subset of (Z_MQ_VectSp V)
for lq being Linear_Combination of IQ ex m being Integer ex a being Element of F_Rat st
( m <> 0 & m = a & rng (a * lq) c= INT )

proof end;

theorem ThEQRZMV3: :: ZMODUL04:9

for V being Z_Module
for I being Subset of V
for IQ being Subset of (Z_MQ_VectSp V)
for lq being Linear_Combination of IQ st V is Mult-cancelable & IQ = (MorphsZQ V) .: I holds
ex m being Element of INT.Ring ex a being Element of F_Rat ex l being Linear_Combination of I st
( m <> 0. INT.Ring & m = a & l = (a * lq) * (MorphsZQ V) & (MorphsZQ V) " (Carrier lq) = Carrier l )

proof end;

theorem ThEQRZMV3B: :: ZMODUL04:10

for V being Z_Module
for I being Subset of V
for IQ being Subset of (Z_MQ_VectSp V)
for lq being Linear_Combination of IQ
for m being Integer
for a being Element of F_Rat
for l being Linear_Combination of I st V is Mult-cancelable & IQ = (MorphsZQ V) .: I & m <> 0 & m = a & l = (a * lq) * (MorphsZQ V) holds
a * (Sum lq) = (MorphsZQ V) . (Sum l)

proof end;

theorem ThEQRZMV3C: :: ZMODUL04:11

for V being Z_Module
for I being Subset of V
for IQ being Subset of (Z_MQ_VectSp V) st V is Mult-cancelable & IQ = (MorphsZQ V) .: I & I is linearly-independent holds
IQ is linearly-independent

proof end;

theorem ThEQRZMV4: :: ZMODUL04:12

for V being Z_Module
for I being Subset of V
for l being Linear_Combination of I
for IQ being Subset of (Z_MQ_VectSp V) st V is Mult-cancelable & IQ = (MorphsZQ V) .: I holds
ex lq being Linear_Combination of IQ st
( l = lq * (MorphsZQ V) & Carrier lq = (MorphsZQ V) .: (Carrier l) )

proof end;

theorem ThQuotAX: :: ZMODUL04:13

for V being free Z_Module
for I being Subset of V
for IQ being Subset of (Z_MQ_VectSp V)
for l being Linear_Combination of I
for i being Element of INT.Ring st i <> 0. INT.Ring & IQ = (MorphsZQ V) .: I holds
Class ((EQRZM V),[(Sum l),i]) in Lin IQ

proof end;

theorem ThEQRZMV3E: :: ZMODUL04:14

for V being free Z_Module
for I being Subset of V
for IQ being Subset of (Z_MQ_VectSp V) st IQ = (MorphsZQ V) .: I holds
card I = card IQ

proof end;

theorem ThEQRZMV3D: :: ZMODUL04:15

for V being free Z_Module
for I being Subset of V
for IQ being Subset of (Z_MQ_VectSp V) st IQ = (MorphsZQ V) .: I & I is Basis of V holds
IQ is Basis of (Z_MQ_VectSp V)

proof end;

registration

let V be free finite-rank Z_Module;

cluster Z_MQ_VectSp V -> finite-dimensional ;

proof end;

end;

theorem :: ZMODUL04:16

for V being free finite-rank Z_Module holds rank V = dim (Z_MQ_VectSp V)

proof end;

theorem XXTh1: :: ZMODUL04:17

for V being free Z_Module
for I, A being finite Subset of V st I is Basis of V & (card I) + 1 = card A holds
A is linearly-dependent

proof end;

theorem XXTh2: :: ZMODUL04:18

for V being free Z_Module
for A, B being Subset of V st A is linearly-dependent & A c= B holds
B is linearly-dependent by VECTSP_7:1;

theorem XXTh3: :: ZMODUL04:19

for V being free Z_Module
for D, A being Subset of V st D is Basis of V & D is finite & card D c< card A holds
A is linearly-dependent

proof end;

theorem :: ZMODUL04:20

for V being free Z_Module
for I, A being Subset of V st I is Basis of V & I is finite & A is linearly-independent holds
card A c= card I by XXTh3, XBOOLE_0:def 8;

theorem :: ZMODUL04:21

for V being Z_Module st (Omega). V is free holds
V is free

proof end;

theorem :: ZMODUL04:22

for R being Ring
for V being LeftMod of R
for W1, W2 being Subspace of V
for W1s, W2s being strict Subspace of V st W1s = (Omega). W1 & W2s = (Omega). W2 holds
W1s + W2s = W1 + W2

proof end;

theorem :: ZMODUL04:23

for R being Ring
for V being LeftMod of R
for W1, W2 being Subspace of V
for W1s, W2s being strict Subspace of V st W1s = (Omega). W1 & W2s = (Omega). W2 holds
W1s /\ W2s = W1 /\ W2

proof end;

theorem Thn0V: :: ZMODUL04:24

for R being Ring
for V being LeftMod of R
for W being strict Subspace of V st W <> (0). V holds
ex v being Vector of V st
( v in W & v <> 0. V )

proof end;

theorem ThCarrier1: :: ZMODUL04:25

for K being Ring
for V being VectSp of K
for A being Subset of V
for l1, l2 being Linear_Combination of A st (Carrier l1) /\ (Carrier l2) = {} holds
Carrier (l1 + l2) = (Carrier l1) \/ (Carrier l2)

proof end;

theorem ThCarrier2: :: ZMODUL04:26

for R being Ring
for V being VectSp of R
for A1, A2 being Subset of V
for l being Linear_Combination of A1 \/ A2 st A1 /\ A2 = {} holds
ex l1 being Linear_Combination of A1 ex l2 being Linear_Combination of A2 st l = l1 + l2

proof end;

theorem FRds1: :: ZMODUL04:27

for V being Z_Module
for W1, W2 being free Subspace of V
for I1 being Basis of W1
for I2 being Basis of W2 st V is_the_direct_sum_of W1,W2 holds
I1 /\ I2 = {}

proof end;

theorem FRds2: :: ZMODUL04:28

for V being Z_Module
for W1, W2 being free Subspace of V
for I1 being Basis of W1
for I2 being Basis of W2
for I being Subset of V st V is_the_direct_sum_of W1,W2 & I = I1 \/ I2 holds
Lin I = ModuleStr(# the carrier of V, the addF of V, the ZeroF of V, the lmult of V #)

proof end;

theorem FRds3: :: ZMODUL04:29

for V being LeftMod of INT.Ring
for W1, W2 being free Subspace of V
for I1 being Basis of W1
for I2 being Basis of W2
for I being Subset of V st V is_the_direct_sum_of W1,W2 & I = I1 \/ I2 holds
I is linearly-independent

proof end;

theorem FRdsX: :: ZMODUL04:30

for V being Z_Module
for W1, W2 being free Subspace of V st V is_the_direct_sum_of W1,W2 holds
V is free

proof end;

theorem ThDirectSum: :: ZMODUL04:31

for V being Z_Module
for W1, W2 being free Subspace of V st W1 /\ W2 = (0). V holds
W1 + W2 is free

proof end;

theorem :: ZMODUL04:32

for V being free Z_Module
for I being Basis of V
for v being Vector of V st v in I holds
( Lin (I \ {v}) is free & Lin {v} is free )

proof end;

theorem FRdsY: :: ZMODUL04:33

for V being free Z_Module
for I being Basis of V
for v being Vector of V st v in I holds
V is_the_direct_sum_of Lin (I \ {v}), Lin {v}

proof end;

FRX: for V being free finite-rank Z_Module
for W being Subspace of V holds W is free

proof end;

registration

let V be free finite-rank Z_Module;

cluster -> free for Subspace of V;

correctness by FRX;

end;

theorem :: ZMODUL04:34

for V being Z_Module
for W being Subspace of V
for W1, W2 being free Subspace of V st W1 /\ W2 = (0). V & ModuleStr(# the carrier of W, the addF of W, the ZeroF of W, the lmult of W #) = W1 + W2 holds
W is free

proof end;

theorem :: ZMODUL04:35

for p being prime Element of INT.Ring
for V being free Z_Module st Z_MQ_VectSp (V,p) is finite-dimensional holds
V is finite-rank

proof end;

theorem :: ZMODUL04:36

for p being prime Element of INT.Ring
for V being Z_Module
for s being Element of V
for a being Element of INT.Ring
for b being Element of (GF p) st b = a mod p holds
b * (ZMtoMQV (V,p,s)) = ZMtoMQV (V,p,(a * s))

proof end;

LMX2: for p being prime Element of INT.Ring
for V being free Z_Module
for i being Element of INT.Ring
for v being Element of V holds ZMtoMQV (V,p,((i mod p) * v)) = ZMtoMQV (V,p,(i * v))

proof end;

theorem ThQuotBasis5A: :: ZMODUL04:37

for p being prime Element of INT.Ring
for V being free Z_Module
for I being Subset of V
for IQ being Subset of (Z_MQ_VectSp (V,p))
for l being Linear_Combination of I st IQ = { (ZMtoMQV (V,p,u)) where u is Vector of V : u in I } holds
ZMtoMQV (V,p,(Sum l)) in Lin IQ

proof end;

theorem ThQuotBasis5: :: ZMODUL04:38

for p being prime Element of INT.Ring
for V being free Z_Module
for I being Subset of V
for IQ being Subset of (Z_MQ_VectSp (V,p)) st Lin I = ModuleStr(# the carrier of V, the addF of V, the ZeroF of V, the lmult of V #) & IQ = { (ZMtoMQV (V,p,u)) where u is Vector of V : u in I } holds
Lin IQ = ModuleStr(# the carrier of (Z_MQ_VectSp (V,p)), the addF of (Z_MQ_VectSp (V,p)), the ZeroF of (Z_MQ_VectSp (V,p)), the lmult of (Z_MQ_VectSp (V,p)) #)

proof end;

theorem FG02: :: ZMODUL04:39

for V being free finitely-generated Z_Module ex A being finite Subset of V st A is Basis of V

proof end;

registration

cluster non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed free finitely-generated -> free finite-rank finitely-generated for ModuleStr over INT.Ring ;

proof end;

end;

registration

cluster non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed free finite-rank -> free finite-rank finitely-generated for ModuleStr over INT.Ring ;

proof end;

end;

theorem RL5Th25: :: ZMODUL04:40

for V being free finite-rank Z_Module
for A being Subset of V st A is linearly-independent holds
A is finite

proof end;

RL5Th28: for V being free finite-rank Z_Module
for W being Subspace of V holds W is finite-rank

proof end;

registration

let V be Z_Module;
let W1, W2 be free finite-rank Subspace of V;

cluster W1 /\ W2 -> free ;

proof end;

end;

registration

let V be Z_Module;
let W1, W2 be free finite-rank Subspace of V;

cluster W1 /\ W2 -> finite-rank ;

proof end;

end;

registration

let V be free finite-rank Z_Module;

cluster -> finite-rank for Subspace of V;

correctness by RL5Th28;

end;