:: Free $\mathbb Z$-module
:: by Yuichi Futa , Hiroyuki Okazaki and Yasunari Shidama
::
:: Received August 6, 2012
:: Copyright (c) 2012-2021 Association of Mizar Users

registration

cluster non empty non trivial left_add-cancelable right_add-cancelable right_complementable V156( INT.Ring ) V157( INT.Ring ) V158( INT.Ring ) V159( INT.Ring ) V163() V164() V165() V259() V260() V261() V262() for ModuleStr over INT.Ring ;

correctness
existence
not for b₁ being Z_Module holds b₁ is trivial ;

proof end;

end;

registration

let V be Z_Module;

cluster finite linearly-independent for Element of bool the carrier of V;

correctness
existence
ex b₁ being finite Subset of V st b₁ is linearly-independent ;

proof end;

end;

theorem Th1: :: ZMODUL03:1

for V being Z_Module
for u being Vector of V ex l being Linear_Combination of V st
( l . u = 1 & ( for v being Vector of V st v <> u holds
l . v = 0 ) )

proof end;

Lm1: for r being Element of INT.Ring
for n being Element of NAT
for i being Integer st i = n holds
i * r = n * r

proof end;

theorem Th2: :: ZMODUL03:2

for G being Z_Module
for i being Element of INT.Ring
for w being Element of INT
for v being Element of G st G = ModuleStr(# the carrier of INT.Ring, the addF of INT.Ring, the ZeroF of INT.Ring,(Int-mult-left INT.Ring) #) & v = w holds
i * v = i * w

proof end;

definition

end;

:: deftheorem ZMODUL03:def 1 :
canceled;

registration

let V be Z_Module;

cluster (0). V -> free ;

coherence
(0). V is free by MOD_3:14;

end;

registration

cluster non empty left_add-cancelable right_add-cancelable right_complementable strict V156( INT.Ring ) V157( INT.Ring ) V158( INT.Ring ) V159( INT.Ring ) V163() V164() V165() free V259() V260() V261() V262() for ModuleStr over INT.Ring ;

existence
ex b₁ being Z_Module st
( b₁ is strict & b₁ is free )

proof end;

end;

registration

let V be Z_Module;

cluster non empty left_add-cancelable right_add-cancelable right_complementable strict V156( INT.Ring ) V157( INT.Ring ) V158( INT.Ring ) V159( INT.Ring ) V163() V164() V165() free V259() V260() V261() V262() for Subspace of V;

existence
ex b₁ being Submodule of V st
( b₁ is strict & b₁ is free )

proof end;

end;

registration

let V be free Z_Module;

cluster base for Element of bool the carrier of V;

existence
ex b₁ being Subset of V st b₁ is base by VECTSP_7:def 4;

end;

definition

let V be free Z_Module;
mode Basis of V is base Subset of V;

end;

:: deftheorem ZMODUL03:def 2 :
canceled;

registration

cluster non empty right_complementable V156( INT.Ring ) V157( INT.Ring ) V158( INT.Ring ) V159( INT.Ring ) V163() V164() V165() free -> free Mult-cancelable for ModuleStr over INT.Ring ;

coherence
for b₁ being free Z_Module holds b₁ is Mult-cancelable

proof end;

end;

registration

cluster non empty non trivial left_add-cancelable right_add-cancelable right_complementable V156( INT.Ring ) V157( INT.Ring ) V158( INT.Ring ) V159( INT.Ring ) V163() V164() V165() free V259() V260() V261() V262() for ModuleStr over INT.Ring ;

correctness
existence
ex b₁ being non trivial Z_Module st b₁ is free ;

proof end;

end;

theorem Th3: :: ZMODUL03:3

for V being Z_Module
for KL1, KL2 being Linear_Combination of V
for X being Subset of V st X is linearly-independent & Carrier KL1 c= X & Carrier KL2 c= X & Sum KL1 = Sum KL2 holds
KL1 = KL2

proof end;

theorem :: ZMODUL03:4

for V being free Z_Module
for A being Subset of V st A is linearly-independent holds
ex B being Subset of V st
( A c= B & B is linearly-independent & ( for v being Vector of V ex a being Element of INT.Ring st a * v in Lin B ) )

proof end;

theorem Th5: :: ZMODUL03:5

for V being Z_Module
for L being Linear_Combination of V
for F, G being FinSequence of V
for P being Permutation of (dom F) st G = F * P holds
Sum (L (#) F) = Sum (L (#) G)

proof end;

theorem Th6: :: ZMODUL03:6

for V being Z_Module
for L being Linear_Combination of V
for F being FinSequence of V st Carrier L misses rng F holds
Sum (L (#) F) = 0. V

proof end;

theorem :: ZMODUL03:7

for V being Z_Module
for F being FinSequence of V st F is one-to-one holds
for L being Linear_Combination of V st Carrier L c= rng F holds
Sum (L (#) F) = Sum L

proof end;

theorem :: ZMODUL03:8

for V being Z_Module
for L being Linear_Combination of V
for F being FinSequence of V ex K being Linear_Combination of V st
( Carrier K = (rng F) /\ (Carrier L) & L (#) F = K (#) F )

proof end;

theorem Th9: :: ZMODUL03:9

for V being Z_Module
for L being Linear_Combination of V
for A being Subset of V
for F being FinSequence of V st rng F c= the carrier of (Lin A) holds
ex K being Linear_Combination of A st Sum (L (#) F) = Sum K

proof end;

theorem Th10: :: ZMODUL03:10

for V being Z_Module
for L being Linear_Combination of V
for A being Subset of V st Carrier L c= the carrier of (Lin A) holds
ex K being Linear_Combination of A st Sum L = Sum K

proof end;

theorem Th11: :: ZMODUL03:11

for V being Z_Module
for W being Submodule of V
for L being Linear_Combination of V st Carrier L c= the carrier of W holds
for K being Linear_Combination of W st K = L | the carrier of W holds
( Carrier L = Carrier K & Sum L = Sum K )

proof end;

theorem Th12: :: ZMODUL03:12

for V being Z_Module
for W being Submodule of V
for K being Linear_Combination of W ex L being Linear_Combination of V st
( Carrier K = Carrier L & Sum K = Sum L )

proof end;

theorem Th13: :: ZMODUL03:13

for V being Z_Module
for W being Submodule of V
for L being Linear_Combination of V st Carrier L c= the carrier of W holds
ex K being Linear_Combination of W st
( Carrier K = Carrier L & Sum K = Sum L )

proof end;

theorem Th14: :: ZMODUL03:14

for V being free Z_Module
for I being Basis of V
for v being Vector of V holds v in Lin I

proof end;

theorem :: ZMODUL03:15

for V being Z_Module
for W being Submodule of V
for A being Subset of W st A is linearly-independent holds
A is linearly-independent Subset of V

proof end;

theorem Th16: :: ZMODUL03:16

for V being Z_Module
for W being Submodule of V
for A being Subset of V st A is linearly-independent & A c= the carrier of W holds
A is linearly-independent Subset of W

proof end;

theorem Th17: :: ZMODUL03:17

for V being Z_Module
for A being Subset of V st A is linearly-independent holds
for v being Vector of V st v in A holds
for B being Subset of V st B = A \ {v} holds
not v in Lin B

proof end;

theorem Th18: :: ZMODUL03:18

for V being free Z_Module
for I being Basis of V
for A being non empty Subset of V st A misses I holds
for B being Subset of V st B = I \/ A holds
B is linearly-dependent

proof end;

theorem :: ZMODUL03:19

for V being Z_Module
for W being Submodule of V
for A being Subset of V st A c= the carrier of W holds
Lin A is Submodule of W

proof end;

theorem Th20: :: ZMODUL03:20

for V being Z_Module
for W being Submodule of V
for A being Subset of V
for B being Subset of W st A = B holds
Lin A = Lin B

proof end;

registration

let V be Z_Module;
let A be linearly-independent Subset of V;

cluster Lin A -> free ;

correctness
coherence
Lin A is free ;

proof end;

end;

registration

let V be free Z_Module;

cluster (Omega). V -> free ;

coherence
( (Omega). V is strict & (Omega). V is free )

proof end;

end;

definition

let IT be free Z_Module;

attr IT is finite-rank means :Def3: :: ZMODUL03:def 3
ex A being finite Subset of IT st A is Basis of IT;

end;

:: deftheorem Def3 defines finite-rank ZMODUL03:def 3 :
for IT being free Z_Module holds
( IT is finite-rank iff ex A being finite Subset of IT st A is Basis of IT );

registration

let V be Z_Module;

cluster (0). V -> finite-rank ;

coherence
(0). V is finite-rank

proof end;

end;

registration

cluster non empty left_add-cancelable right_add-cancelable right_complementable strict V156( INT.Ring ) V157( INT.Ring ) V158( INT.Ring ) V159( INT.Ring ) V163() V164() V165() free V259() V260() V261() V262() Mult-cancelable finite-rank for ModuleStr over INT.Ring ;

existence
ex b₁ being free Z_Module st
( b₁ is strict & b₁ is finite-rank )

proof end;

end;

registration

let V be Z_Module;

cluster non empty left_add-cancelable right_add-cancelable right_complementable strict V156( INT.Ring ) V157( INT.Ring ) V158( INT.Ring ) V159( INT.Ring ) V163() V164() V165() free V259() V260() V261() V262() Mult-cancelable finite-rank for Subspace of V;

existence
ex b₁ being free Submodule of V st
( b₁ is strict & b₁ is finite-rank )

proof end;

end;

registration

let V be Z_Module;
let A be finite linearly-independent Subset of V;

cluster Lin A -> finite-rank ;

coherence
Lin A is finite-rank

proof end;

end;

definition

let V be Z_Module;

attr V is finitely-generated means :: ZMODUL03:def 4
ex A being finite Subset of V st Lin A = ModuleStr(# the carrier of V, the addF of V, the ZeroF of V, the lmult of V #);

end;

:: deftheorem defines finitely-generated ZMODUL03:def 4 :
for V being Z_Module holds
( V is finitely-generated iff ex A being finite Subset of V st Lin A = ModuleStr(# the carrier of V, the addF of V, the ZeroF of V, the lmult of V #) );

registration

let V be Z_Module;

cluster (0). V -> finitely-generated ;

coherence
(0). V is finitely-generated

proof end;

end;

registration

cluster non empty left_add-cancelable right_add-cancelable right_complementable strict V156( INT.Ring ) V157( INT.Ring ) V158( INT.Ring ) V159( INT.Ring ) V163() V164() V165() free V259() V260() V261() V262() finitely-generated for ModuleStr over INT.Ring ;

existence
ex b₁ being Z_Module st
( b₁ is strict & b₁ is finitely-generated & b₁ is free )

proof end;

end;

registration

let V be free finite-rank Z_Module;

cluster base -> finite for Element of bool the carrier of V;

coherence
for b₁ being Basis of V holds b₁ is finite

proof end;

end;

theorem Th21: :: ZMODUL03:21

for p being prime Element of INT.Ring
for V being free Z_Module
for I being Basis of V
for u1, u2 being Vector of V st u1 <> u2 & u1 in I & u2 in I holds
ZMtoMQV (V,p,u1) <> ZMtoMQV (V,p,u2)

proof end;

theorem Th22: :: ZMODUL03:22

for p being prime Element of INT.Ring
for V being Z_Module
for ZQ being VectSp of GF p
for vq being Vector of ZQ st ZQ = Z_MQ_VectSp (V,p) holds
ex v being Vector of V st vq = ZMtoMQV (V,p,v)

proof end;

Lm2: for p being prime Element of INT.Ring
for V being Z_Module
for v, w being Vector of V st (ZMtoMQV (V,p,w)) /\ (ZMtoMQV (V,p,v)) <> {} holds
ZMtoMQV (V,p,w) = ZMtoMQV (V,p,v)

proof end;

theorem Th23: :: ZMODUL03:23

for p being prime Element of INT.Ring
for V being Z_Module
for I being Subset of V
for lq being Linear_Combination of Z_MQ_VectSp (V,p) ex l being Linear_Combination of I st
for v being Vector of V st v in I holds
ex w being Vector of V st
( w in I & w in ZMtoMQV (V,p,v) & l . w = lq . (ZMtoMQV (V,p,v)) )

proof end;

theorem Th24: :: ZMODUL03:24

for p being prime Element of INT.Ring
for V being free Z_Module
for I being Basis of V
for lq being Linear_Combination of Z_MQ_VectSp (V,p) ex l being Linear_Combination of I st
for v being Vector of V st v in I holds
l . v = lq . (ZMtoMQV (V,p,v))

proof end;

theorem Th25: :: ZMODUL03:25

for p being prime Element of INT.Ring
for V being free Z_Module
for I being Basis of V
for X being non empty Subset of (Z_MQ_VectSp (V,p)) st X = { (ZMtoMQV (V,p,u)) where u is Vector of V : u in I } holds
ex F being Function of X, the carrier of V st
( ( for u being Vector of V st u in I holds
F . (ZMtoMQV (V,p,u)) = u ) & F is one-to-one & dom F = X & rng F = I )

proof end;

theorem Th26: :: ZMODUL03:26

for p being prime Element of INT.Ring
for V being free Z_Module
for I being Basis of V holds card { (ZMtoMQV (V,p,u)) where u is Vector of V : u in I } = card I

proof end;

theorem Th27: :: ZMODUL03:27

for p being prime Element of INT.Ring
for V being free Z_Module holds ZMtoMQV (V,p,(0. V)) = 0. (Z_MQ_VectSp (V,p))

proof end;

theorem Th28: :: ZMODUL03:28

for p being prime Element of INT.Ring
for V being free Z_Module
for s, t being Element of V holds (ZMtoMQV (V,p,s)) + (ZMtoMQV (V,p,t)) = ZMtoMQV (V,p,(s + t))

proof end;

theorem Th29: :: ZMODUL03:29

for p being prime Element of INT.Ring
for V being free Z_Module
for s being FinSequence of V
for t being FinSequence of (Z_MQ_VectSp (V,p)) 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 = ZMtoMQV (V,p,si) ) ) holds
Sum t = ZMtoMQV (V,p,(Sum s))

proof end;

theorem Th30: :: ZMODUL03:30

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

proof end;

theorem Th31: :: ZMODUL03:31

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

proof end;

theorem Th32: :: ZMODUL03:32

for p being prime Element of INT.Ring
for V being free Z_Module
for I being Basis of V
for IQ being Subset of (Z_MQ_VectSp (V,p)) st IQ = { (ZMtoMQV (V,p,u)) where u is Vector of V : u in I } holds
IQ is linearly-independent

proof end;

Lm3: for p being Prime
for i being Element of INT holds i mod p is Element of (GF p)

proof end;

Lm4: 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 Th33: :: ZMODUL03:33

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 IQ = { (ZMtoMQV (V,p,u)) where u is Vector of V : u in I } holds
for s being FinSequence of V st ( for i being Element of NAT st i in dom s holds
ex si being Vector of V st
( si = s . i & ZMtoMQV (V,p,si) in Lin IQ ) ) holds
ZMtoMQV (V,p,(Sum s)) in Lin IQ

proof end;

theorem Th34: :: ZMODUL03:34

for p being prime Element of INT.Ring
for V being free Z_Module
for I being Basis 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 Th35: :: ZMODUL03:35

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

proof end;

registration

let p be prime Element of INT.Ring;
let V be free finite-rank Z_Module;

cluster Z_MQ_VectSp (V,p) -> finite-dimensional ;

coherence
Z_MQ_VectSp (V,p) is finite-dimensional

proof end;

end;

theorem Th36: :: ZMODUL03:36

for V being free finite-rank Z_Module
for A, B being Basis of V holds card A = card B

proof end;

definition

let V be free finite-rank Z_Module;

func rank V -> Nat means :Def5: :: ZMODUL03:def 5
for I being Basis of V holds it = card I;

existence
ex b₁ being Nat st
for I being Basis of V holds b₁ = card I

proof end;

uniqueness
for b₁, b₂ being Nat st ( for I being Basis of V holds b₁ = card I ) & ( for I being Basis of V holds b₂ = card I ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def5 defines rank ZMODUL03:def 5 :
for V being free finite-rank Z_Module
for b₂ being Nat holds
( b₂ = rank V iff for I being Basis of V holds b₂ = card I );

theorem :: ZMODUL03:37

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

proof end;