:: Divisible $\mathbb Z$-modules
:: by Yuichi Futa and Yasunari Shidama
::
:: Received December 30, 2015
:: Copyright (c) 2015-2016 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies GAUSSINT, NUMBERS, SUBSET_1, RLVECT_1, STRUCT_0, FUNCT_1, RAT_1,
XBOOLE_0, ALGSTR_0, RELAT_1, ARYTM_3, CARD_3, BINOP_2, RLSUB_2, EQREL_1,
PRELAMB, XXREAL_0, TARSKI, CARD_1, SUPINF_2, MSSUBFAM, ARYTM_1, NAT_1,
FUNCT_2, FINSET_1, RLSUB_1, BINOP_1, ZFMISC_1, INT_1, RLVECT_2, ZMODUL01,
ZMODUL03, RLVECT_3, RMOD_2, RANKNULL, UNIALG_1, MSAFREE2, INT_3,
COMPLEX1, VECTSP_1, MESFUNC1, XCMPLX_0, REALSET1, VECTSP10, ZMODUL02,
ZMODUL04, ZMODUL06, ZMODUL07, ZMODUL08;
notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, RELAT_1, FUNCT_1, ORDINAL1,
RELSET_1, PARTFUN1, MCART_1, FUNCT_2, BINOP_1, DOMAIN_1, FINSET_1,
CARD_1, NUMBERS, XCMPLX_0, XXREAL_0, INT_1, RAT_1, BINOP_2, REALSET1,
EQREL_1, STRUCT_0, ALGSTR_0, RLVECT_1, GROUP_1, VECTSP_1, VECTSP_4,
VECTSP_5, VECTSP_6, VECTSP_7, INT_3, MOD_2, ZMODUL01, ZMODUL02, ZMODUL03,
GAUSSINT, ZMODUL04, ZMODUL05, ZMODUL06, ZMODUL07;
constructors BINOP_2, UPROOTS, ZMODUL01, REALSET1, ALGSTR_1, EC_PF_1,
ZMODUL04, ZMODUL06, ZMODUL07;
registrations SUBSET_1, RELSET_1, FUNCT_2, FINSET_1, NUMBERS, XREAL_0,
STRUCT_0, RLVECT_1, MEMBERED, CARD_1, INT_1, XBOOLE_0, ORDINAL1,
XXREAL_0, NAT_1, INT_3, REALSET1, RELAT_1, VECTSP_1, GAUSSINT, VECTSP_7,
EQREL_1, RAT_1, XCMPLX_0, ZMODUL03, ZMODUL04, ZMODUL06, ZMODUL07;
requirements REAL, NUMERALS, BOOLE, SUBSET, ARITHM;
begin :: 1. Divisible Module
definition
let V be Z_Module, v be Vector of V;
attr v is divisible means
:: 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;
registration
let V be Z_Module;
cluster 0.V -> divisible;
end;
registration
let V be Z_Module;
cluster divisible for Vector of V;
end;
theorem :: ZMODUL08:1
for V being Z_Module, v, u being divisible Vector of V holds
v + u is divisible;
theorem :: ZMODUL08:2
for V being Z_Module, v being divisible Vector of V holds
- v is divisible;
theorem :: ZMODUL08:3
for V being Z_Module, v being divisible Vector of V,
i being Element of INT.Ring holds
i * v is divisible;
definition
let V be Z_Module;
attr V is divisible means
:: ZMODUL08:def 2
for v being Vector of V holds v is divisible;
end;
registration
let V be Z_Module;
cluster (0).V -> divisible;
end;
registration
cluster Rat-Module -> divisible;
end;
registration
cluster divisible for Z_Module;
end;
registration
let V be Z_Module;
cluster divisible for Submodule of V;
end;
registration
cluster non finitely-generated for divisible Z_Module;
end;
theorem :: ZMODUL08:4
(Int-mult-left(F_Rat)) | [:INT, INT:] = Int-mult-left(INT.Ring);
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;
theorem :: ZMODUL08:6
for V being divisible Z_Module, W be Submodule of V
holds Z_ModuleQuot(V, W) is divisible;
registration
cluster non trivial for divisible Z_Module;
end;
theorem :: ZMODUL08:7
for V being Z_Module holds
V is divisible iff (Omega).V is divisible;
theorem :: ZMODUL08:8
for V being Z_Module, v being Vector of V st v is non torsion holds
Lin{v} is non divisible;
theorem :: ZMODUL08:9
for V being Z_Module, v being Vector of V st v is torsion & v <> 0.V holds
Lin{v} is non divisible;
registration
let V be non trivial Z_Module, v be non zero Vector of V;
cluster Lin{v} -> non divisible;
end;
registration
let V be non trivial Z_Module;
cluster non divisible for Submodule of V;
end;
theorem :: ZMODUL08:10
for V being non trivial finitely-generated torsion-free Z_Module holds
V is non divisible;
theorem :: ZMODUL08:11
for V being non trivial finitely-generated torsion Z_Module holds
ex i being Element of INT.Ring st i <> 0 & for v being Vector of V
holds i * v = 0.V;
theorem :: ZMODUL08:12
for V being non trivial finitely-generated torsion Z_Module,
i being Element of INT.Ring st i <> 0 & for v being Vector of V
holds i * v = 0.V
holds V is non divisible;
theorem :: ZMODUL08:13
for V being non trivial finitely-generated torsion Z_Module holds
V is non divisible;
registration
cluster non divisible for non trivial finitely-generated torsion Z_Module;
end;
theorem :: ZMODUL08:14
for V being non trivial finitely-generated Z_Module holds V is non divisible;
registration
cluster -> non finitely-generated for non trivial divisible Z_Module;
end;
registration
let V be non trivial non divisible Z_Module;
cluster non divisible for non zero Vector of V;
end;
registration
let V be non trivial finite-rank free Z_Module;
cluster rank V -> non zero;
end;
theorem :: ZMODUL08:15
for V being non trivial free Z_Module, v being non zero Vector of V,
I being Basis of V holds
ex L being Linear_Combination of I, u being Vector of V
st v = Sum(L) & u in I & L.u <> 0;
theorem :: ZMODUL08:16
for V being non trivial free Z_Module, v being non zero Vector of V
holds v is non divisible;
registration
cluster -> non divisible for non trivial free Z_Module;
end;
theorem :: ZMODUL08:17
for V being non trivial free Z_Module, v being non zero Vector of V
holds ex a being Element of INT.Ring
st a in NAT & for b being Element of INT.Ring,
u being Vector of V st b > a holds v <> b*u;
theorem :: ZMODUL08:18
for V being non trivial free Z_Module, v being non zero Vector of V
holds ex a being Element of INT.Ring, u being Vector of V
st a in NAT & a <> 0 & v = a*u &
for b being Element of INT.Ring, w being Vector of V st b > a
holds v <> b*w;
begin :: 2. Divisible module for torsion-free $\mathbb{Z}$-module
definition
let V be torsion-free Z_Module;
func EMbedding(V) -> strict Z_Module means
:: 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):];
end;
theorem :: 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), 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, j being Element of F_Rat,
x being Vector of EMbedding(V), v being Vector of Z_MQ_VectSp(V)
st i = j & x = v holds i*x = j*v;
theorem :: 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, v being Vector of Z_MQ_VectSp(V)
st j in INT & v in EMbedding(V)
holds j*v in EMbedding(V);
theorem :: ZMODUL08:21
for V being torsion-free Z_Module holds
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]) );
theorem :: ZMODUL08:22
for V being torsion-free Z_Module, vv being Vector of EMbedding(V)
holds ex v being Vector of V st (MorphsZQ(V)).v = vv;
definition
let V be torsion-free Z_Module;
func DivisibleMod(V) -> strict Z_Module means
:: 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):];
end;
theorem :: ZMODUL08:23
for V being torsion-free Z_Module holds
for v being Vector of DivisibleMod(V) holds
for a being Element of INT.Ring st a <> 0 holds
ex u being Vector of DivisibleMod(V) st a*u = v;
registration
let V be torsion-free Z_Module;
cluster DivisibleMod(V) -> divisible;
end;
theorem :: ZMODUL08:24
for V being torsion-free Z_Module holds
EMbedding(V) is Submodule of DivisibleMod(V);
registration
let V be finitely-generated torsion-free Z_Module;
cluster EMbedding(V) -> finitely-generated;
end;
registration
let V be non trivial torsion-free Z_Module;
cluster EMbedding(V) -> non trivial;
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};
end;
definition
let V be torsion-free Z_Module, r be Element of F_Rat;
func EMbedding(r,V) -> strict Z_Module means
:: 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)):];
end;
theorem :: ZMODUL08:25
for V being torsion-free Z_Module, 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),
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, j being Element of F_Rat,
x being Vector of EMbedding(r, V), v being Vector of Z_MQ_VectSp(V)
st i = j & x = v holds i*x = j*v;
theorem :: ZMODUL08:26
for V being torsion-free Z_Module,
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,
v being Vector of Z_MQ_VectSp(V)
st j in INT & v in EMbedding(r,V)
holds j*v in EMbedding(r,V);
theorem :: ZMODUL08:27
for V being torsion-free Z_Module, 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;
theorem :: ZMODUL08:28
for V being torsion-free Z_Module, v being Vector of V holds
Class(EQRZM(V), [v, 1]) in EMbedding(V);
theorem :: ZMODUL08:29
for V being torsion-free Z_Module, v being Vector of DivisibleMod(V) holds
ex a being Element of INT.Ring st a <> 0 & a * v in EMbedding(V);
registration
let V be torsion-free Z_Module;
cluster DivisibleMod(V) -> torsion-free;
end;
registration
let V be torsion-free Z_Module;
cluster EMbedding(V) -> torsion-free;
end;
registration
let V be free Z_Module;
cluster EMbedding(V) -> free;
end;
theorem :: 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));
theorem :: ZMODUL08:31
for V being torsion-free Z_Module holds
(for x, y being Vector of DivisibleMod(V),
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), w being Vector of Z_MQ_VectSp(V),
a being Element of INT.Ring, aq being Element of F_Rat
st z = w & a = aq holds
a * z = aq * w) &
(for z being Vector of DivisibleMod(V),
w being Vector of Z_MQ_VectSp(V), aq being Element of F_Rat,
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), v being Vector of Z_MQ_VectSp(V),
r being Element of F_Rat, m, n being Element of INT.Ring,
mi,ni be 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);
theorem :: ZMODUL08:32
for V being torsion-free Z_Module, r being Element of F_Rat holds
EMbedding(r, V) is Submodule of DivisibleMod(V);
registration
let V be finitely-generated torsion-free Z_Module;
let r be Element of F_Rat;
cluster EMbedding(r, V) -> finitely-generated;
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;
end;
registration
let V be torsion-free Z_Module;
let r be Element of F_Rat;
cluster EMbedding(r, V) -> torsion-free;
end;
registration
let V be free Z_Module;
let r be non zero Element of F_Rat;
cluster EMbedding(r, V) -> free;
end;
theorem :: ZMODUL08:33
for V being non trivial free Z_Module,
v being Vector of DivisibleMod(V) holds
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);
theorem :: ZMODUL08:34
for V being finite-rank free Z_Module holds
rank(EMbedding(V)) = rank(V);
theorem :: ZMODUL08:35
for V being finite-rank free Z_Module, r being non zero Element of F_Rat
holds rank(EMbedding(r, V)) = rank(EMbedding(V));
theorem :: ZMODUL08:36
for V being finite-rank free Z_Module, r being non zero Element of F_Rat
holds rank(EMbedding(r, V)) = rank(V);
registration
cluster -> infinite for non trivial torsion-free Z_Module;
end;
theorem :: ZMODUL08:37
for V being Z_Module holds
ex A being Subset of V st (A is linearly-independent &
for v being Vector of V holds ex a being Element of INT.Ring
st a in NAT & a > 0 & a * v in Lin(A));
theorem :: ZMODUL08:38
for V being non trivial torsion-free Z_Module, v being non zero Vector of V,
A being Subset of V, 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, u being Vector of V
st a * v = Sum(L) & u in A & L.u <> 0;
theorem :: ZMODUL08:39
for V being torsion-free Z_Module, i being non zero Integer,
r1, r2 being non zero Element of F_Rat st r2 = r1/i holds
EMbedding(r1, V) is Submodule of EMbedding(r2, V);
theorem :: ZMODUL08:40
for V being finite-rank free Z_Module,
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);