:: Divisible $\mathbb Z$-modules
:: by Yuichi Futa and Yasunari Shidama
::
:: Received December 30, 2015
:: Copyright (c) 2015-2026 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,
RANKNULL, GAUSSINT, ZMODUL04, ZMODUL05, ZMODUL06, ZMODUL07, VECTSP10;
constructors BINOP_2, UPROOTS, ZMODUL01, REALSET1, ALGSTR_1, EC_PF_1,
ZMODUL04, ZMODUL06, ZMODUL07, ZMODUL05, RELSET_1, ZMODUL02, VECTSP10;
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, GAUSSINT, VECTSP_7, EQREL_1,
RAT_1, XCMPLX_0, ZMODUL03, ZMODUL04, ZMODUL06, ZMODUL07;
requirements REAL, NUMERALS, BOOLE, SUBSET, ARITHM;
definitions TARSKI, VECTSP_1;
equalities XCMPLX_0, BINOP_1, STRUCT_0, ALGSTR_0, INT_3, VECTSP_1, REALSET1,
GAUSSINT, VECTSP_4, VECTSP_6, ZMODUL07, VECTSP10;
expansions TARSKI, STRUCT_0, ALGSTR_0, VECTSP_1, VECTSP_5, ZMODUL06, MOD_2;
theorems CARD_1, CARD_2, FUNCT_1, FUNCT_2, INT_1, RLVECT_1, TARSKI, ZMODUL01,
BINOP_2, ZFMISC_1, RELAT_1, GAUSSINT, EC_PF_1, ZMODUL03, XBOOLE_0,
XBOOLE_1, XCMPLX_1, ORDINAL1, VECTSP_7, VECTSP_1, ALGSTR_0, INT_2,
ZMODUL02, NAT_D, NUMBERS, EQREL_1, VECTSP_6, RAT_1, ABSVALUE, COMPLEX1,
VECTSP_4, ZMODUL04, ZMODUL05, ZMODUL06, ZMODUL07, VECTSP10;
schemes FUNCT_2, NAT_1, XBOOLE_0;
begin :: 1. Divisible Module
definition
let V be Z_Module, v be Vector of V;
attr v is divisible means
:defDivisibleVector:
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;
correctness
proof
for a being Element of INT.Ring st a <> 0 holds
ex u being Vector of V st a * u = 0.V
proof
let a be Element of INT.Ring such that
a <> 0;
take 0.V;
thus thesis by ZMODUL01:1;
end;
hence thesis;
end;
end;
registration
let V be Z_Module;
cluster divisible for Vector of V;
correctness
proof
take 0.V;
thus thesis;
end;
end;
theorem
for V being Z_Module, v, u being divisible Vector of V holds
v + u is divisible
proof
let V be Z_Module, v, u be divisible Vector of V;
thus for a being Element of INT.Ring st a <> 0.INT.Ring holds
ex w being Vector of V st v + u = a * w
proof
let a be Element of INT.Ring such that
A1: a <> 0.INT.Ring;
consider v1 be Vector of V such that
A2: v = a * v1 by A1,defDivisibleVector;
consider u1 be Vector of V such that
A3: u = a * u1 by A1,defDivisibleVector;
take v1 + u1;
thus v + u = a * (v1 + u1) by A2,A3,VECTSP_1:def 14;
end;
end;
theorem
for V being Z_Module, v being divisible Vector of V holds
- v is divisible
proof
let V be Z_Module, v be divisible Vector of V;
thus for a being Element of INT.Ring st a <> 0.INT.Ring holds
ex w being Vector of V st - v = a * w
proof
let a be Element of INT.Ring such that
A1: a <> 0.INT.Ring;
consider u be Vector of V such that
A2: v = a * u by A1,defDivisibleVector;
take -u;
thus -v = a * (-u) by A2,ZMODUL01:6;
end;
end;
theorem
for V being Z_Module, v being divisible Vector of V,
i being Element of INT.Ring holds
i * v is divisible
proof
let V be Z_Module, v be divisible Vector of V, i be Element of INT.Ring;
thus for a being Element of INT.Ring st a <> 0.INT.Ring holds
ex w being Vector of V st i * v = a * w
proof
let a be Element of INT.Ring such that
A1: a <> 0.INT.Ring;
consider v1 be Vector of V such that
A2: v = a * v1 by A1,defDivisibleVector;
take i * v1;
thus i * v = (i * a) * v1 by A2,VECTSP_1:def 16
.= a * (i * v1) by VECTSP_1:def 16;
end;
end;
definition
let V be Z_Module;
attr V is divisible means
:defDivisibleModule:
for v being Vector of V holds v is divisible;
end;
registration
let V be Z_Module;
cluster (0).V -> divisible;
correctness
proof
thus for x being Vector of (0).V holds x is divisible
proof
let x be Vector of (0).V;
x in (0).V;
then x = 0.V by ZMODUL02:66
.= 0.(0).V by ZMODUL01:26;
hence thesis;
end;
end;
end;
registration
cluster Rat-Module -> divisible;
correctness
proof
set V = Rat-Module;
for v being Vector of V holds v is divisible
proof
let v be Vector of V;
for a being Element of INT.Ring st a <> 0.INT.Ring holds
ex u being Vector of V st a*u = v
proof
let a be Element of INT.Ring;
assume AS: a <> 0.INT.Ring;
reconsider v1 = v as Element of F_Rat;
set u1 = (1/a)*v1;
reconsider u1 as Element of F_Rat by RAT_1:def 2;
reconsider u = u1 as Vector of V;
take u;
thus a*u = a*u1 by ZMODUL07:15
.= v by AS,XCMPLX_1:109;
end;
hence thesis;
end;
hence thesis;
end;
end;
registration
cluster divisible for Z_Module;
correctness
proof
set ZR = Rat-Module;
take ZR;
thus thesis;
end;
end;
registration
let V be Z_Module;
cluster divisible for Submodule of V;
correctness
proof
(0).V is divisible;
hence thesis;
end;
end;
registration
cluster non finitely-generated for divisible Z_Module;
correctness
proof
reconsider ZR = Rat-Module as divisible Z_Module;
take ZR;
thus thesis;
end;
end;
theorem LMLT11:
(Int-mult-left(F_Rat)) | [:INT, INT:] = Int-mult-left(INT.Ring)
proof
set ad = (Int-mult-left(F_Rat)) | [:INT, INT:];
[:INT,INT:] c= [:INT,RAT:] by NUMBERS:14,ZFMISC_1:96;
then A2: [:INT,INT:] c= dom (Int-mult-left(F_Rat)) by FUNCT_2:def 1;
A3: dom (Int-mult-left(INT.Ring)) = [:INT,INT:] by FUNCT_2:def 1;
for z being object st z in dom ad holds ad.z = (Int-mult-left(INT.Ring)).z
proof
let z be object;
assume A4: z in dom ad;
then consider x, y be object such that
A5: x in INT & y in INT & z = [x,y] by ZFMISC_1:def 2;
reconsider x1 = x, y1 = y as Element of INT.Ring by A5;
reconsider y2 = y1 as Element of F_Rat by RAT_1:def 2;
reconsider y3 = y1 as Element of INT.Ring;
thus ad.z = (Int-mult-left(F_Rat)). (x1,y1) by A4,A5,FUNCT_1:49
.= x1*y2 by ZMODUL07:15
.= (Int-mult-left(INT.Ring)). (x1,y3) by ZMODUL06:14
.= (Int-mult-left(INT.Ring)).z by A5;
end;
hence thesis by A2,A3,FUNCT_1:2,RELAT_1:62;
end;
LMLT12:
addreal||INT = addint
proof
set ad = addreal||INT;
[:INT,INT:] c= [:REAL,REAL:] by NUMBERS:15,ZFMISC_1:96;
then A1: [:INT,INT:] c= dom (addreal) by FUNCT_2:def 1;
then A2: dom ad = [:INT,INT:] by RELAT_1:62;
A3: dom (addint) = [:INT,INT:] by FUNCT_2:def 1;
for z being object st z in dom ad holds ad.z = addint.z
proof
let z be object;
assume A4: z in dom ad;
then consider x, y be object such that
A5: x in INT & y in INT & z = [x,y] by A2,ZFMISC_1:def 2;
reconsider x1 = x, y1 = y as Integer by A5;
thus ad.z = addreal.(x1,y1) by A4,A5,A2,FUNCT_1:49
.= x1+y1 by BINOP_2:def 9
.= addint.(x1,y1) by BINOP_2:def 20
.= addint.z by A5;
end;
hence thesis by A1,A3,FUNCT_1:2,RELAT_1:62;
end;
theorem
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
set W = ModuleStr(# the carrier of INT.Ring, the addF of INT.Ring,
the ZeroF of INT.Ring, Int-mult-left(INT.Ring) #);
set V = Rat-Module;
G1: W is Z_Module by ZMODUL01:164;
P2: 0.W = 0.V;
(the addF of V) || the carrier of W
= the addF of W by LMLT12,GAUSSINT:13,NUMBERS:14,RELAT_1:74,ZFMISC_1:96;
hence thesis by G1,P2,LMLT11,NUMBERS:14,VECTSP_4:def 2;
end;
theorem LMLT2:
for V being divisible Z_Module, W be Submodule of V
holds VectQuot(V, W) is divisible
proof
let V be divisible Z_Module, W be Submodule of V;
set VW = VectQuot(V, W);
X0: the carrier of VW = CosetSet(V, W) by VECTSP10:def 6;
for vw being Vector of VW holds vw is divisible
proof
let vw be Vector of VW;
for a being Element of INT.Ring st a <> 0 holds
ex u being Vector of VW st a*u = vw
proof
let a be Element of INT.Ring;
assume AS:a <> 0;
vw in CosetSet(V, W) by X0;
then consider A be Coset of W such that
X1: vw = A;
consider v be Vector of V such that
X2: A = v + W by VECTSP_4:def 6;
v is divisible by defDivisibleModule;
then consider u0 be Vector of V such that
X3: a*u0 = v by AS;
u0 + W is Coset of W by VECTSP_4:def 6;
then u0 + W in CosetSet(V,W);
then reconsider B = u0 + W as Element of CosetSet(V,W);
reconsider u = B as Vector of VectQuot(V, W) by VECTSP10:def 6;
take u;
thus a*u = lmultCoset(V, W).(a,B) by VECTSP10:def 6
.= vw by X1,X2,X3,VECTSP10:def 5;
end;
hence thesis;
end;
hence thesis;
end;
registration
cluster non trivial for divisible Z_Module;
correctness
proof
reconsider ZR = Rat-Module as divisible Z_Module;
take ZR;
reconsider v = 1 as Element of F_Rat;
thus ZR is non trivial;
end;
end;
theorem
for V being Z_Module holds
V is divisible iff (Omega).V is divisible
proof
let V be Z_Module;
hereby
assume A1: V is divisible;
for vv being Vector of (Omega).V holds vv is divisible
proof
let vv be Vector of (Omega).V;
reconsider v = vv as Vector of V;
B1: v is divisible by A1;
for a being Element of INT.Ring st a <> 0 holds
ex uu being Vector of (Omega).V st a*uu = vv
proof
let a be Element of INT.Ring such that
C1: a <> 0;
consider u be Vector of V such that
C2: a*u = v by B1,C1;
reconsider uu = u as Vector of (Omega).V;
take uu;
thus thesis by C2;
end;
hence thesis;
end;
hence (Omega).V is divisible;
end;
assume A1: (Omega).V is divisible;
for v being Vector of V holds v is divisible
proof
let v be Vector of V;
reconsider vv = v as Vector of (Omega).V;
B1: vv is divisible by A1;
for a being Element of INT.Ring st a <> 0 holds
ex u being Vector of V st a*u = v
proof
let a be Element of INT.Ring such that
C1: a <> 0;
consider uu be Vector of (Omega).V such that
C2: a*uu = vv by B1,C1;
reconsider u = uu as Vector of V;
take u;
thus thesis by C2;
end;
hence thesis;
end;
hence V is divisible;
end;
theorem LmFGND1:
for V being Z_Module, v being Vector of V st v is non torsion holds
Lin{v} is non divisible
proof
let V be Z_Module, v be Vector of V such that
A1: v is non torsion;
reconsider i2=2 as Element of INT.Ring by INT_1:def 2;
assume A2: Lin{v} is divisible;
v in Lin{v} by ZMODUL06:20;
then reconsider vv = v as Vector of Lin{v};
vv is divisible by A2;
then consider uu be Vector of Lin{v} such that
A3: i2*uu = vv;
reconsider u = uu as Vector of V by ZMODUL01:25;
u in Lin{v};
then consider i be Element of INT.Ring such that
A4: u = i*v by ZMODUL06:19;
reconsider i3=i as Integer;
v = i2 * (i*v) by A3,A4,ZMODUL01:29
.= (i2*i)*v by VECTSP_1:def 16;
then (i2*i)*v - v = 0.V by RLVECT_1:15;
then (i2*i)*v - 1.INT.Ring *v = 0.V by VECTSP_1:def 17;
then A5: (i2*i - 1.INT.Ring)*v = 0.V by ZMODUL01:9;
2*i3 - 1 <> 0
proof
assume 2*i3 - 1 = 0;
then 1/2 is Integer;
hence contradiction by NAT_D:33;
end;
hence contradiction by A1,A5;
end;
theorem LmFGND2:
for V being Z_Module, v being Vector of V st v is torsion & v <> 0.V holds
Lin{v} is non divisible
proof
let V be Z_Module, v be Vector of V such that
A1: v is torsion & v <> 0.V;
consider i be Element of INT.Ring such that
A2: i <> 0 & i * v = 0.V by A1;
assume A3: Lin{v} is divisible;
v in Lin{v} by ZMODUL06:20;
then reconsider vv = v as Vector of Lin{v};
vv is divisible by A3;
then consider uu be Vector of Lin{v} such that
A4: i * uu = vv by A2;
reconsider u = uu as Vector of V by ZMODUL01:25;
u in Lin{v};
then consider b be Element of INT.Ring such that
A5: u = b * v by ZMODUL06:19;
vv = i * (b * v) by A4,A5,ZMODUL01:29
.= (i*b) * v by VECTSP_1:def 16
.= b * (i*v) by VECTSP_1:def 16
.= 0.V by A2,ZMODUL01:1;
hence contradiction by A1;
end;
registration
let V be non trivial Z_Module, v be non zero Vector of V;
cluster Lin{v} -> non divisible;
correctness
proof
per cases;
suppose v is torsion;
hence thesis by LmFGND2;
end;
suppose v is non torsion;
hence thesis by LmFGND1;
end;
end;
end;
registration
let V be non trivial Z_Module;
cluster non divisible for Submodule of V;
correctness
proof
set v = the non zero Vector of V;
Lin{v} is non divisible;
hence thesis;
end;
end;
theorem LmFGND3:
for V being non trivial finitely-generated torsion-free Z_Module holds
V is non divisible
proof
let V be non trivial finitely-generated torsion-free Z_Module;
consider I be finite Subset of V such that
A1: I is Basis of V by ZMODUL03:def 3;
(Omega).V <> (0).V;
then Lin(I) <> (0).V by A1,VECTSP_7:def 3;
then I <> {}(the carrier of V) by ZMODUL02:67;
then consider v be object such that
A3: v in I by XBOOLE_0:def 1;
reconsider v as Vector of V by A3;
A4: V is Submodule of V & I is linearly-independent &
(Omega).V = Lin(I) by A1,ZMODUL01:32,VECTSP_7:def 3; then
A5: (Omega).V = Lin(I \ {v}) + Lin{v} & Lin(I \ {v}) /\ Lin{v} = (0).V
& Lin(I \ {v}) is free & Lin{v} is free & v <> 0.V
by A3,ZMODUL06:24;
(I \ {v}) \/ {v} = I \/ {v} by XBOOLE_1:39
.= I by A3,XBOOLE_1:12,ZFMISC_1:31;
then B3: Lin(I) = Lin(I \ {v}) + Lin{v} by ZMODUL02:72;
reconsider i2=2 as Element of INT.Ring by INT_1:def 2;
v is non divisible
proof
assume v is divisible;
then consider u be Vector of V such that
C1: i2 * u = v;
u in Lin(I) by A4;
then consider u1, u2 be Vector of V such that
C2: u1 in Lin(I \ {v}) & u2 in Lin{v} & u = u1 + u2
by B3,ZMODUL01:92;
consider iu2 be Element of INT.Ring such that
C3: u2 = iu2 * v by C2,ZMODUL06:19;
C4: u1 <> 0.V
proof
assume u1 = 0.V;
then v = (i2*iu2) * v by C1,C2,C3,VECTSP_1:def 16;
then (i2*iu2)*v - v = 0.V by RLVECT_1:15;
then (i2*iu2)*v - 1.INT.Ring*v = 0.V by VECTSP_1:def 17;
then D1: (i2*iu2 - 1.INT.Ring) * v = 0.V by ZMODUL01:9;
reconsider iiu2=iu2 as Integer;
2*iiu2 - 1 <> 0
proof
assume 2*iiu2 - 1 = 0;
then 1/2 is Integer;
hence contradiction by NAT_D:33;
end;
then v is torsion by D1;
hence contradiction by A5,ZMODUL06:def 3;
end;
v = i2*u1 + i2*u2 by C1,C2,VECTSP_1:def 14
.= i2*u1 + (i2*iu2)*v by C3,VECTSP_1:def 16;
then v - (i2*iu2)*v = i2*u1 + ((i2*iu2)*v - (i2*iu2)*v) by RLVECT_1:28
.= i2*u1 + 0.V by RLVECT_1:15
.= i2*u1;
then 1.INT.Ring *v - (i2*iu2)*v = i2*u1 by VECTSP_1:def 17;
then C5: (1.INT.Ring - i2*iu2)*v = i2*u1 by ZMODUL01:9;
i2 <> 0.INT.Ring; then
C6: i2*u1 <> 0.V by C4,ZMODUL01:def 7;
C7: i2*u1 in Lin(I \ {v}) by C2,ZMODUL01:37;
(1.INT.Ring - i2*iu2)*v in Lin{v} by ZMODUL06:21;
hence contradiction by A5,C5,C6,C7,ZMODUL01:94,ZMODUL02:66;
end;
hence thesis;
end;
theorem LmTM1:
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
proof
let V be non trivial finitely-generated torsion Z_Module;
defpred P[Nat] means
for I being finite Subset of V st card(I) = $1
holds ex i being Element of INT.Ring st i <> 0 &
for v being Vector of V
st v in Lin(I) holds i * v = 0.V;
P1: P[0]
proof
let I be finite Subset of V;
assume card(I) = 0;
then A2: I = {}(the carrier of V);
reconsider i = 1 as Element of INT.Ring;
take i;
thus i <> 0;
thus for v being Vector of V
st v in Lin(I) holds i * v = 0.V
proof
let v be Vector of V;
assume v in Lin(I);
then v in (0).V by A2,ZMODUL02:67;
then v in {0.V} by VECTSP_4:def 3;
then v = 0.V by TARSKI:def 1;
hence i * v = 0.V by ZMODUL01:1;
end;
end;
P2: for n being Nat st P[n] holds P[n+1]
proof
let n be Nat;
assume A0: P[n];
thus P[n+1]
proof
let I be finite Subset of V;
assume A1: card(I) = n+1;
then I <> {};
then consider v be object such that
A3: v in I by XBOOLE_0:def 1;
reconsider v as Vector of V by A3;
(I \ {v}) \/ {v} = I \/ {v} by XBOOLE_1:39
.= I by A3,ZFMISC_1:40; then
A4: Lin(I) = Lin(I \ {v}) + Lin{v} by ZMODUL02:72;
A5: card(I \ {v}) = card(I) - card{v} by A3,CARD_2:44,ZFMISC_1:31
.= card(I) - 1 by CARD_1:30
.= n by A1;
reconsider J = I \ {v} as finite Subset of V;
consider j be Element of INT.Ring such that
B8:j <> 0 &
for v being Vector of V st v in Lin(J) holds j * v = 0.V by A0,A5;
v is torsion by ZMODUL06:def 2;
then consider k be Element of INT.Ring such that
A8: k <> 0 & k * v = 0.V;
reconsider i = j*k as Element of INT.Ring;
take i;
thus i <> 0 by A8,B8;
thus for w being Vector of V st w in Lin(I) holds i * w = 0.V
proof
let w be Vector of V;
assume w in Lin(I);
then consider u1, u2 be Vector of V such that
A10: u1 in Lin(I \ {v}) & u2 in Lin{v} & w = u1 + u2
by A4,ZMODUL01:92;
consider iu2 be Element of INT.Ring such that
A11: u2 = iu2 * v by A10,ZMODUL06:19;
thus i * w = i*u1+i*u2 by A10,VECTSP_1:def 14
.= k*(j*u1) + (j*k)*u2 by VECTSP_1:def 16
.= k*0.V + (j*k)*u2 by B8,A10
.= k*0.V + j*(k*u2) by VECTSP_1:def 16
.= k*0.V + j*(k*iu2 * v) by A11,VECTSP_1:def 16
.= k*0.V + j*(iu2 * (k * v)) by VECTSP_1:def 16
.= 0.V + j*(iu2 * 0.V) by A8,ZMODUL01:1
.= 0.V + j*0.V by ZMODUL01:1
.= 0.V by ZMODUL01:1;
end;
end;
end;
X1: for n being Nat holds P[n] from NAT_1:sch 2(P1,P2);
consider I be finite Subset of V such that
A1: Lin(I) = the ModuleStr of V by ZMODUL03:def 4;
card I is Nat;
then consider i be Element of INT.Ring such that
X2: i <> 0 & for v being Vector of V
st v in Lin(I) holds i * v = 0.V by X1;
take i;
thus i <> 0 by X2;
thus for v being Vector of V holds i * v = 0.V
proof
let v be Vector of V;
v in Lin(I) by A1;
hence i * v = 0.V by X2;
end;
end;
theorem LmFGND41:
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
proof
let V be non trivial finitely-generated torsion Z_Module,
i be Element of INT.Ring such that
A1: i <> 0 & for v being Vector of V holds i * v = 0.V;
assume AS: V is divisible;
set v = the non zero Vector of V;
v is divisible by AS;
then consider u be Vector of V such that
A2: i * u = v by A1;
thus contradiction by A1,A2;
end;
theorem LmFGND4:
for V being non trivial finitely-generated torsion Z_Module holds
V is non divisible
proof
let V be non trivial finitely-generated torsion Z_Module;
consider i be Element of INT.Ring such that
A1: i <> 0 & for v being Vector of V holds i * v = 0.V by LmTM1;
thus thesis by A1,LmFGND41;
end;
registration
cluster non divisible for non trivial finitely-generated torsion Z_Module;
correctness
proof
set V = the non trivial finitely-generated torsion Z_Module;
take V;
thus thesis by LmFGND4;
end;
end;
theorem ThFGND:
for V being non trivial finitely-generated Z_Module holds V is non divisible
proof
let V be non trivial finitely-generated Z_Module;
per cases;
suppose V is torsion;
hence thesis by LmFGND4;
end;
suppose B2: V is non torsion;
assume V is divisible;
then VectQuot(V, torsion_part(V)) is divisible by LMLT2;
hence contradiction by B2,LmFGND3;
end;
end;
registration
cluster -> non finitely-generated for non trivial divisible Z_Module;
correctness by ThFGND;
end;
registration
let V be non trivial non divisible Z_Module;
cluster non divisible for non zero Vector of V;
correctness
proof
thus ex v being non zero Vector of V st v is non divisible
proof
assume AS: for v being non zero Vector of V holds v is divisible;
for v being Vector of V holds v is divisible
proof
let v be Vector of V;
per cases;
suppose v = 0.V;
hence thesis;
end;
suppose v <> 0.V;
then v is non zero;
hence thesis by AS;
end;
end;
hence contradiction by defDivisibleModule;
end;
end;
end;
registration
let V be non trivial finite-rank free Z_Module;
cluster rank V -> non zero;
correctness
proof
assume rank V is zero;
then (Omega).V = (0).V by ZMODUL05:1;
hence contradiction;
end;
end;
theorem LmND1:
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
proof
let V be non trivial free Z_Module, v be non zero Vector of V,
I be Basis of V;
A1: I is linearly-independent & (Omega).V = Lin(I) by VECTSP_7:def 3;
v in Lin(I) by A1;
then consider L be Linear_Combination of I such that
A2: v = Sum(L) by ZMODUL02:64;
Carrier(L) <> {}
proof
assume Carrier(L) = {};
then Sum(L) = 0.V by ZMODUL02:23;
hence contradiction by A2;
end;
then consider uu be object such that
A3: uu in Carrier(L) by XBOOLE_0:def 1;
consider u be Vector of V such that
A4: u = uu & L.u <> 0 by A3;
A5: Carrier(L) c= I by VECTSP_6:def 4;
take L, u;
thus thesis by A2,A3,A4,A5;
end;
theorem ThND1:
for V being non trivial free Z_Module, v being non zero Vector of V
holds v is non divisible
proof
let V be non trivial free Z_Module, v be non zero Vector of V;
reconsider i2=2 as Element of INT.Ring by INT_1:def 2;
set I = the Basis of V;
A1: I is linearly-independent & (Omega).V = Lin(I) by VECTSP_7:def 3;
consider L be Linear_Combination of I, u be Vector of V such that
A2: v = Sum(L) & u in I & L.u <> 0 by LmND1;
assume v is divisible;
then consider w be Vector of V such that
A5: (i2*L.u)*w = v by A2;
w in Lin(I) by A1;
then consider Lw be Linear_Combination of I such that
A6: w = Sum(Lw) by ZMODUL02:64;
reconsider Luw = (i2*L.u)*Lw as Linear_Combination of I by ZMODUL02:31;
A8: Sum(Luw) = Sum(L) by A2,A5,A6,ZMODUL02:53;
Carrier(Luw) c= I & Carrier(L) c= I by VECTSP_6:def 4;
then Luw = L by A8,VECTSP_7:def 3,ZMODUL03:3;
then L.u = (i2*L.u)*Lw.u by VECTSP_6:def 9
.= (i2*Lw.u)*L.u;
then i2*Lw.u = 1 by A2,XCMPLX_1:7;
hence contradiction by INT_1:9;
end;
registration
cluster -> non divisible for non trivial free Z_Module;
correctness
proof
let V be non trivial free Z_Module;
set v = the non zero Vector of V;
v is non divisible by ThND1;
hence thesis;
end;
end;
theorem LmND2:
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
proof
let V be non trivial free Z_Module, v be non zero Vector of V;
set I = the Basis of V;
A1: I is linearly-independent & (Omega).V = Lin(I) by VECTSP_7:def 3;
consider L be Linear_Combination of I, w be Vector of V such that
A2: v = Sum(L) & w in I & L.w <> 0 by LmND1;
reconsider a = |. L.w .| as Element of INT.Ring;
A3: for b being Element of INT.Ring,
u being Vector of V st b > a holds v <> b*u
proof
let b be Element of INT.Ring, u be Vector of V such that
B0: b > a;
assume B1: v = b*u;
u in Lin(I) by A1;
then consider Lu be Linear_Combination of I such that
B2: u = Sum(Lu) by ZMODUL02:64;
reconsider Lnu = b*Lu as Linear_Combination of I by ZMODUL02:31;
B4: Sum(Lnu) = Sum(L) by A2,B1,B2,ZMODUL02:53;
Carrier(Lnu) c= I & Carrier(L) c= I by VECTSP_6:def 4;
then B5: Lnu = L by B4,VECTSP_7:def 3,ZMODUL03:3;
B6: Lnu.w = b*Lu.w by VECTSP_6:def 9;
reconsider ib = b as Integer;
|. L.w .| <> 0 by A2,ABSVALUE:2;
then B8: |. L.w .| > 0 by COMPLEX1:46;
N3: 0 <= b by B0,COMPLEX1:46;
|. L.w .| = |. b .| * |. Lu.w .| by B5,B6,COMPLEX1:65
.= ib * |. Lu.w .| by N3,ABSVALUE:def 1;
hence contradiction by B0,B8,INT_1:def 3,INT_2:27;
end;
take a;
thus thesis by A3,COMPLEX1:46,INT_1:3;
end;
theorem
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
proof
let V be non trivial free Z_Module, v be non zero Vector of V;
defpred P[Nat] means
ex u being Vector of V, k be Element of INT.Ring
st k = $1 & v = k*u;
consider a be Element of INT.Ring such that
A1: a in NAT & for b being Element of INT.Ring,
u being Vector of V st b > a holds v <> b*u by LmND2;
reconsider na = a as Nat by A1;
A2: for k being Nat st P[k] holds k <= na by A1;
A3: ex k being Nat st P[k]
proof
take 1;
v = 1.INT.Ring*v by VECTSP_1:def 17;
hence thesis;
end;
consider a0 be Nat such that
A4: P[a0] & for n being Nat st P[n] holds n <= a0 from NAT_1:sch 6(A2,A3);
reconsider a=a0 as Element of INT.Ring by INT_1:def 2;
consider u be Vector of V such that
A5: v = a*u by A4;
take a, u;
thus a in NAT by ORDINAL1:def 12;
thus a <> 0
proof
assume a = 0;
then v = 0.V by A5,ZMODUL01:1;
hence contradiction;
end;
thus v = a*u by A5;
thus for b being Element of INT.Ring, w being Vector of V
st b > a holds v <> b*w
proof
let b be Element of INT.Ring, w be Vector of V such that
B1: b > a;
b in NAT by B1,INT_1:3;
then reconsider bn = b as Nat;
not P[bn] by A4,B1;
hence thesis;
end;
end;
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
:defEmbedding:
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
set EZV = Z_MQ_VectSp(V);
D1: EZV = ModuleStr(# Class EQRZM(V), addCoset(V), zeroCoset(V),
lmultCoset(V) #) by ZMODUL04:def 5;
AX: EZV is scalar-distributive vector-distributive
scalar-associative scalar-unital add-associative right_zeroed
right_complementable Abelian non empty;
set Cl = rng MorphsZQ(V);
set Add =(addCoset(V)) || Cl;
set Mlt = (lmultCoset(V)) |
[:the carrier of INT.Ring,rng MorphsZQ(V):];
X0: Cl c= the carrier of EZV;
dom addCoset(V) = [:the carrier of EZV,the carrier of EZV:]
by D1,FUNCT_2:def 1;
then
X3: dom Add = [:Cl,Cl:] by RELAT_1:62;
for x being object st x in [:Cl,Cl:]
holds Add.x in Cl
proof
let x be object;
assume X40: x in [:Cl,Cl:];
then consider v, w be object such that
X41: v in Cl & w in Cl & x = [v,w] by ZFMISC_1:def 2;
consider a be object such that
X43: a in the carrier of V & v = (MorphsZQ(V)).a by X41,FUNCT_2:11;
reconsider a as Vector of V by X43;
X44: v = Class(EQRZM(V),[a,1]) by ZMODUL04:def 6,X43;
consider b be object such that
X45: b in the carrier of V & w = (MorphsZQ(V)).b by X41,FUNCT_2:11;
reconsider b as Vector of V by X45;
X46: w = Class(EQRZM(V),[b,1]) by ZMODUL04:def 6,X45;
Add.x = (addCoset(V)).(v,w) by X40,X41,FUNCT_1:49
.= Class(EQRZM(V),[1.INT.Ring*a+1.INT.Ring*b,1.INT.Ring*1.INT.Ring])
by D1,X41,X44,X46,ZMODUL04:def 2
.= Class(EQRZM(V),[a+1.INT.Ring*b,1]) by VECTSP_1:def 17
.= Class(EQRZM(V),[a+b,1]) by VECTSP_1:def 17
.= (MorphsZQ(V)).(a+b) by ZMODUL04:def 6;
hence Add.x in Cl by FUNCT_2:4;
end;
then reconsider Add as BinOp of Cl by X3,FUNCT_2:3;
dom lmultCoset(V) = [:the carrier of F_Rat,the carrier of EZV:]
by FUNCT_2:def 1,D1;
then
Y3: dom Mlt = [:the carrier of INT.Ring,Cl:]
by RELAT_1:62,NUMBERS:14,ZFMISC_1:96;
for x being object st x in [:the carrier of INT.Ring,Cl:]
holds Mlt.x in Cl
proof
let x be object;
assume X40: x in [:the carrier of INT.Ring,Cl:];
then consider i, w be object such that
X41: i in INT & w in Cl & x = [i,w] by ZFMISC_1:def 2;
consider b be object such that
X45: b in the carrier of V & w = (MorphsZQ(V)).b
by X41,FUNCT_2:11;
reconsider b as Vector of V by X45;
reconsider i as Element of INT.Ring by X41;
reconsider j = i as Element of F_Rat by NUMBERS:14;
X47: j = i/1 & 1 <> 0;
X46: w = Class(EQRZM(V),[b,1]) by ZMODUL04:def 6,X45;
Mlt.x = (lmultCoset(V)).(j,w) by X40,X41,FUNCT_1:49
.= Class(EQRZM(V),[i*b,1*1]) by D1,X41,X46,X47,ZMODUL04:def 4
.= (MorphsZQ(V)).(i*b) by ZMODUL04:def 6;
hence Mlt.x in Cl by FUNCT_2:4;
end;
then reconsider Mlt = (lmultCoset(V)) |
[:the carrier of INT.Ring,Cl:]
as Function of [:the carrier of INT.Ring,Cl:], rng MorphsZQ(V)
by Y3,FUNCT_2:3;
X1:(MorphsZQ(V)).(0.V) = 0.EZV by ZMODUL04:def 6
.= zeroCoset(V) by D1;
reconsider z = zeroCoset(V) as Element of Cl by X1,FUNCT_2:4;
set ZS = ModuleStr(#Cl,Add,z,Mlt#);
reconsider ZS as non empty ModuleStr over INT.Ring;
LM2: for x,y being Vector of ZS, v, w being Vector of EZV
st x = v & y = w
holds x+y = v+w
proof
let x, y be Vector of ZS, v, w be Vector of EZV;
assume L0: x = v & y = w;
thus x+y = (addCoset(V)).[x,y] by FUNCT_1:49
.= v+ w by D1,L0;
end;
LM3: for i being Element of INT.Ring, j being Element of F_Rat,
x being Vector of ZS, v being Vector of EZV
st i = j & x = v holds i*x = j*v
proof
let i be Element of INT.Ring,
j be Element of F_Rat,
x be Vector of ZS,
v be Vector of EZV;
assume L0: i = j & x = v;
thus i*x = (lmultCoset(V)).[i,x] by FUNCT_1:49
.= j*v by D1,L0;
end;
ZS is Abelian add-associative right_zeroed
right_complementable scalar-distributive vector-distributive
scalar-associative scalar-unital non empty ModuleStr over INT.Ring
proof
P1: for x being Element of INT.Ring, v, w being Element of ZS holds
x * (v + w) = (x * v) + (x * w)
proof
let x be Element of INT.Ring, v, w be Element of ZS;
reconsider y = x as Element of F_Rat by NUMBERS:14;
reconsider s = v, t = w as Vector of EZV by X0;
P1: v+w = s+t by LM2;
P2: x*v =y*s & x*w =y*t by LM3;
thus x * (v + w) = y*( s + t ) by P1,LM3
.= y*s + y*t by AX
.= x*v + x*w by LM2,P2;
end;
P2: for x, y being Element of INT.Ring,
v being Element of ZS holds
(x + y) * v = (x * v) + (y * v)
proof
let x, y be Element of INT.Ring, v be Element of ZS;
reconsider p = x,q = y as Element of F_Rat by NUMBERS:14;
reconsider p1 = p,q1 = q as Rational;
reconsider s = v as Vector of EZV by X0;
P1: x*v = p*s by LM3;
P2: y*v = q*s by LM3;
thus (x + y) * v = (p+q)*s by LM3
.= p*s + q*s by AX
.= x*v + y*v by P1,P2,LM2;
end;
P3: for x, y being Element of INT.Ring, v being Element of ZS holds
(x * y) * v = x * (y * v)
proof
let x, y be Element of INT.Ring,v be Element of ZS;
reconsider p = x,q = y as Element of F_Rat by NUMBERS:14;
reconsider p1 = p,q1 = q as Rational;
reconsider s = v as Vector of EZV by X0;
P1: y*v = q*s by LM3;
thus (x * y) * v = (p*q)*s by LM3
.= p*(q*s) by AX
.= x*(y*v) by P1,LM3;
end;
P4: for v being Element of ZS holds 1.INT.Ring * v = v
proof
let v be Element of ZS;
reconsider s = v as Vector of EZV by X0;
thus 1.INT.Ring * v = 1.F_Rat *s by LM3
.= v by AX;
end;
P5: for v being Element of ZS holds v is right_complementable
proof
let v be Element of ZS;
reconsider s = v as Vector of EZV by X0;
reconsider i1 = 1.F_Rat as Rational;
P5: -s = (-1.F_Rat)*s by VECTSP_1:14;
P1: (-1.INT.Ring)*v = (-1.F_Rat)*s by LM3;
v+(-1.INT.Ring)*v = s - s by P1,P5,LM2
.= 0.EZV by RLVECT_1:15
.= 0.ZS by D1;
hence v is right_complementable;
end;
P6: for v, w being Element of ZS holds v + w = w + v
proof
let v, w be Element of ZS;
reconsider s = v, t = w as Vector of EZV by X0;
thus v + w = s+t by LM2
.= w + v by LM2;
end;
P7: for u, v, w being Element of ZS holds (u + v) + w = u + (v + w)
proof
let u, v, w be Element of ZS;
reconsider z = u, s = v, t = w as Vector of EZV by X0;
P1:u + v = z+s by LM2;
P2:v + w = s+t by LM2;
thus (u + v) + w = (z+s) + t by P1,LM2
.= z+(s+t) by RLVECT_1:def 3
.= u + (v + w) by LM2,P2;
end;
for v being Element of ZS holds v + (0. ZS) = v
proof
let v be Element of ZS;
reconsider s = v as Vector of EZV by X0;
thus v + (0. ZS) = s + 0.EZV by LM2,D1
.= v;
end;
hence thesis
by P1,P2,P3,P4,P5,P6,P7,ALGSTR_0:def 16,RLVECT_1:def 2,def 3,def 4,
VECTSP_1:def 14,def 15,def 16,def 17;
end;
then reconsider ZS as strict Z_Module;
take ZS;
thus thesis;
end;
uniqueness;
end;
theorem SB01:
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
proof
let V be torsion-free Z_Module;
set EZV = Z_MQ_VectSp(V);
D1: EZV = ModuleStr(# Class EQRZM(V), addCoset(V), zeroCoset(V),
lmultCoset(V) #) by ZMODUL04:def 5;
set ZS = EMbedding(V);
AS1: the carrier of ZS = rng MorphsZQ(V) &
the ZeroF of ZS = zeroCoset(V) &
the addF of ZS = (addCoset(V)) || ( rng MorphsZQ(V) ) &
the lmult of ZS = (lmultCoset(V)) |
[:the carrier of INT.Ring,rng MorphsZQ(V):] by defEmbedding;
set Cl = the carrier of ZS;
set Add = (addCoset(V)) || Cl;
set Mlt = (lmultCoset(V)) |
[:the carrier of INT.Ring,rng MorphsZQ(V):];
Cl c= the carrier of EZV by AS1;
hence for x being Vector of ZS holds x is Vector of EZV;
thus 0.ZS = 0.EZV by D1,defEmbedding;
thus for x, y being Vector of ZS, v, w being Vector of EZV
st x = v & y = w holds x+y = v+w
proof
let x, y be Vector of ZS,
v, w be Vector of EZV;
assume L0: x = v & y = w;
thus x+y = (addCoset(V)).[x,y] by AS1,FUNCT_1:49
.= v+ w by D1,L0;
end;
thus for i being Element of INT.Ring, j being Element of F_Rat,
x being Vector of ZS, v being Vector of EZV
st i = j & x = v holds i*x = j*v
proof
let i be Element of INT.Ring,
j be Element of F_Rat,
x be Vector of ZS,
v be Vector of EZV;
assume L0: i = j & x = v;
thus i*x = (lmultCoset(V)).[i,x] by AS1,FUNCT_1:49
.= j*v by D1,L0;
end;
end;
theorem SB02:
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)
proof
let V be torsion-free Z_Module;
set EZV = Z_MQ_VectSp(V);
set ZS = EMbedding(V);
set Cl = the carrier of ZS;
set Add =(addCoset(V)) || Cl;
set Mlt = (lmultCoset(V)) |
[:the carrier of INT.Ring,rng MorphsZQ(V):];
thus 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)
proof
let v, w be Vector of Z_MQ_VectSp(V);
assume B1: v in EMbedding(V) & w in EMbedding(V);
reconsider v1 = v, w1 = w as Vector of EMbedding(V) by B1;
v+w = v1+w1 by SB01;
hence thesis;
end;
thus 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)
proof
let j be Element of F_Rat,
v be Vector of Z_MQ_VectSp(V);
assume B1: j in INT & v in EMbedding(V);
then reconsider v1 = v as Vector of EMbedding(V);
reconsider i = j as Element of INT.Ring by B1;
j*v= i*v1 by SB01;
hence thesis;
end;
end;
theorem SB03:
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]) )
proof
let V be torsion-free Z_Module;
set T = MorphsZQ(V);
rng T = the carrier of EMbedding(V) by defEmbedding;
then reconsider T0 = T as Function of V, EMbedding(V) by FUNCT_2:6;
B0: T0 is additive
proof
let x, y be Element of V;
thus T0.(x+y) = T0.x + T0.y
proof
L1: T.(x+y) = T.x + T.y by ZMODUL04:def 6;
reconsider v = T0.x, w = T0.y as Vector of EMbedding(V);
thus T0.(x+y) = T0.x + T0.y by L1,SB01;
end;
end;
for x being Vector of V, i being Element of INT.Ring
holds T0.(i*x) = i*(T0.x)
proof
let x be Vector of V, i be Element of INT.Ring;
thus T0.(i*x) = i*T0.x
proof
reconsider j = i as Element of F_Rat by NUMBERS:14;
L1: T.(i*x) = j*T.x by ZMODUL04:def 6;
reconsider v = T0.x as Vector of EMbedding(V);
thus T0.(i*x) = i*T0.x by L1,SB01;
end;
end;
then T0 is additive homogeneous by B0;
then reconsider T0 as linear-transformation of V, EMbedding(V);
take T0;
SS: T0 is one-to-one by ZMODUL04:def 6;
rng T0 = the carrier of EMbedding(V) by defEmbedding;
then T0 is onto by FUNCT_2:def 3;
hence T0 is bijective by SS;
thus T0 = MorphsZQ(V);
thus thesis by ZMODUL04:def 6;
end;
theorem
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
proof
let V be torsion-free Z_Module, vv be Vector of EMbedding(V);
set Z = EMbedding(V);
consider T be linear-transformation of V, Z such that
A1: T is bijective & T = MorphsZQ(V) &
(for v being Element of V holds T.v = Class(EQRZM(V),[v,1])) by SB03;
vv in the carrier of Z;
then vv in rng MorphsZQ(V) by A1,FUNCT_2:def 3;
then consider v be object such that
A2: v in the carrier of V & vv = (MorphsZQ(V)).v by FUNCT_2:11;
reconsider v as Vector of V by A2;
take v;
thus thesis by A2;
end;
definition
let V be torsion-free Z_Module;
func DivisibleMod(V) -> strict Z_Module means
:defDivisibleMod:
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
set Z = Z_MQ_VectSp(V);
reconsider Z as VectSp of F_Rat;
set Mlt = (lmultCoset(V)) | [:INT, Class EQRZM(V):];
dom lmultCoset(V) = [:the carrier of F_Rat, Class EQRZM(V):]
by FUNCT_2:def 1;
then
Y3: dom Mlt = [:INT, Class EQRZM(V):] by NUMBERS:14,RELAT_1:62,ZFMISC_1:96;
Z1: Z = ModuleStr(# Class EQRZM(V), addCoset(V), zeroCoset(V),
lmultCoset(V) #) by ZMODUL04:def 5;
Z2: 0.Z = zeroCoset(V) by Z1;
for x being object st x in [:INT, Class EQRZM(V):] holds
Mlt.x in Class EQRZM(V)
proof
let x be object;
assume X40: x in [:INT, Class EQRZM(V):];
then consider i, w be object such that
X41: i in INT & w in Class EQRZM(V) & x = [i,w] by ZFMISC_1:def 2;
reconsider i as Element of INT by X41;
reconsider j = i as Element of F_Rat by NUMBERS:14;
reconsider b = w as Element of Z by X41,Z1;
X46: Mlt.x = (lmultCoset(V)).(j,w) by X40,X41,FUNCT_1:49;
[j, w] in [:the carrier of F_Rat, Class EQRZM(V):]
by X41,ZFMISC_1:87;
hence thesis by X46,FUNCT_2:5;
end;
then reconsider Mlt
as Function of [:the carrier of INT.Ring,Class EQRZM(V):],
Class EQRZM(V) by Y3,FUNCT_2:3;
set ZS = ModuleStr(#Class EQRZM(V), addCoset(V), zeroCoset(V), Mlt#);
reconsider ZS as non empty ModuleStr over INT.Ring;
LM2: for x, y being Vector of ZS, v, w being Vector of Z
st x = v & y = w holds x+y = v+w by Z1;
LM3: for i being Element of INT.Ring, j being Element of F_Rat,
x being Vector of ZS, v being Vector of Z
st i = j & x = v holds i*x = j*v
proof
let i be Element of INT.Ring,
j be Element of F_Rat,
x be Vector of ZS,
v be Vector of Z;
assume L0: i = j & x = v;
thus i*x = (lmultCoset(V)).[i,x] by FUNCT_1:49
.= j*v by L0,Z1;
end;
ZS is Abelian add-associative right_zeroed
right_complementable scalar-distributive vector-distributive
scalar-associative scalar-unital non empty ModuleStr over INT.Ring
proof
P1: for x being Element of INT.Ring
for v, w being Element of ZS holds x * (v + w) = (x * v) + (x * w)
proof
let x be Element of INT.Ring, v, w be Element of ZS;
reconsider y = x as Element of F_Rat by NUMBERS:14;
reconsider s = v, t = w as Vector of Z by Z1;
P2: x*v =y*s & x*w =y*t by LM3;
thus x * (v + w) = y*( s + t ) by Z1,LM3
.= y*s + y*t by VECTSP_1:def 14
.= x*v + x*w by P2,Z1;
end;
P2: for x, y being Element of INT.Ring
for v being Element of ZS holds (x + y) * v = (x * v) + (y * v)
proof
let x, y be Element of INT.Ring, v be Element of ZS;
reconsider p = x,q = y as Element of F_Rat by NUMBERS:14;
reconsider p1 = p,q1 = q as Rational;
reconsider s = v as Vector of Z by Z1;
P2: y*v = q*s by LM3;
thus (x + y) * v = (p+q)*s by LM3
.= p*s + q*s by VECTSP_1:def 15
.= x*v + y*v by P2,Z1,LM3;
end;
P3: for x, y being Element of INT.Ring
for v being Element of ZS holds (x * y) * v = x * (y * v)
proof
let x, y be Element of INT.Ring,v be Element of ZS;
reconsider p = x,q = y as Element of F_Rat by NUMBERS:14;
reconsider p1 = p,q1 = q as Rational;
reconsider s = v as Vector of Z by Z1;
P1: y*v = q*s by LM3;
thus (x * y) * v = (p*q)*s by LM3
.= p*(q*s) by VECTSP_1:def 16
.= x*(y*v) by P1,LM3;
end;
P4: for v being Element of ZS holds 1.INT.Ring * v = v
proof
let v be Element of ZS;
reconsider s = v as Vector of Z by Z1;
thus 1.INT.Ring * v = 1.F_Rat *s by LM3
.= v by VECTSP_1:def 17;
end;
P5: for v being Element of ZS holds v is right_complementable
proof
let v be Element of ZS;
reconsider s = v as Vector of Z by Z1;
reconsider i1 = 1.F_Rat as Rational;
P5: -s = (-1.F_Rat)*s by VECTSP_1:14;
v+(-1.INT.Ring)*v = s - s by P5,Z1,LM3
.= 0.ZS by Z2,RLVECT_1:15;
hence v is right_complementable;
end;
P6: for v, w being Element of ZS holds v + w = w + v
proof
let v, w be Element of ZS;
reconsider s = v, t = w as Vector of Z by Z1;
thus v + w = s+t by Z1
.= w + v by LM2;
end;
P7: for u, v, w being Element of ZS holds (u + v) + w = u + (v + w)
proof
let u, v, w be Element of ZS;
reconsider z = u, s = v, t = w as Vector of Z by Z1;
thus (u + v) + w = (z+s) + t by Z1
.= z+(s+t) by RLVECT_1:def 3
.= u + (v + w) by Z1;
end;
for v being Element of ZS holds v + (0. ZS) = v
proof
let v be Element of ZS;
reconsider s = v as Vector of Z by Z1;
thus v + (0. ZS) = s + 0.Z by Z1
.= v;
end;
hence thesis
by P1,P2,P3,P4,P5,P6,P7,ALGSTR_0:def 16,RLVECT_1:def 2,def 3,def 4,
VECTSP_1:def 14,def 15,def 16,def 17;
end;
then reconsider ZS as strict Z_Module;
take ZS;
thus thesis;
end;
uniqueness;
end;
theorem ThDivisible1:
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
proof
let V be torsion-free Z_Module;
thus 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
proof
let v be Vector of DivisibleMod(V);
assume AS: ex a being Element of INT.Ring st a <> 0 &
for u being Vector of DivisibleMod(V) holds a*u <> v;
consider a be Element of INT.Ring such that
B1: a <> 0 &
for u being Vector of DivisibleMod(V) holds a*u <> v by AS;
reconsider vv = v as Element of Class EQRZM(V) by defDivisibleMod;
set Z = Z_MQ_VectSp(V);
reconsider Z as VectSp of F_Rat;
BX: Z = ModuleStr(# Class EQRZM(V), addCoset(V), zeroCoset(V),
lmultCoset(V) #) by ZMODUL04:def 5;
reconsider vv as Element of Z by BX;
reconsider aa = a as Element of F_Rat by NUMBERS:14;
B2: aa <> 0.F_Rat by B1;
reconsider ai = aa" as Element of F_Rat;
B3: aa * ai = 1.F_Rat by B2,VECTSP_1:def 10;
set uu = ai*vv;
reconsider uu as Element of Z;
reconsider u = uu as Element of DivisibleMod(V) by BX,defDivisibleMod;
aa*uu = (aa*ai)*vv by VECTSP_1:def 16
.= vv by B3,VECTSP_1:def 17;
then v = ((lmultCoset(V)) | [:INT, Class EQRZM(V):]).[a,u]
by BX,FUNCT_1:49,ZFMISC_1:87
.= a*u by defDivisibleMod;
hence contradiction by B1;
end;
end;
registration
let V be torsion-free Z_Module;
cluster DivisibleMod(V) -> divisible;
correctness
proof
thus for v being Vector of DivisibleMod(V) holds v is divisible
by ThDivisible1;
end;
end;
theorem ThDivisible2:
for V being torsion-free Z_Module holds
EMbedding(V) is Submodule of DivisibleMod(V)
proof
let V be torsion-free Z_Module;
set EV = EMbedding(V);
set DV = DivisibleMod(V);
for x being object st x in the carrier of EV holds x in the carrier of DV
proof
let x be object such that
B1: x in the carrier of EV;
x in rng MorphsZQ(V) by B1,defEmbedding;
then consider y be object such that
B2: y in the carrier of V & (MorphsZQ(V)).y = x by FUNCT_2:11;
reconsider y as Vector of V by B2;
B3: Z_MQ_VectSp(V) = ModuleStr(# Class EQRZM(V), addCoset(V),
zeroCoset(V), lmultCoset(V) #) by ZMODUL04:def 5;
x in Class EQRZM(V) by B2,B3,FUNCT_2:5;
hence thesis by defDivisibleMod;
end;
then A1: the carrier of EV c= the carrier of DV;
A2: 0.EV = zeroCoset(V) by defEmbedding
.= 0.DV by defDivisibleMod;
A3: the addF of EV = (addCoset(V)) || ( rng MorphsZQ(V) ) by defEmbedding
.= (the addF of DV) || ( rng MorphsZQ(V) ) by defDivisibleMod
.= (the addF of DV) || (the carrier of EV) by defEmbedding;
the lmult of EV = (the lmult of DV) | [:the carrier of INT.Ring,
rng MorphsZQ(V):]
proof
the carrier of EV c= Class EQRZM(V) by A1,defDivisibleMod;
then B1: rng MorphsZQ(V) c= Class EQRZM(V) by defEmbedding;
thus the lmult of EV = (lmultCoset(V)) |
[:the carrier of INT.Ring, rng MorphsZQ(V):]
by defEmbedding
.= ((lmultCoset(V)) | [:the carrier of INT.Ring, Class EQRZM(V):])
| [:the carrier of INT.Ring, rng MorphsZQ(V):]
by B1,RELAT_1:74,ZFMISC_1:96
.= (the lmult of DV) | [:the carrier of INT.Ring, rng MorphsZQ(V):]
by defDivisibleMod;
end;
then the lmult of EV = (the lmult of DV) |
[:the carrier of INT.Ring, (the carrier of EV):]
by defEmbedding;
hence thesis by A1,A2,A3,VECTSP_4:def 2;
end;
registration
let V be finitely-generated torsion-free Z_Module;
cluster EMbedding(V) -> finitely-generated;
correctness
proof
consider T be linear-transformation of V, EMbedding(V) such that
A1: T is bijective & T = MorphsZQ(V) &
(for v being Vector of V holds T.v = Class(EQRZM(V), [v, 1])) by SB03;
reconsider Z = EMbedding(V) as free Z_Module by A1,ZMODUL06:48;
Z is finite-rank by A1,ZMODUL06:50;
hence thesis;
end;
end;
registration
let V be non trivial torsion-free Z_Module;
cluster EMbedding(V) -> non trivial;
correctness
proof
consider T be linear-transformation of V, EMbedding(V) such that
A1: T is bijective & T = MorphsZQ(V) &
(for v being Vector of V holds T.v = Class(EQRZM(V), [v,1])) by SB03;
set v = the non zero Vector of V;
T.v <> 0.EMbedding(V)
proof
assume T.v = 0.EMbedding(V);
then T.v = T.(0.V) by ZMODUL05:19;
hence contradiction by A1,FUNCT_2:19;
end;
then not T.v in (0).EMbedding(V) by ZMODUL02:66;
then (Omega).EMbedding(V) <> (0).EMbedding(V);
hence thesis by ZMODUL07:41;
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
{a*u where u is Vector of V: u in W};
coherence
proof
set Y = {a*u where u is Vector of V : u in W};
defpred Sep[object] means ex u being Vector of V st $1 = a*u & u in W;
consider X be set such that
A1: for x being object holds x in X iff x in the carrier of V & Sep[x]
from XBOOLE_0:sch 1;
X c= the carrier of V by A1;
then reconsider X as Subset of V;
A2: Y c= X
proof
let x be object;
assume x in Y;
then ex u being Vector of V st x = a*u & u in W;
hence thesis by A1;
end;
X c= Y
proof
let x be object;
assume x in X;
then ex u being Vector of V st x = a*u & u in W by A1;
hence thesis;
end;
hence thesis by A2,XBOOLE_0:def 10;
end;
end;
definition
let V be torsion-free Z_Module, r be Element of F_Rat;
func EMbedding(r,V) -> strict Z_Module means :defriV:
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
set EZV = Z_MQ_VectSp(V);
D1: EZV
= ModuleStr(# Class EQRZM(V), addCoset(V), zeroCoset(V), lmultCoset(V) #)
by ZMODUL04:def 5;
AX: EZV is scalar-distributive vector-distributive
scalar-associative scalar-unital add-associative right_zeroed
right_complementable Abelian non empty;
BX: rng MorphsZQ(V) = the carrier of EMbedding(V) by defEmbedding;
set Cl = r* (rng MorphsZQ(V));
set Add =(addCoset(V)) || Cl;
set Mlt = (lmultCoset(V)) | [:INT,Cl:];
X0: Cl c= the carrier of EZV;
dom addCoset(V) = [:the carrier of EZV,the carrier of EZV:]
by D1,FUNCT_2:def 1; then
X3: dom Add = [:Cl,Cl:] by RELAT_1:62;
for x being object st x in [:Cl,Cl:]
holds Add.x in Cl
proof
let x be object;
assume X40: x in [:Cl,Cl:];
then consider v0,w0 be object such that
X41: v0 in Cl & w0 in Cl & x = [v0,w0] by ZFMISC_1:def 2;
consider v be Vector of EZV such that
X410: v0 = r*v & v in (rng MorphsZQ(V)) by X41;
consider w be Vector of EZV such that
X411: w0 = r*w & w in (rng MorphsZQ(V)) by X41;
v in EMbedding(V) &
w in EMbedding(V) by X410,X411,defEmbedding;
then
X42: v+w in EMbedding(V) by SB02;
Add.x = r*v + r*w by X40,X41,X410,X411,D1,FUNCT_1:49
.= r*(v+w) by VECTSP_1:def 14;
hence Add.x in Cl by BX,X42;
end;
then reconsider Add as BinOp of Cl by X3,FUNCT_2:3;
dom lmultCoset(V) = [:the carrier of F_Rat,the carrier of EZV:]
by FUNCT_2:def 1,D1;
then
Y3: dom Mlt = [:the carrier of INT.Ring,Cl:]
by RELAT_1:62,NUMBERS:14,ZFMISC_1:96;
for x being object st x in [:the carrier of INT.Ring,Cl:]
holds Mlt.x in Cl
proof
let x be object;
assume X40: x in [:the carrier of INT.Ring,Cl:];
then consider i, w0 be object such that
X41: i in INT & w0 in Cl & x = [i,w0] by ZFMISC_1:def 2;
reconsider i1=i as Integer by X41;
reconsider i2=i as Element of F_Rat by X41,NUMBERS:14;
consider w be Vector of EZV such that
X411: w0=r*w & w in (rng MorphsZQ(V)) by X41;
w in EMbedding(V) by X411,defEmbedding;
then
X42: i2*w in EMbedding(V) by SB02,X41;
Mlt.x = i2*(r*w) by D1,X40,X411,X41,FUNCT_1:49
.= (i2*r)*w by VECTSP_1:def 16
.= r*(i2*w) by VECTSP_1:def 16;
hence Mlt.x in Cl by BX,X42;
end;
then reconsider Mlt = (lmultCoset(V))
| [:the carrier of INT.Ring,Cl:]
as Function of [:the carrier of INT.Ring,Cl:], Cl by Y3,FUNCT_2:3;
X1: r*(0.EZV) = 0.EZV by VECTSP_1:15;
0.EZV = 0.EMbedding(V) by D1,defEmbedding;
then
X2: 0.EZV in r*(rng MorphsZQ(V)) by BX,X1;
reconsider z = zeroCoset(V) as Element of Cl by D1,X2;
set ZS = ModuleStr(#Cl,Add,z,Mlt#);
reconsider ZS as non empty ModuleStr over INT.Ring by X2;
LM2: for x, y being Vector of ZS, v, w being Vector of EZV
st x = v & y = w
holds x+y = v+w
proof
let x, y be Vector of ZS, v, w be Vector of EZV;
assume L0: x = v & y = w;
thus x+y = (addCoset(V)).[x,y] by FUNCT_1:49
.= v+ w by D1,L0;
end;
LM3: for i being Element of INT.Ring, j being Element of F_Rat,
x being Vector of ZS, v being Vector of EZV
st i = j & x = v
holds i*x = j*v
proof
let i be Element of INT.Ring,
j be Element of F_Rat,
x be Vector of ZS,
v be Vector of EZV;
assume L0: i = j & x = v;
thus i*x = (lmultCoset(V)).[i,x] by FUNCT_1:49
.= j*v by D1,L0;
end;
ZS is Abelian add-associative right_zeroed
right_complementable scalar-distributive vector-distributive
scalar-associative scalar-unital non empty ModuleStr over INT.Ring
proof
P1: for x being Element of INT.Ring
for v, w being Element of ZS holds x * (v + w) = (x * v) + (x * w)
proof
let x be Element of INT.Ring, v, w be Element of ZS;
reconsider y = x as Element of F_Rat by NUMBERS:14;
reconsider s = v, t = w as Vector of EZV by X0;
P1: v+w = s+t by LM2;
P2: x*v =y*s & x*w =y*t by LM3;
thus x * (v + w) = y*( s + t ) by P1,LM3
.= y*s + y*t by AX
.= x*v + x*w by LM2,P2;
end;
P2: for x, y being Element of INT.Ring
for v being Element of ZS holds (x + y) * v = (x * v) + (y * v)
proof
let x, y be Element of INT.Ring, v be Element of ZS;
reconsider p = x, q = y as Element of F_Rat by NUMBERS:14;
reconsider p1 = p,q1 = q as Rational;
reconsider s = v as Vector of EZV by X0;
P1: x*v = p*s by LM3;
P2: y*v = q*s by LM3;
thus (x + y) * v = (p+q)*s by LM3
.= p*s + q*s by AX
.= x*v + y*v by P1,P2,LM2;
end;
P3: for x, y being Element of INT.Ring, v being Element of ZS holds
(x * y) * v = x * (y * v)
proof
let x, y be Element of INT.Ring,v be Element of ZS;
reconsider p = x,q = y as Element of F_Rat by NUMBERS:14;
reconsider p1 = p,q1 = q as Rational;
reconsider s = v as Vector of EZV by X0;
P1: y*v = q*s by LM3;
thus (x * y) * v = (p*q)*s by LM3
.= p*(q*s) by AX
.= x*(y*v) by P1,LM3;
end;
P4: for v being Element of ZS holds 1.INT.Ring * v = v
proof
let v be Element of ZS;
reconsider s = v as Vector of EZV by X0;
thus 1.INT.Ring * v = 1.F_Rat *s by LM3
.= v by AX;
end;
P5: for v being Element of ZS holds v is right_complementable
proof
let v be Element of ZS;
reconsider s = v as Vector of EZV by X0;
reconsider i1 = 1.F_Rat as Rational;
P5: -s = (-1.F_Rat)*s by VECTSP_1:14;
P1: (-1.INT.Ring)*v = (-1.F_Rat)*s by LM3;
v+(-1.INT.Ring)*v = s - s by P1,P5,LM2
.= 0.EZV by RLVECT_1:15
.= 0.ZS by D1;
hence v is right_complementable;
end;
P6: for v, w being Element of ZS holds v + w = w + v
proof
let v, w be Element of ZS;
reconsider s = v, t = w as Vector of EZV by X0;
thus v + w = s+t by LM2
.= w + v by LM2;
end;
P7: for u, v, w being Element of ZS holds (u + v) + w = u + (v + w)
proof
let u, v, w be Element of ZS;
reconsider z = u, s = v, t = w as Vector of EZV by X0;
P1:u + v = z+s by LM2;
P2:v + w = s+t by LM2;
thus (u + v) + w = (z+s) + t by P1,LM2
.= z+(s+t) by RLVECT_1:def 3
.= u + (v + w) by LM2,P2;
end;
for v being Element of ZS holds v + (0. ZS) = v
proof
let v be Element of ZS;
reconsider s = v as Vector of EZV by X0;
thus v + (0. ZS) = s + 0.EZV by LM2,D1
.= v;
end;
hence thesis
by P1,P2,P3,P4,P5,P6,P7,ALGSTR_0:def 16,RLVECT_1:def 2,def 3,def 4,
VECTSP_1:def 14,def 15,def 16,def 17;
end;
then reconsider ZS as strict Z_Module;
take ZS;
thus thesis;
end;
uniqueness;
end;
theorem rSB01:
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
proof
let V be torsion-free Z_Module,
r be Element of F_Rat;
set EZV = Z_MQ_VectSp(V);
D1: EZV = ModuleStr(# Class EQRZM(V), addCoset(V), zeroCoset(V),
lmultCoset(V) #) by ZMODUL04:def 5;
set ZS = EMbedding(r,V);
AS1: the carrier of ZS = r*(rng MorphsZQ(V)) &
the ZeroF of ZS = zeroCoset(V) &
the addF of ZS = (addCoset(V)) || ( r*(rng MorphsZQ(V)) ) &
the lmult of ZS = (lmultCoset(V)) | [:INT,r*(rng MorphsZQ(V)):] by defriV;
set Cl = the carrier of ZS;
set Add = (addCoset(V)) || Cl;
set Mlt = (lmultCoset(V)) | [:INT,r*(rng MorphsZQ(V)):];
X0: Cl c= the carrier of EZV by AS1;
thus for x being Vector of ZS holds x is Vector of EZV by X0;
thus 0.ZS = 0.EZV by D1,defriV;
thus for x, y being Vector of ZS, v, w being Vector of EZV
st x = v & y = w
holds x+y = v+w
proof
let x, y be Vector of ZS,
v, w be Vector of EZV;
assume L0: x = v & y = w;
thus x+y = (addCoset(V)).[x,y] by AS1,FUNCT_1:49
.= v+ w by D1,L0;
end;
thus for i being Element of INT.Ring, j being Element of F_Rat,
x being Vector of ZS, v being Vector of EZV
st i = j & x = v holds i*x = j*v
proof
let i be Element of INT.Ring,
j be Element of F_Rat,
x be Vector of ZS,
v be Vector of EZV;
assume L0: i = j & x = v;
thus i*x = (lmultCoset(V)).[i,x] by AS1,FUNCT_1:49
.= j*v by D1,L0;
end;
end;
theorem
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)
proof
let V be torsion-free Z_Module,
r be Element of F_Rat;
set EZV = Z_MQ_VectSp(V);
set ZS = EMbedding(r,V);
set Cl = the carrier of ZS;
set Add =(addCoset(V)) || Cl;
set Mlt = (lmultCoset(V)) | [:INT,r*(rng MorphsZQ(V)):];
thus 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)
proof
let v, w be Vector of Z_MQ_VectSp(V);
assume B1: v in EMbedding(r,V) & w in EMbedding(r,V);
reconsider v1 = v, w1 = w as Vector of EMbedding(r,V) by B1;
v+w = v1+w1 by rSB01;
hence thesis;
end;
thus 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)
proof
let j be Element of F_Rat,
v be Vector of Z_MQ_VectSp(V);
assume B1: j in INT & v in EMbedding(r,V);
then reconsider v1 = v as Vector of EMbedding(r,V);
reconsider i = j as Element of INT.Ring by B1;
j*v= i*v1 by rSB01;
hence thesis;
end;
end;
theorem rSB03A:
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
proof
let V be torsion-free Z_Module,
r be Element of F_Rat;
assume AS: r <> 0.F_Rat;
set EZV = Z_MQ_VectSp(V);
deffunc F(Vector of EZV) = r*$1;
consider T be Function of the carrier of EZV, the carrier of EZV
such that
P1: for x being Element of the carrier of EZV holds T.x = F(x)
from FUNCT_2:sch 4;
set T0 = T | the carrier of EMbedding(V);
D0: the carrier of EMbedding(V) = rng MorphsZQ(V) by defEmbedding;
dom T = the carrier of EZV by FUNCT_2:def 1;
then
P3: dom T0 = the carrier of EMbedding(V) by D0,RELAT_1:62;
D1: the carrier of EMbedding(r,V) = r * (rng MorphsZQ(V)) by defriV;
RX0: for y being object
holds y in rng T0 iff y in the carrier of EMbedding(r,V)
proof
let y be object;
hereby
assume y in rng T0;
then consider x be object such that
A2: x in dom T0 & y = T0.x by FUNCT_1:def 3;
reconsider x as Element of EZV by A2;
T0.x = T.x by FUNCT_1:49,A2,P3
.= r*x by P1;
hence y in the carrier of EMbedding(r,V) by A2,D0,D1,P3;
end;
assume y in the carrier of EMbedding(r,V);
then y in r * (rng MorphsZQ(V)) by defriV;
then consider x be Vector of EZV such that
A4: y = r*x & x in rng MorphsZQ(V);
A5: x in the carrier of EMbedding(V) by A4,defEmbedding;
T0.x = T.x by FUNCT_1:49,A5
.= y by A4,P1;
hence y in rng T0 by A5,P3,FUNCT_1:def 3;
end;
then rng T0 = the carrier of EMbedding(r,V) by TARSKI:2;
then reconsider T0 as Function of EMbedding(V),EMbedding(r,V)
by P3,FUNCT_2:1;
B0: T0 is additive
proof
let x, y be Element of EMbedding(V);
F1: x in EMbedding(V) & y in EMbedding(V);
reconsider x0=x,y0=y as Vector of EZV by SB01;
F2: x0 + y0 in EMbedding(V) by F1,SB02;
F3: T.x0 = T0.x by FUNCT_1:49;
F4: T.y0 = T0.y by FUNCT_1:49;
thus T0.(x+y) = T0.(x0+y0) by SB01
.= T.(x0+y0) by FUNCT_1:49,F2
.= r*(x0+y0) by P1
.= r*x0 + r*y0 by VECTSP_1:def 14
.= T.x0 + r*y0 by P1
.= T.x0 + T.y0 by P1
.= T0.x + T0.y by rSB01,F3,F4;
end;
for x being Element of EMbedding(V), i being Element of INT.Ring
holds T0.(i*x) = i*(T0.x)
proof
let x be Element of EMbedding(V), i be Element of INT.Ring;
F1: x in EMbedding(V);
reconsider x0 = x as Vector of EZV by SB01;
reconsider j = i as Element of F_Rat by NUMBERS:14;
F2: j*x0 in EMbedding(V) by F1,SB02;
F3: T.x0 = T0.x by FUNCT_1:49;
thus T0.(i*x) = T0.(j*x0) by SB01
.= T.(j*x0) by FUNCT_1:49,F2
.= r*(j*x0) by P1
.= (r*j)*x0 by VECTSP_1:def 16
.= j*(r*x0) by VECTSP_1:def 16
.= i*T0.x by rSB01,F3,P1;
end;
then T0 is additive homogeneous by B0;
then reconsider T0 as linear-transformation of EMbedding(V),EMbedding(r,V);
take T0;
thus
XX1: for v being Element of Z_MQ_VectSp(V) st v in EMbedding(V)
holds T0.v = r*v
proof
let x be Element of Z_MQ_VectSp(V);
assume F1: x in EMbedding(V);
thus T0.x = T.x by FUNCT_1:49,F1
.= r*x by P1;
end;
for x1, x2 being object st
x1 in the carrier of EMbedding(V)
& x2 in the carrier of EMbedding(V)
& T0.x1 = T0.x2 holds x1 = x2
proof
let x1, x2 be object;
assume AS2: x1 in the carrier of EMbedding(V)
& x2 in the carrier of EMbedding(V) & T0.x1 = T0.x2;
then reconsider xx1 = x1, xx2 = x2 as Element of EZV by D0;
Q0: xx1 in EMbedding(V) & xx2 in EMbedding(V) by AS2;
Q1: T0.x1 = r*xx1 by Q0,XX1;
Q2: r"*(r*xx1) = r"*(r*xx2) by AS2,Q0,Q1,XX1;
r"*(r*xx1) = xx1 by AS,VECTSP_1:20;
hence x1 = x2 by Q2,AS,VECTSP_1:20;
end; then
T1: T0 is one-to-one by FUNCT_2:19;
T0 is onto by RX0,FUNCT_2:def 3,TARSKI:2;
hence thesis by T1;
end;
theorem ThEM1:
for V being torsion-free Z_Module, v being Vector of V holds
Class(EQRZM(V), [v, 1]) in EMbedding(V)
proof
let V be torsion-free Z_Module, v be Vector of V;
(MorphsZQ(V)).v = Class(EQRZM(V), [v, 1]) by ZMODUL04:def 6;
then Class(EQRZM(V), [v, 1]) in rng MorphsZQ(V) by FUNCT_2:4;
hence thesis by defEmbedding;
end;
theorem ThDM1:
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)
proof
let V be torsion-free Z_Module, v be Vector of DivisibleMod(V);
A1: v in the carrier of DivisibleMod(V);
reconsider vv = v as Element of Class EQRZM(V) by defDivisibleMod;
AX1: v in Class EQRZM(V) by A1,defDivisibleMod;
v is Element of ModuleStr (# Class EQRZM(V), addCoset(V),
zeroCoset(V), lmultCoset(V) #) by defDivisibleMod;
then consider a be Element of INT.Ring, z be Vector of V such that
A2: a <> 0 & v = Class(EQRZM(V), [z, a]) by ZMODUL04:5;
reconsider aq = a as Element of F_Rat by NUMBERS:14;
A3: aq = a / 1 & 1 <> 0;
AX4: v in Class EQRZM(V) by A1,defDivisibleMod;
a * v = ((lmultCoset(V)) | [:INT, Class EQRZM(V):]).(a, v)
by defDivisibleMod
.= (lmultCoset(V)).(a, v) by AX4,FUNCT_1:49,ZFMISC_1:87
.= Class(EQRZM(V), [a*z, 1.INT.Ring*a]) by AX1,A2,A3,ZMODUL04:def 4
.= Class(EQRZM(V), [z, 1.INT.Ring]) by A2,ZMODUL04:4;
hence thesis by A2,ThEM1;
end;
registration
let V be torsion-free Z_Module;
cluster DivisibleMod(V) -> torsion-free;
correctness
proof
set D = DivisibleMod(V);
set Z = EMbedding(V);
assume D is non torsion-free;
then consider v be Vector of D such that
P1: v <> 0.D & v is torsion;
consider i be Element of INT.Ring such that
P2: i <> 0 & i * v = 0.D by P1;
v in the carrier of D;
then A1: v in Class EQRZM(V) by defDivisibleMod;
reconsider vv = v as Element of Class EQRZM(V) by defDivisibleMod;
v is Element of ModuleStr(# Class EQRZM(V), addCoset(V),
zeroCoset(V), lmultCoset(V) #) by defDivisibleMod;
then consider a be Element of INT.Ring, z be Vector of V such that
A2: a <> 0 & v = Class(EQRZM(V), [z, a]) by ZMODUL04:5;
reconsider iq = i as Element of F_Rat by NUMBERS:14;
A4: iq = i / 1 & 1 <> 0;
A6: i * v = ((lmultCoset(V)) | [:INT, Class EQRZM(V):]).(i, v)
by defDivisibleMod
.= (lmultCoset(V)).(i, v) by A1,FUNCT_1:49,ZFMISC_1:87
.= Class(EQRZM(V), [i*z, 1.INT.Ring *a]) by A1,A2,A4,ZMODUL04:def 4
.= Class(EQRZM(V), [i*z, a]);
A7: not a in {0} by A2,TARSKI:def 1;
a in INT \ {0} by A7,XBOOLE_0:def 5;
then A8: [i*z, a] in [:the carrier of V, (INT \ {0}):] by ZFMISC_1:87;
Class(EQRZM(V), [i*z, a]) = zeroCoset(V) by P2,A6,defDivisibleMod
.= Class(EQRZM(V), [0.V, a]) by A2,ZMODUL04:def 3;
then [[i*z, a], [0.V, a]] in EQRZM(V) by A8,EQREL_1:35;
then a * 0.V = a * (i*z) by ZMODUL04:3;
then A9: 0.V = a * (i*z) by ZMODUL01:1
.= (a*i) * z by VECTSP_1:def 16;
A10: z <> 0.V
proof
assume z = 0.V;
then v = zeroCoset(V) by A2,ZMODUL04:def 3
.= 0.D by defDivisibleMod;
hence contradiction by P1;
end;
z is torsion by P2,A2,A9;
then V is non torsion-free by A10;
hence contradiction;
end;
end;
registration
let V be torsion-free Z_Module;
cluster EMbedding(V) -> torsion-free;
correctness
proof
EMbedding(V) is Submodule of DivisibleMod(V) by ThDivisible2;
hence thesis;
end;
end;
registration
let V be free Z_Module;
cluster EMbedding(V) -> free;
correctness
proof
consider T be linear-transformation of V, EMbedding(V) such that
A1: T is bijective & T = MorphsZQ(V) &
(for v being Vector of V holds T.v = Class(EQRZM(V), [v,1])) by SB03;
thus thesis by A1,ZMODUL06:48;
end;
end;
theorem ThDivisibleX1:
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
let V be torsion-free Z_Module;
A1: Z_MQ_VectSp(V) = ModuleStr(# Class EQRZM(V), addCoset(V),
zeroCoset(V), lmultCoset(V) #) by ZMODUL04:def 5;
thus for v being Vector of Z_MQ_VectSp(V) holds
v is Vector of DivisibleMod(V) by A1,defDivisibleMod;
thus for v being Vector of DivisibleMod(V) holds
v is Vector of Z_MQ_VectSp(V) by A1,defDivisibleMod;
thus 0.(DivisibleMod(V)) = 0.(Z_MQ_VectSp(V)) by A1,defDivisibleMod;
end;
theorem ThDivisibleX2:
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)
proof
let V be torsion-free Z_Module;
A1: Z_MQ_VectSp(V) = ModuleStr(# Class EQRZM(V), addCoset(V),
zeroCoset(V), lmultCoset(V) #) by ZMODUL04:def 5;
thus 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 by A1,defDivisibleMod;
thus A2: 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
proof
let z be Vector of DivisibleMod(V), w be Vector of Z_MQ_VectSp(V),
a be Element of INT.Ring, aq be Element of F_Rat such that
B1: z = w & a = aq;
thus a * z = ((lmultCoset(V)) | [:INT, Class EQRZM(V):]).(a, z)
by defDivisibleMod
.= aq * w by A1,B1,FUNCT_1:49,ZFMISC_1:87;
end;
thus A3: 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
proof
let z be Vector of DivisibleMod(V), w be Vector of Z_MQ_VectSp(V),
aq be Element of F_Rat, a be Element of INT.Ring such that
B1: a <> 0 & aq = a & a * z = aq * w;
assume B2: z <> w;
reconsider ww = w as Vector of DivisibleMod(V) by ThDivisibleX1;
B4: a * ww = a * z by A2,B1;
a * (z - ww) = a*z - a*ww by ZMODUL01:8
.= 0.(DivisibleMod(V)) by B4,RLVECT_1:15;
then z - ww is torsion by B1;
hence contradiction by B2,RLVECT_1:21,ZMODUL06:def 3;
end;
thus 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
proof
let x be Vector of DivisibleMod(V), v be Vector of Z_MQ_VectSp(V),
r be Element of F_Rat, m, n be Element of INT.Ring,
mi,ni be Integer such that
B1: m=mi & n=ni & x = v & r <> 0.F_Rat & n <> 0 & r = mi / ni;
consider y be Vector of DivisibleMod(V) such that
B2: n * y = x by B1,ThDivisible1;
take y;
reconsider mq = m, nq = n as Element of F_Rat by NUMBERS:14;
B3: nq * r = mq by B1,XCMPLX_1:87;
B4: n * (m * y) = (n * m) * y by VECTSP_1:def 16
.= m * x by B2,VECTSP_1:def 16;
nq * (r * v) = mq * v by B3,VECTSP_1:def 16;
then n * (m * y) = nq * (r * v) by A2,B1,B4;
hence thesis by A3,B1,B2;
end;
end;
theorem ThDivisible3:
for V being torsion-free Z_Module, r being Element of F_Rat holds
EMbedding(r, V) is Submodule of DivisibleMod(V)
proof
let V be torsion-free Z_Module, r be Element of F_Rat;
set Z = EMbedding(r, V);
set D = DivisibleMod(V);
for x being object st x in the carrier of EMbedding(r, V) holds
x in the carrier of DivisibleMod(V)
proof
let x be object such that
B1: x in the carrier of EMbedding(r, V);
x is Vector of Z_MQ_VectSp(V) by B1,rSB01;
then x is Vector of DivisibleMod(V) by ThDivisibleX1;
hence thesis;
end;
then A1: the carrier of Z c= the carrier of D;
A2: the addF of Z = (addCoset(V)) || (r * (rng MorphsZQ(V))) by defriV
.= (addCoset(V)) || the carrier of Z by defriV
.= (the addF of D) || the carrier of Z by defDivisibleMod;
A3: 0.Z = zeroCoset(V) by defriV
.= 0.D by defDivisibleMod;
A4: [:the carrier of INT.Ring, the carrier of Z:]
c= [:the carrier of INT.Ring, the carrier of D:] by A1,ZFMISC_1:96;
(the lmult of D) | [:the carrier of INT.Ring, the carrier of Z:]
= ((lmultCoset(V)) | [:the carrier of INT.Ring, Class EQRZM(V):])
| [:the carrier of INT.Ring, the carrier of Z:]
by defDivisibleMod
.= ((lmultCoset(V)) | [:the carrier of INT.Ring, the carrier of D:])
| [:INT, the carrier of Z:] by defDivisibleMod
.= (lmultCoset(V)) | [:the carrier of INT.Ring, the carrier of Z:]
by A4,FUNCT_1:51
.= (lmultCoset(V)) | [:the carrier of INT.Ring,
r * (rng MorphsZQ(V)):] by defriV
.= (the lmult of Z) by defriV;
hence thesis by A1,A2,A3,VECTSP_4:def 2;
end;
registration
let V be finitely-generated torsion-free Z_Module;
let r be Element of F_Rat;
cluster EMbedding(r, V) -> finitely-generated;
correctness
proof
per cases;
suppose B1: r is zero;
B2: for v being Vector of Z_MQ_VectSp(V) st v in r * (rng MorphsZQ(V))
holds v = 0.Z_MQ_VectSp(V)
proof
let v be Vector of Z_MQ_VectSp(V) such that
C1: v in r * (rng MorphsZQ(V));
consider u be Vector of Z_MQ_VectSp(V) such that
C2: v = 0.F_Rat*u & u in rng MorphsZQ(V) by B1,C1;
thus v = 0.Z_MQ_VectSp(V) by C2,VECTSP_1:14;
end;
B3: EMbedding(r, V) is strict Submodule of DivisibleMod(V)
by ThDivisible3;
for v being Vector of DivisibleMod(V) holds
v in EMbedding(r, V) iff v in (0).DivisibleMod(V)
proof
let v be Vector of DivisibleMod(V);
hereby
assume v in EMbedding(r, V);
then v in r * (rng MorphsZQ(V)) by defriV;
then v = 0.Z_MQ_VectSp(V) by B2
.= 0.DivisibleMod(V) by ThDivisibleX1;
hence v in (0).DivisibleMod(V) by ZMODUL02:66;
end;
assume v in (0).DivisibleMod(V);
then v = 0.DivisibleMod(V) by ZMODUL02:66
.= 0.EMbedding(r, V) by B3,ZMODUL01:26;
hence thesis;
end;
hence thesis by B3,ZMODUL01:46;
end;
suppose r is non zero;
then consider T be linear-transformation of EMbedding(V), EMbedding(r, V)
such that
A1: (for v being Vector of Z_MQ_VectSp(V) st v in EMbedding(V)
holds T.v = r * v) & T is bijective by rSB03A;
reconsider Z = EMbedding(r, V) as free Z_Module by A1,ZMODUL06:48;
Z is finite-rank by A1,ZMODUL06:50;
hence thesis;
end;
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;
correctness
proof
consider T be linear-transformation of EMbedding(V), EMbedding(r, V)
such that
A1: (for v being Element of Z_MQ_VectSp(V) st v in EMbedding(V)
holds T.v = r*v) &
T is bijective by rSB03A;
set v = the non zero Vector of EMbedding(V);
T.v <> 0.EMbedding(r, V)
proof
assume T.v = 0.EMbedding(r, V);
then T.v = T.(0.EMbedding(V)) by ZMODUL05:19;
hence contradiction by A1,FUNCT_2:19;
end;
then not T.v in (0).EMbedding(r, V) by ZMODUL02:66;
then (Omega).EMbedding(r, V) <> (0).EMbedding(r, V);
hence thesis by ZMODUL07:41;
end;
end;
registration
let V be torsion-free Z_Module;
let r be Element of F_Rat;
cluster EMbedding(r, V) -> 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) -> free;
correctness
proof
consider T be linear-transformation of EMbedding(V),EMbedding(r, V)
such that
A1: (for v being Element of Z_MQ_VectSp(V) st v in EMbedding(V)
holds T.v = r*v) &
T is bijective by rSB03A;
thus thesis by A1,ZMODUL06:48;
end;
end;
theorem
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)
proof
let V be non trivial free Z_Module, v be Vector of DivisibleMod(V);
consider ai be Element of INT.Ring such that
A2: ai <> 0 & ai * v in EMbedding(V) by ThDM1;
reconsider aiv = ai * v as Vector of EMbedding(V) by A2;
A3: |. ai .| * v in EMbedding(V)
proof
B1: EMbedding(V) is Submodule of DivisibleMod(V) by ThDivisible2;
per cases by A2;
suppose ai > 0;
hence thesis by A2,ABSVALUE:def 1;
end;
suppose ai < 0;
then |. ai .| * v = (-ai) * v by ABSVALUE:def 1
.= - ai * v by ZMODUL01:16
.= - aiv by B1,ZMODUL01:30;
hence thesis;
end;
end;
reconsider ain = |. ai .| as Element of INT.Ring;
reconsider ainv = ain*v as Vector of EMbedding(V) by A3;
N1: |. ai .| in NAT by COMPLEX1:46,INT_1:3;
then reconsider nai=|. ai .| as Nat;
A4: ain <> 0 by A2,ABSVALUE:2;
defpred P[Nat] means
ex n being Element of INT.Ring
st n = $1 & n in NAT & n <> 0 & n * v in EMbedding(V);
A6: ex k being Nat st P[k] by A3,A4,N1;
ex k being Nat st P[k] & for n being Nat st P[n] holds k <= n
from NAT_1:sch 5(A6);
then consider a0 be Nat such that
A7: P[a0] & for b0 being Nat st P[b0] holds a0 <= b0;
reconsider a=a0 as Element of INT.Ring by INT_1:def 2;
take a;
thus a in NAT by ORDINAL1:def 12;
thus a <> 0 by A7;
thus a * v in EMbedding(V) by A7;
thus for b being Element of INT.Ring
st b in NAT & b < a & b <> 0 holds not b * v in EMbedding(V) by A7;
end;
theorem ThRankEM:
for V being finite-rank free Z_Module holds
rank(EMbedding(V)) = rank(V)
proof
let V be finite-rank free Z_Module;
consider T be linear-transformation of V,EMbedding(V) such that
A1: T is bijective & T = MorphsZQ(V) &
(for v being Vector of V holds T.v = Class(EQRZM(V),[v,1])) by SB03;
thus thesis by A1,ZMODUL06:51;
end;
theorem ThRankrEM1:
for V being finite-rank free Z_Module, r being non zero Element of F_Rat
holds rank(EMbedding(r, V)) = rank(EMbedding(V))
proof
let V be finite-rank free Z_Module, r be non zero Element of F_Rat;
consider T be linear-transformation of EMbedding(V),EMbedding(r,V)
such that
A1: (for v being Element of Z_MQ_VectSp(V) st v in EMbedding(V)
holds T.v = r*v) &
T is bijective by rSB03A;
thus thesis by A1,ZMODUL06:51;
end;
theorem
for V being finite-rank free Z_Module, r being non zero Element of F_Rat
holds rank(EMbedding(r, V)) = rank(V)
proof
let V be finite-rank free Z_Module, r be non zero Element of F_Rat;
thus rank(EMbedding(r, V)) = rank(EMbedding(V)) by ThRankrEM1
.= rank(V) by ThRankEM;
end;
registration
cluster -> infinite for non trivial torsion-free Z_Module;
correctness
proof
let V be non trivial torsion-free Z_Module;
set v = the non zero Vector of V;
defpred P[object, object] means
for i being Element of INT.Ring st i = $1 holds $2 = i*v;
A1: for i being Element of INT.Ring holds
ex w being Element of Lin{v} st P[i, w]
proof
let i be Element of INT.Ring;
set w = i*v;
w in Lin{v} by ZMODUL06:21;
then reconsider w as Element of Lin{v};
take w;
thus thesis;
end;
ex f being Function of INT.Ring,Lin{v} st
for i being Element of INT.Ring holds P[i, f.i] from FUNCT_2:sch 3(A1);
then consider f be Function of INT.Ring,Lin{v} such that
A2: for i being Element of INT.Ring holds P[i, f.i];
A3: dom f = INT & rng f c= the carrier of Lin{v} by FUNCT_2:def 1;
f is one-to-one
proof
for x1, x2 being object st x1 in dom f & x2 in dom f & f.x1 = f.x2
holds x1 = x2
proof
let x1, x2 be object such that
B1: x1 in dom f & x2 in dom f & f.x1 = f.x2;
reconsider xx1 = x1, xx2 = x2 as Element of INT.Ring by B1;
f.x1 = xx1 * v by A2;
then xx1 * v = xx2 * v by A2,B1;
then xx1 * v - xx2 * v = 0.V by RLVECT_1:15;
then (xx1 - xx2) * v = 0.V by ZMODUL01:9;
then xx1 - xx2 = 0.INT.Ring by ZMODUL01:def 7;
hence thesis;
end;
hence thesis by FUNCT_1:def 4;
end;
then A4: card INT c= card Lin{v} by A3,CARD_1:10;
the carrier of Lin{v} is Subset of the carrier of V by VECTSP_4:def 2;
hence thesis by A4;
end;
end;
theorem
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))
proof
let V be Z_Module;
{}(the carrier of V) is linearly-independent;
then consider A be Subset of V such that
A1: {} c= A & A is linearly-independent &
(for v being Vector of V holds ex ai being Element of INT.Ring st
ai <> 0 & ai * v in Lin(A)) by ZMODUL07:2;
A2: 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)
proof
let v be Vector of V;
consider ai be Element of INT.Ring such that
B1: ai <> 0 & ai * v in Lin(A) by A1;
set a = |. ai .|;
B2: a <> 0 by B1,ABSVALUE:2;
N1: a in NAT by COMPLEX1:46,INT_1:3;
a * v in Lin(A)
proof
per cases by B1;
suppose ai > 0;
hence thesis by B1,ABSVALUE:def 1;
end;
suppose ai < 0;
then a = -ai by ABSVALUE:def 1;
then a * v = -ai * v by ZMODUL01:16;
hence thesis by B1,ZMODUL01:38;
end;
end;
hence thesis by N1,B2;
end;
take A;
thus thesis by A1,A2;
end;
theorem
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
proof
let V be non trivial torsion-free Z_Module, v be non zero Vector of V,
A be Subset of V, a be Element of INT.Ring such that
A1: a in NAT & A is linearly-independent & a > 0 & a * v in Lin(A);
a1: a <> 0.INT.Ring by A1;
consider L be Linear_Combination of A such that
A2: a * v = Sum(L) by A1,ZMODUL02:64;
Carrier(L) <> {}
proof
assume Carrier(L) = {};
then Sum(L) = 0.V by ZMODUL02:23;
hence contradiction by a1,A2,ZMODUL01:def 7;
end;
then consider uu be object such that
A3: uu in Carrier(L) by XBOOLE_0:def 1;
consider u be Vector of V such that
A4: u = uu & L.u <> 0 by A3;
A5: Carrier(L) c= A by VECTSP_6:def 4;
take L, u;
thus thesis by A2,A3,A4,A5;
end;
theorem ThDivisible4:
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)
proof
let V be torsion-free Z_Module, i be non zero Integer,
r1, r2 be non zero Element of F_Rat such that
A1: r2 = r1/i;
A2: for x being Vector of DivisibleMod(V) st x in EMbedding(r1, V)
holds x in EMbedding(r2, V)
proof
let x be Vector of DivisibleMod(V) such that
B1: x in EMbedding(r1, V);
consider T1 be linear-transformation of EMbedding(V),EMbedding(r1,V)
such that
B2: (for v being Element of Z_MQ_VectSp(V) st v in EMbedding(V)
holds T1.v = r1*v) & T1 is bijective by rSB03A;
consider T2 be linear-transformation of EMbedding(V),EMbedding(r2,V)
such that
B3: (for v being Element of Z_MQ_VectSp(V) st v in EMbedding(V)
holds T2.v = r2*v) & T2 is bijective by rSB03A;
reconsider ii = i as Element of INT.Ring by INT_1:def 2;
reconsider ir = i as Element of F_Rat by INT_1:def 2,NUMBERS:14;
reconsider iv = 1/i as Element of F_Rat by RAT_1:def 1;
x in rng T1 by B1,B2,FUNCT_2:def 3;
then consider v be object such that
B4: v in the carrier of EMbedding(V) & x = T1.v by FUNCT_2:11;
reconsider vv = v as Vector of Z_MQ_VectSp(V) by B4,SB01;
B5: vv in EMbedding(V) by B4;
then T2.vv = r2*vv by B3;
then reconsider rv = r2*vv as Vector of EMbedding(r2, V) by B4,FUNCT_2:5;
B7: ir*iv = i/i
.= 1.F_Rat by XCMPLX_1:60;
ii*rv = ir*(r2*vv) by rSB01
.= (ir*r2)*vv by VECTSP_1:def 16
.= (r1*(ir*iv))*vv by A1
.= x by B2,B4,B5,B7;
hence thesis;
end;
EMbedding(r1, V) is Submodule of DivisibleMod(V) &
EMbedding(r2, V) is Submodule of DivisibleMod(V) by ThDivisible3;
hence thesis by A2,ZMODUL01:44;
end;
theorem
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)
proof
let V be finite-rank free Z_Module, Z be Submodule of DivisibleMod(V);
hereby
assume AS: Z is finitely-generated;
then reconsider ZX = Z as free Submodule of DivisibleMod(V);
reconsider ZX as finite-rank free Submodule of DivisibleMod(V) by AS;
defpred P[Nat] means
for ZZ being finite-rank free Submodule of DivisibleMod(V)
st rank(ZZ) = $1 holds ex i being non zero Integer,
r being non zero Element of F_Rat
st ZZ is Submodule of EMbedding(r, V) & r = 1/i;
B1: P[0]
proof
let ZZ be finite-rank free Submodule of DivisibleMod(V) such that
C0: rank(ZZ) = 0;
reconsider i = 1 as non zero Integer;
reconsider r = 1/i as Element of F_Rat;
r is non zero;
then reconsider r = 1/i as non zero Element of F_Rat;
C1: EMbedding(r, V) is Submodule of DivisibleMod(V) by ThDivisible3;
C2: (Omega).ZZ = (0).ZZ by C0,ZMODUL05:1
.= (0).(EMbedding(r, V)) by C1,ZMODUL01:52;
take i, r;
ZZ is Submodule of (Omega).ZZ by VECTSP_4:41;
hence thesis by C2,ZMODUL01:42;
end;
B2: for n being Nat st P[n] holds P[n+1]
proof
let n be Nat such that
C1: P[n];
let ZZ be finite-rank free Submodule of DivisibleMod(V) such that
C0: rank(ZZ) = n+1;
set I = the Basis of ZZ;
C2: card(I) = n+1 by C0,ZMODUL03:def 5;
then I <> {};
then consider v be object such that
C3: v in I by XBOOLE_0:def 1;
reconsider v as Vector of ZZ by C3;
C4: ZZ is_the_direct_sum_of Lin(I \ {v}), Lin{v} by C3,ZMODUL04:33;
C5: card(I \ {v}) = card(I) - card{v} by C3,CARD_2:44,ZFMISC_1:31
.= card(I) - 1 by CARD_1:30
.= n by C2;
I is linearly-independent by VECTSP_7:def 3;
then I \ {v} is linearly-independent by XBOOLE_1:36,ZMODUL02:56;
then C6: rank Lin(I \ {v}) = n by C5,ZMODUL05:3;
Lin(I \ {v}) is Submodule of DivisibleMod(V) by ZMODUL01:42;
then consider ix be non zero Integer, rx be non zero Element of F_Rat
such that
C7: Lin(I \ {v}) is Submodule of EMbedding(rx, V) & rx = 1/ix by C1,C6;
ex iy being non zero Integer, ry being non zero Element of F_Rat
st Lin{v} is Submodule of EMbedding(ry, V) & ry = 1/iy
proof
reconsider vv = v as Vector of DivisibleMod(V) by ZMODUL01:25;
consider iiy be Element of INT.Ring such that
D1: iiy <> 0.INT.Ring & iiy * vv in EMbedding(V) by ThDM1;
reconsider iy = iiy as Integer;
reconsider iy as non zero Integer by D1;
reconsider ry = 1/iy as Element of F_Rat by RAT_1:def 1;
ry is non zero;
then reconsider ry as non zero Element of F_Rat;
take iy, ry;
reconsider ivv = iiy*vv as Vector of Z_MQ_VectSp(V) by D1,SB01;
reconsider iv = ivv as Vector of DivisibleMod(V);
consider T be linear-transformation of EMbedding(V),EMbedding(ry,V)
such that
D7: (for v being Element of Z_MQ_VectSp(V) st v in EMbedding(V)
holds T.v = ry*v) & T is bijective by rSB03A;
consider y be Vector of DivisibleMod(V) such that
D8: iv = iiy * y & ry * ivv = (1.INT.Ring) * y by ThDivisibleX2;
T.ivv = ry*ivv by D1,D7
.= y by D8,VECTSP_1:def 17
.= vv by D8,ZMODUL01:10;
then D3: vv in EMbedding(ry, V) by D1,FUNCT_2:5;
D4: EMbedding(ry, V) is Submodule of DivisibleMod(V) by ThDivisible3;
D5: for x being Vector of DivisibleMod(V) st x in Lin{v} holds
x in EMbedding(ry, V)
proof
let x be Vector of DivisibleMod(V) such that
E1: x in Lin{v};
consider a be Element of INT.Ring such that
E2: x = a*v by E1,ZMODUL06:19;
a*vv in EMbedding(ry, V) by D3,D4,ZMODUL01:37;
hence thesis by E2,ZMODUL01:29;
end;
Lin{v} is Submodule of DivisibleMod(V) by ZMODUL01:42;
hence thesis by D4,D5,ZMODUL01:44;
end;
then consider iy be non zero Integer, ry be non zero Element of F_Rat
such that
C8: Lin{v} is Submodule of EMbedding(ry, V) & ry = 1/iy;
reconsider i = ix*iy as non zero Integer;
reconsider r = 1/i as Element of F_Rat by RAT_1:def 1;
r is non zero;
then reconsider r as non zero Element of F_Rat;
take i, r;
r = rx/iy by C7,XCMPLX_1:78;
then EMbedding(rx, V) is Submodule of EMbedding(r, V) by ThDivisible4;
then C9: Lin(I \ {v}) is Submodule of EMbedding(r, V)
by C7,ZMODUL01:42;
r = ry/ix by C8,XCMPLX_1:78;
then EMbedding(ry, V) is Submodule of EMbedding(r, V) by ThDivisible4;
then C13: Lin{v} is Submodule of EMbedding(r, V)
by C8,ZMODUL01:42;
reconsider LIv = Lin(I \ {v}), Lv = Lin{v}
as Submodule of DivisibleMod(V) by ZMODUL01:42;
reconsider EMr = EMbedding(r, V) as Submodule of DivisibleMod(V)
by ThDivisible3;
C11: LIv + Lv is Submodule of EMr by C9,C13,ZMODUL02:76;
C12: (Omega).ZZ is Submodule of EMbedding(r, V)
by C4,C11,ZMODUL06:31;
ZZ is Submodule of (Omega).ZZ by VECTSP_4:41;
hence thesis by C12,ZMODUL01:42;
end;
B3: for n being Nat holds P[n] from NAT_1:sch 2(B1,B2);
set n = rank(ZX);
P[n] by B3;
then consider i be non zero Integer, r be non zero Element of F_Rat
such that
B4: Z is Submodule of EMbedding(r, V) & r = 1/i;
thus ex r being non zero Element of F_Rat
st Z is Submodule of EMbedding(r, V) by B4;
end;
given r be non zero Element of F_Rat such that
B1: Z is Submodule of EMbedding(r, V);
thus Z is finitely-generated by B1;
end;