:: Divisible $\mathbb Z$-modules
:: by Yuichi Futa and Yasunari Shidama
::
:: Copyright (c) 2015-2021 Association of Mizar Users

definition
let V be Z_Module;
let v be Vector of V;
attr v is divisible means :defDivisibleVector: :: ZMODUL08:def 1
for a being Element of INT.Ring st a <> 0. INT.Ring holds
ex u being Vector of V st a * u = v;
end;

:: deftheorem defDivisibleVector defines divisible ZMODUL08:def 1 :
for V being Z_Module
for v being Vector of V holds
( v is divisible iff for a being Element of INT.Ring st a <> 0. INT.Ring holds
ex u being Vector of V st a * u = v );

registration
let V be Z_Module;
correctness
coherence
0. V is divisible
;
proof end;
end;

registration
let V be Z_Module;
cluster divisible for Element of the carrier of V;
correctness
existence
ex b1 being Vector of V st b1 is divisible
;
proof end;
end;

theorem :: ZMODUL08:1
for V being Z_Module
for v, u being divisible Vector of V holds v + u is divisible
proof end;

theorem :: ZMODUL08:2
for V being Z_Module
for v being divisible Vector of V holds - v is divisible
proof end;

theorem :: ZMODUL08:3
for V being Z_Module
for v being divisible Vector of V
for i being Element of INT.Ring holds i * v is divisible
proof end;

definition
let V be Z_Module;
attr V is divisible means :defDivisibleModule: :: ZMODUL08:def 2
for v being Vector of V holds v is divisible ;
end;

:: deftheorem defDivisibleModule defines divisible ZMODUL08:def 2 :
for V being Z_Module holds
( V is divisible iff for v being Vector of V holds v is divisible );

registration
let V be Z_Module;
correctness
coherence ;
proof end;
end;

registration
correctness
coherence ;
proof end;
end;

registration
correctness
existence
ex b1 being Z_Module st b1 is divisible
;
proof end;
end;

registration
let V be Z_Module;
correctness
existence
ex b1 being Submodule of V st b1 is divisible
;
proof end;
end;

registration
correctness
existence
not for b1 being divisible Z_Module holds b1 is finitely-generated
;
proof end;
end;

theorem LMLT11: :: ZMODUL08:4
proof end;

LMLT12:
proof end;

