ZMODUL08: Divisible $\mathbb Z$-modules

:: Divisible $\mathbb Z$-modules
:: by Yuichi Futa and Yasunari Shidama
::
:: Received December 30, 2015
:: 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 :

registration

let V be Z_Module;

cluster 0. V -> divisible ;

correctness

proof end;

end;

registration

let V be Z_Module;

cluster divisible for Element of the carrier of V;

correctness

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 :

registration

let V be Z_Module;

cluster (0). V -> divisible ;

correctness

proof end;

end;

registration

cluster Rat-Module -> divisible ;

correctness

proof end;

end;

registration

cluster non empty left_complementable right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed V164() divisible for ModuleStr over INT.Ring ;

correctness

proof end;

end;

registration

let V be Z_Module;

correctness

proof end;

end;

registration

correctness

proof end;

end;

theorem LMLT11: :: ZMODUL08:4

(Int-mult-left F_Rat) | [:INT,INT:] = Int-mult-left INT.Ring

proof end;

LMLT12: addreal || INT = addint

proof end;

theorem :: ZMODUL08:5

ModuleStr(# the carrier of INT.Ring, the addF of INT.Ring, the ZeroF of INT.Ring,(Int-mult-left 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

cluster non empty non trivial left_complementable right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed V164() divisible for ModuleStr over INT.Ring ;

correctness

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

proof end;

end;

registration

let V be non trivial Z_Module;

correctness

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

proof end;

end;

theorem ThFGND: :: ZMODUL08:14

for V being non trivial finitely-generated Z_Module holds not V is divisible

proof end;

registration

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

correctness 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

proof end;

end;

registration

let V be non trivial free finite-rank Z_Module;

cluster rank V -> non zero ;

correctness

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

cluster non empty non trivial right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed free -> non trivial free non divisible for ModuleStr over INT.Ring ;

correctness

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 (MorphsZQ V) & the ZeroF of it = zeroCoset V & the addF of it = (addCoset V) || (rng (MorphsZQ V)) & the lmult of it = (lmultCoset V) | [:INT,(rng (MorphsZQ V)):] );

existence

proof end;

uniqueness ;

end;

:: deftheorem defEmbedding defines EMbedding ZMODUL08:def 3 :

theorem SB01: :: ZMODUL08:19

for V being torsion-free Z_Module holds
( ( for x being Vector of (EMbedding V) holds x is Vector of (Z_MQ_VectSp V) ) & 0. (EMbedding V) = 0. (Z_MQ_VectSp V) & ( for x, y being Vector of (EMbedding V)
for v, w being Vector of (Z_MQ_VectSp V) 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 V)
for v being Vector of (Z_MQ_VectSp V) 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 (Z_MQ_VectSp V) 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 (Z_MQ_VectSp V) 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,(EMbedding V) st
( T is bijective & T = MorphsZQ V & ( for v being Vector of V holds T . v = Class ((EQRZM V),[v,1]) ) )

proof end;

theorem :: ZMODUL08:22

for V being torsion-free Z_Module
for vv being Vector of (EMbedding V) ex v being Vector of V st (MorphsZQ V) . 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 (EQRZM V) & the ZeroF of it = zeroCoset V & the addF of it = addCoset V & the lmult of it = (lmultCoset V) | [:INT,(Class (EQRZM V)):] );

existence

proof end;

uniqueness ;

end;

:: deftheorem defDivisibleMod defines DivisibleMod ZMODUL08:def 4 :

theorem ThDivisible1: :: ZMODUL08:23

for V being torsion-free Z_Module
for v being Vector of (DivisibleMod V)
for a being Element of INT.Ring st a <> 0 holds
ex u being Vector of (DivisibleMod V) st a * u = v

proof end;

registration

let V be torsion-free Z_Module;

cluster DivisibleMod V -> strict divisible ;

correctness

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;

cluster EMbedding V -> strict finitely-generated ;

correctness

proof end;

end;

registration

let V be non trivial torsion-free Z_Module;

cluster EMbedding V -> non trivial strict ;

correctness

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

proof end;

end;

:: deftheorem defines * ZMODUL08:def 5 :

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 (MorphsZQ V)) & the ZeroF of it = zeroCoset V & the addF of it = (addCoset V) || (r * (rng (MorphsZQ V))) & the lmult of it = (lmultCoset V) | [: the carrier of INT.Ring,(r * (rng (MorphsZQ V))):] );

existence

proof end;

uniqueness ;

end;

:: deftheorem defriV defines EMbedding ZMODUL08:def 6 :

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 (Z_MQ_VectSp V) ) & 0. (EMbedding (r,V)) = 0. (Z_MQ_VectSp V) & ( for x, y being Vector of (EMbedding (r,V))
for v, w being Vector of (Z_MQ_VectSp V) 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 (Z_MQ_VectSp V) 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 (Z_MQ_VectSp V) 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 (Z_MQ_VectSp V) 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 V),(EMbedding (r,V)) st
( ( for v being Element of (Z_MQ_VectSp V) 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 ((EQRZM V),[v,1]) in EMbedding V

proof end;

theorem ThDM1: :: ZMODUL08:29

for V being torsion-free Z_Module
for v being Vector of (DivisibleMod V) 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;

cluster DivisibleMod V -> strict torsion-free ;

correctness

proof end;

end;

registration

let V be torsion-free Z_Module;

cluster EMbedding V -> strict torsion-free ;

correctness

proof end;

end;

registration

let V be free Z_Module;

cluster EMbedding V -> strict free ;

correctness

proof end;

end;

theorem ThDivisibleX1: :: ZMODUL08:30

for V being torsion-free Z_Module holds
( ( for v being Vector of (Z_MQ_VectSp V) holds v is Vector of (DivisibleMod V) ) & ( for v being Vector of (DivisibleMod V) holds v is Vector of (Z_MQ_VectSp V) ) & 0. (DivisibleMod V) = 0. (Z_MQ_VectSp V) )

proof end;

theorem ThDivisibleX2: :: ZMODUL08:31

for V being torsion-free Z_Module holds
( ( for x, y being Vector of (DivisibleMod V)
for v, u being Vector of (Z_MQ_VectSp V) st x = v & y = u holds
x + y = v + u ) & ( for z being Vector of (DivisibleMod V)
for w being Vector of (Z_MQ_VectSp V)
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 (DivisibleMod V)
for w being Vector of (Z_MQ_VectSp V)
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 (DivisibleMod V)
for v being Vector of (Z_MQ_VectSp V)
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 (DivisibleMod V) 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;

cluster EMbedding (r,V) -> strict finitely-generated ;

correctness

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

proof end;

end;

registration

let V be torsion-free Z_Module;
let r be Element of F_Rat;

cluster EMbedding (r,V) -> strict torsion-free ;

correctness 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

proof end;

end;

theorem :: ZMODUL08:33

for V being non trivial free Z_Module
for v being Vector of (DivisibleMod V) 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 (EMbedding V) = 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 (EMbedding V)

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

cluster non empty non trivial right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed torsion-free -> non trivial infinite torsion-free for ModuleStr over INT.Ring ;

correctness

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;