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

registration
correctness
existence
not for b1 being Z_Module holds b1 is trivial
;
proof end;
end;

registration
let V be Z_Module;
correctness
existence
ex b1 being finite Subset of V st b1 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, #) & 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
existence
ex b1 being Z_Module st
( b1 is strict & b1 is free )
proof end;
end;

registration
let V be Z_Module;
existence
ex b1 being Submodule of V st
( b1 is strict & b1 is free )
proof end;
end;

registration
let V be free Z_Module;
cluster base for Element of bool the carrier of V;
existence
ex b1 being Subset of V st b1 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
coherence
for b1 being free Z_Module holds b1 is Mult-cancelable
proof end;
end;

registration
correctness
existence
ex b1 being non trivial Z_Module st b1 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) /\ () & 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;
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;
coherence
proof end;
end;

registration
existence
ex b1 being free Z_Module st
( b1 is strict & b1 is finite-rank )
proof end;
end;

registration
let V be Z_Module;
existence
ex b1 being free Submodule of V st
( b1 is strict & b1 is finite-rank )
proof end;
end;

registration
let V be Z_Module;
let A be finite linearly-independent Subset of V;
coherence
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;
coherence
proof end;
end;

registration
existence
ex b1 being Z_Module st
( b1 is strict & b1 is finitely-generated & b1 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 b1 being Basis of V holds b1 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;
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 b1 being Nat st
for I being Basis of V holds b1 = card I
proof end;
uniqueness
for b1, b2 being Nat st ( for I being Basis of V holds b1 = card I ) & ( for I being Basis of V holds b2 = card I ) holds
b1 = b2
proof end;
end;

:: deftheorem Def5 defines rank ZMODUL03:def 5 :
for V being free finite-rank Z_Module
for b2 being Nat holds
( b2 = rank V iff for I being Basis of V holds b2 = 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;