theorem :: ZMODUL08:5
ModuleStr(# the carrier of INT.Ring, the addF of INT.Ring, the ZeroF of INT.Ring, #) is Submodule of Rat-Module
proof end;

theorem LMLT2: :: ZMODUL08:6
for V being divisible Z_Module
for W being Submodule of V holds VectQuot (V,W) is divisible
proof end;

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

theorem :: ZMODUL08:7
for V being Z_Module holds
( V is divisible iff (Omega). V is divisible )
proof end;

theorem LmFGND1: :: ZMODUL08:8
for V being Z_Module
for v being Vector of V st not v is torsion holds
not Lin {v} is divisible
proof end;

theorem LmFGND2: :: ZMODUL08:9
for V being Z_Module
for v being Vector of V st v is torsion & v <> 0. V holds
not Lin {v} is divisible
proof end;

registration
let V be non trivial Z_Module;
let v be non zero Vector of V;
cluster Lin {v} -> non divisible ;
correctness
coherence
not Lin {v} is divisible
;
proof end;
end;

registration
let V be non trivial Z_Module;
correctness
existence
not for b1 being Submodule of V holds b1 is divisible
;
proof end;
end;

theorem LmFGND3: :: ZMODUL08:10
for V being non trivial torsion-free finitely-generated Z_Module holds not V is divisible
proof end;

theorem LmTM1: :: ZMODUL08:11
for V being non trivial torsion finitely-generated Z_Module ex i being Element of INT.Ring st
( i <> 0 & ( for v being Vector of V holds i * v = 0. V ) )
proof end;

theorem LmFGND41: :: ZMODUL08:12
for V being non trivial torsion finitely-generated Z_Module
for i being Element of INT.Ring st i <> 0 & ( for v being Vector of V holds i * v = 0. V ) holds
not V is divisible
proof end;

theorem LmFGND4: :: ZMODUL08:13
for V being non trivial torsion finitely-generated Z_Module holds not V is divisible
proof end;

registration
correctness
existence
not for b1 being non trivial torsion finitely-generated Z_Module holds b1 is divisible
;
proof end;
end;

theorem ThFGND: :: ZMODUL08:14
for V being non trivial finitely-generated Z_Module holds not V is divisible
proof end;

registration
correctness
coherence
for b1 being non trivial divisible Z_Module holds not b1 is finitely-generated
;
by ThFGND;
end;

registration
let V be non trivial non divisible Z_Module;
cluster non zero non divisible for Element of the carrier of V;
correctness
existence
not for b1 being non zero Vector of V holds b1 is divisible
;
proof end;
end;

registration
let V be non trivial free finite-rank Z_Module;
cluster rank V -> non zero ;
correctness
coherence
not rank V is zero
;
proof end;
end;

theorem LmND1: :: ZMODUL08:15
for V being non trivial free Z_Module
for v being non zero Vector of V
for I being Basis of V ex L being Linear_Combination of I ex u being Vector of V st
( v = Sum L & u in I & L . u <> 0 )
proof end;

theorem ThND1: :: ZMODUL08:16
for V being non trivial free Z_Module
for v being non zero Vector of V holds not v is divisible
proof end;

registration
correctness
coherence
for b1 being non trivial free Z_Module holds not b1 is divisible
;
proof end;
end;

theorem LmND2: :: ZMODUL08:17
for V being non trivial free Z_Module
for v being non zero Vector of V ex a being Element of INT.Ring st
( a in NAT & ( for b being Element of INT.Ring
for u being Vector of V st b > a holds
v <> b * u ) )
proof end;

theorem :: ZMODUL08:18
for V being non trivial free Z_Module
for v being non zero Vector of V ex a being Element of INT.Ring ex u being Vector of V st
( a in NAT & a <> 0 & v = a * u & ( for b being Element of INT.Ring
for w being Vector of V st b > a holds
v <> b * w ) )
proof end;

definition
let V be torsion-free Z_Module;
func EMbedding V -> strict Z_Module means :defEmbedding: :: ZMODUL08:def 3
( the carrier of it = rng () & the ZeroF of it = zeroCoset V & the addF of it = () || (rng ()) & the lmult of it = () | [:INT,(rng ()):] );
existence
ex b1 being strict Z_Module st
( the carrier of b1 = rng () & the ZeroF of b1 = zeroCoset V & the addF of b1 = () || (rng ()) & the lmult of b1 = () | [:INT,(rng ()):] )
proof end;
uniqueness
for b1, b2 being strict Z_Module st the carrier of b1 = rng () & the ZeroF of b1 = zeroCoset V & the addF of b1 = () || (rng ()) & the lmult of b1 = () | [:INT,(rng ()):] & the carrier of b2 = rng () & the ZeroF of b2 = zeroCoset V & the addF of b2 = () || (rng ()) & the lmult of b2 = () | [:INT,(rng ()):] holds
b1 = b2
;
end;

:: deftheorem defEmbedding defines EMbedding ZMODUL08:def 3 :
for V being torsion-free Z_Module
for b2 being strict Z_Module holds
( b2 = EMbedding V iff ( the carrier of b2 = rng () & the ZeroF of b2 = zeroCoset V & the addF of b2 = () || (rng ()) & the lmult of b2 = () | [:INT,(rng ()):] ) );

theorem SB01: :: ZMODUL08:19
for V being torsion-free Z_Module holds
( ( for x being Vector of () holds x is Vector of () ) & 0. () = 0. () & ( for x, y being Vector of ()
for v, w being Vector of () st x = v & y = w holds
x + y = v + w ) & ( for i being Element of INT.Ring
for j being Element of F_Rat
for x being Vector of ()
for v being Vector of () st i = j & x = v holds
i * x = j * v ) )
proof end;

theorem SB02: :: ZMODUL08:20
for V being torsion-free Z_Module holds
( ( for v, w being Vector of () st v in EMbedding V & w in EMbedding V holds
v + w in EMbedding V ) & ( for j being Element of F_Rat
for v being Vector of () st j in INT & v in EMbedding V holds
j * v in EMbedding V ) )
proof end;

theorem SB03: :: ZMODUL08:21
for V being torsion-free Z_Module ex T being linear-transformation of V,() st
( T is bijective & T = MorphsZQ V & ( for v being Vector of V holds T . v = Class ((),[v,1]) ) )
proof end;

theorem :: ZMODUL08:22
for V being torsion-free Z_Module
for vv being Vector of () ex v being Vector of V st () . v = vv
proof end;

definition
let V be torsion-free Z_Module;
func DivisibleMod V -> strict Z_Module means :defDivisibleMod: :: ZMODUL08:def 4
( the carrier of it = Class () & the ZeroF of it = zeroCoset V & the addF of it = addCoset V & the lmult of it = () | [:INT,(Class ()):] );
existence
ex b1 being strict Z_Module st
( the carrier of b1 = Class () & the ZeroF of b1 = zeroCoset V & the addF of b1 = addCoset V & the lmult of b1 = () | [:INT,(Class ()):] )
proof end;
uniqueness
for b1, b2 being strict Z_Module st the carrier of b1 = Class () & the ZeroF of b1 = zeroCoset V & the addF of b1 = addCoset V & the lmult of b1 = () | [:INT,(Class ()):] & the carrier of b2 = Class () & the ZeroF of b2 = zeroCoset V & the addF of b2 = addCoset V & the lmult of b2 = () | [:INT,(Class ()):] holds
b1 = b2
;
end;

:: deftheorem defDivisibleMod defines DivisibleMod ZMODUL08:def 4 :
for V being torsion-free Z_Module
for b2 being strict Z_Module holds
( b2 = DivisibleMod V iff ( the carrier of b2 = Class () & the ZeroF of b2 = zeroCoset V & the addF of b2 = addCoset V & the lmult of b2 = () | [:INT,(Class ()):] ) );

theorem ThDivisible1: :: ZMODUL08:23
for V being torsion-free Z_Module
for v being Vector of ()
for a being Element of INT.Ring st a <> 0 holds
ex u being Vector of () st a * u = v
proof end;

registration
let V be torsion-free Z_Module;
correctness
coherence ;
proof end;
end;

theorem ThDivisible2: :: ZMODUL08:24
for V being torsion-free Z_Module holds EMbedding V is Submodule of DivisibleMod V
proof end;

registration
let V be torsion-free finitely-generated Z_Module;
correctness
proof end;
end;

registration
let V be non trivial torsion-free Z_Module;
correctness
coherence
not EMbedding V is trivial
;
proof end;
end;

definition
let G be Field;
let V be VectSp of G;
let W be Subset of V;
let a be Element of G;
func a * W -> Subset of V equals :: ZMODUL08:def 5
{ (a * u) where u is Vector of V : u in W } ;
coherence
{ (a * u) where u is Vector of V : u in W } is Subset of V
proof end;
end;

:: deftheorem defines * ZMODUL08:def 5 :
for G being Field
for V being VectSp of G
for W being Subset of V
for a being Element of G holds a * W = { (a * u) where u is Vector of V : u in W } ;

definition
let V be torsion-free Z_Module;
let r be Element of F_Rat;
func EMbedding (r,V) -> strict Z_Module means :defriV: :: ZMODUL08:def 6
( the carrier of it = r * (rng ()) & the ZeroF of it = zeroCoset V & the addF of it = () || (r * (rng ())) & the lmult of it = () | [: the carrier of INT.Ring,(r * (rng ())):] );
existence
ex b1 being strict Z_Module st
( the carrier of b1 = r * (rng ()) & the ZeroF of b1 = zeroCoset V & the addF of b1 = () || (r * (rng ())) & the lmult of b1 = () | [: the carrier of INT.Ring,(r * (rng ())):] )
proof end;
uniqueness
for b1, b2 being strict Z_Module st the carrier of b1 = r * (rng ()) & the ZeroF of b1 = zeroCoset V & the addF of b1 = () || (r * (rng ())) & the lmult of b1 = () | [: the carrier of INT.Ring,(r * (rng ())):] & the carrier of b2 = r * (rng ()) & the ZeroF of b2 = zeroCoset V & the addF of b2 = () || (r * (rng ())) & the lmult of b2 = () | [: the carrier of INT.Ring,(r * (rng ())):] holds
b1 = b2
;
end;

:: deftheorem defriV defines EMbedding ZMODUL08:def 6 :
for V being torsion-free Z_Module
for r being Element of F_Rat
for b3 being strict Z_Module holds
( b3 = EMbedding (r,V) iff ( the carrier of b3 = r * (rng ()) & the ZeroF of b3 = zeroCoset V & the addF of b3 = () || (r * (rng ())) & the lmult of b3 = () | [: the carrier of INT.Ring,(r * (rng ())):] ) );

theorem rSB01: :: ZMODUL08:25
for V being torsion-free Z_Module
for r being Element of F_Rat holds
( ( for x being Vector of (EMbedding (r,V)) holds x is Vector of () ) & 0. (EMbedding (r,V)) = 0. () & ( for x, y being Vector of (EMbedding (r,V))
for v, w being Vector of () st x = v & y = w holds
x + y = v + w ) & ( for i being Element of INT.Ring
for j being Element of F_Rat
for x being Vector of (EMbedding (r,V))
for v being Vector of () st i = j & x = v holds
i * x = j * v ) )
proof end;

theorem :: ZMODUL08:26
for V being torsion-free Z_Module
for r being Element of F_Rat holds
( ( for v, w being Vector of () st v in EMbedding (r,V) & w in EMbedding (r,V) holds
v + w in EMbedding (r,V) ) & ( for j being Element of F_Rat
for v being Vector of () st j in INT & v in EMbedding (r,V) holds
j * v in EMbedding (r,V) ) )
proof end;

theorem rSB03A: :: ZMODUL08:27
for V being torsion-free Z_Module
for r being Element of F_Rat st r <> 0. F_Rat holds
ex T being linear-transformation of (),(EMbedding (r,V)) st
( ( for v being Element of () st v in EMbedding V holds
T . v = r * v ) & T is bijective )
proof end;

theorem ThEM1: :: ZMODUL08:28
for V being torsion-free Z_Module
for v being Vector of V holds Class ((),[v,1]) in EMbedding V
proof end;

theorem ThDM1: :: ZMODUL08:29
for V being torsion-free Z_Module
for v being Vector of () ex a being Element of INT.Ring st
( a <> 0 & a * v in EMbedding V )
proof end;

registration
let V be torsion-free Z_Module;
correctness
proof end;
end;

registration
let V be torsion-free Z_Module;
correctness
coherence ;
proof end;
end;

registration
let V be free Z_Module;
correctness
coherence ;
proof end;
end;

theorem ThDivisibleX1: :: ZMODUL08:30
for V being torsion-free Z_Module holds
( ( for v being Vector of () holds v is Vector of () ) & ( for v being Vector of () holds v is Vector of () ) & 0. () = 0. () )
proof end;

theorem ThDivisibleX2: :: ZMODUL08:31
for V being torsion-free Z_Module holds
( ( for x, y being Vector of ()
for v, u being Vector of () st x = v & y = u holds
x + y = v + u ) & ( for z being Vector of ()
for w being Vector of ()
for a being Element of INT.Ring
for aq being Element of F_Rat st z = w & a = aq holds
a * z = aq * w ) & ( for z being Vector of ()
for w being Vector of ()
for aq being Element of F_Rat
for a being Element of INT.Ring st a <> 0 & aq = a & a * z = aq * w holds
z = w ) & ( for x being Vector of ()
for v being Vector of ()
for r being Element of F_Rat
for m, n being Element of INT.Ring
for mi, ni being Integer st m = mi & n = ni & x = v & r <> 0. F_Rat & n <> 0 & r = mi / ni holds
ex y being Vector of () st
( x = n * y & r * v = m * y ) ) )
proof end;

theorem ThDivisible3: :: ZMODUL08:32
for V being torsion-free Z_Module
for r being Element of F_Rat holds EMbedding (r,V) is Submodule of DivisibleMod V
proof end;

registration
let V be torsion-free finitely-generated Z_Module;
let r be Element of F_Rat;
correctness
coherence
EMbedding (r,V) is finitely-generated
;
proof end;
end;

registration
let V be non trivial torsion-free Z_Module;
let r be non zero Element of F_Rat;
cluster EMbedding (r,V) -> non trivial strict ;
correctness
coherence
not EMbedding (r,V) is trivial
;
proof end;
end;

registration
let V be torsion-free Z_Module;
let r be Element of F_Rat;
correctness
coherence
EMbedding (r,V) is torsion-free
;
by ThDivisible3;
end;

registration
let V be free Z_Module;
let r be non zero Element of F_Rat;
cluster EMbedding (r,V) -> strict free ;
correctness
coherence
EMbedding (r,V) is free
;
proof end;
end;

theorem :: ZMODUL08:33
for V being non trivial free Z_Module
for v being Vector of () ex a being Element of INT.Ring st
( a in NAT & a <> 0 & a * v in EMbedding V & ( for b being Element of INT.Ring st b in NAT & b < a & b <> 0 holds
not b * v in EMbedding V ) )
proof end;

theorem ThRankEM: :: ZMODUL08:34
for V being free finite-rank Z_Module holds rank () = rank V
proof end;

theorem ThRankrEM1: :: ZMODUL08:35
for V being free finite-rank Z_Module
for r being non zero Element of F_Rat holds rank (EMbedding (r,V)) = rank ()
proof end;

theorem :: ZMODUL08:36
for V being free finite-rank Z_Module
for r being non zero Element of F_Rat holds rank (EMbedding (r,V)) = rank V
proof end;

registration
correctness
coherence
for b1 being non trivial torsion-free Z_Module holds b1 is infinite
;
proof end;
end;

theorem :: ZMODUL08:37
for V being Z_Module ex A being Subset of V st
( A is linearly-independent & ( for v being Vector of V ex a being Element of INT.Ring st
( a in NAT & a > 0 & a * v in Lin A ) ) )
proof end;

theorem :: ZMODUL08:38
for V being non trivial torsion-free Z_Module
for v being non zero Vector of V
for A being Subset of V
for a being Element of INT.Ring st a in NAT & A is linearly-independent & a > 0 & a * v in Lin A holds
ex L being Linear_Combination of A ex u being Vector of V st
( a * v = Sum L & u in A & L . u <> 0 )
proof end;

theorem ThDivisible4: :: ZMODUL08:39
for V being torsion-free Z_Module
for i being non zero Integer
for r1, r2 being non zero Element of F_Rat st r2 = r1 / i holds
EMbedding (r1,V) is Submodule of EMbedding (r2,V)
proof end;

theorem :: ZMODUL08:40
for V being free finite-rank Z_Module
for Z being Submodule of DivisibleMod V holds
( Z is finitely-generated iff ex r being non zero Element of F_Rat st Z is Submodule of EMbedding (r,V) )
proof end;