:: Torsion-part of $\mathbb Z$-module
:: by Yuichi Futa , Hiroyuki Okazaki and Yasunari Shidama
::
:: Received August 14, 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, FINSEQ_1, SUBSET_1, RLVECT_1, STRUCT_0,
PBOOLE, FUNCT_1, RAT_1, XBOOLE_0, ALGSTR_0, RELAT_1, ARYTM_3, CARD_3,
BINOM, RLSUB_2, PRELAMB, XXREAL_0, TARSKI, CARD_1, SUPINF_2, MSSUBFAM,
ARYTM_1, NAT_1, FUNCT_2, FINSET_1, VALUED_1, RLSUB_1, ZFMISC_1, INT_1,
ORDINAL1, RLVECT_2, ZMODUL01, ZMODUL03, ORDERS_1, RLVECT_3, RMOD_2,
RANKNULL, UNIALG_1, MSAFREE2, INT_3, VECTSP_1, XCMPLX_0, MESFUNC1, MOD_3,
MONOID_0, VECTSP10, ZMODUL05, ZMODUL06, ZMODUL07, INT_2,
FUNCSDOM, VECTSP_2;
notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, RELAT_1, FUNCT_1, ORDINAL1,
RELSET_1, PARTFUN1, FUNCT_2, BINOP_1, DOMAIN_1, FINSET_1, ORDERS_1,
INT_2, CARD_1, NUMBERS, XCMPLX_0, XXREAL_0, NAT_1, INT_1, RAT_1,
FINSEQ_1, FINSEQOP, STRUCT_0, ALGSTR_0, RLVECT_1, VECTSP_1, INT_3,
VECTSP_2, VECTSP_4, VECTSP_5, VECTSP_6, VECTSP_7, MOD_2, BINOM, ZMODUL01,
ZMODUL02, VECTSP10, ZMODUL03, GAUSSINT, ZMODUL05, ZMODUL06, RANKNULL;
constructors BINOP_2, BINOM, UPROOTS, ORDERS_1, REALSET1, FINSEQOP, ALGSTR_1,
ZMODUL01, ZMODUL02, EC_PF_1, ZMODUL04, ZMODUL05, ZMODUL06, VECTSP10,
RELSET_1;
registrations SUBSET_1, RELSET_1, FUNCT_2, FINSET_1, XREAL_0, STRUCT_0,
RLVECT_1, MEMBERED, FINSEQ_1, CARD_1, INT_1, XBOOLE_0, ORDINAL1,
XXREAL_0, NAT_1, INT_3, RELAT_1, VECTSP_1, GAUSSINT, RAT_1, XCMPLX_0,
ZMODUL02, ZMODUL03, ZMODUL04, ZMODUL05, ZMODUL06, GRCAT_1, VECTSP_4;
requirements REAL, NUMERALS, BOOLE, SUBSET, ARITHM;
definitions FUNCT_1, TARSKI, FUNCT_2, ALGSTR_0, VECTSP_7;
equalities XCMPLX_0, STRUCT_0, ALGSTR_0, INT_3, GAUSSINT, VECTSP_4, VECTSP_6,
ZMODUL02, VECTSP_1, VECTSP10;
expansions TARSKI, STRUCT_0, ALGSTR_0, VECTSP_1, MOD_2, ZMODUL06, VECTSP_4,
VECTSP_7;
theorems BINOP_1, CARD_1, CARD_2, ENUMSET1, SUBSET_1, FINSEQ_1, FUNCT_1,
FUNCT_2, INT_1, NAT_1, RLSUB_2, RLVECT_1, TARSKI, RANKNULL, ZMODUL01,
ZFMISC_1, RELAT_1, GAUSSINT, ZMODUL03, XBOOLE_0, XBOOLE_1,
XCMPLX_1, XREAL_1, XXREAL_0, ORDINAL1, FINSET_1, ORDERS_1, VECTSP_1,
INT_2, ZMODUL02, NAT_D, BINOM, RAT_1, ZMODUL04, RLVECT_3, ZMODUL05,
ZMODUL06, VECTSP_6, VECTSP_4, VECTSP_7, MOD_2, STRUCT_0, VECTSP10, MOD_3,
VECTSP_5;
schemes FUNCT_2, NAT_1, FUNCT_1, XFAMILY;
begin :: 1. Torsion-part of $\mathbb{Z}$-module
reserve x, y, y1, y2 for object;
reserve V for Z_Module;
reserve W, W1, W2 for Submodule of V;
reserve u, v for VECTOR of V;
reserve i, j, k, n for Element of NAT;
theorem LMThFRat31X:
for n being Integer st n <> 0 & n <> -1 & n <> -2
holds not n/(n+1) in INT
proof
let n be Integer;
assume AS: n <> 0 & n <> -1 & n <> -2;
consider m be Nat such that
A0: n = m or n = - m by INT_1:2;
per cases by A0;
suppose n = m;
hence not n/(n+1) in INT by AS,NAT_1:16,NAT_D:33;
end;
suppose D1: n = -m;
then
D2: n/(n+1) = (-m)/(-(m-1))
.= m /(m-1) by XCMPLX_1:191
.= (m-1)/(m-1) + 1/(m-1);
D32: m <> 0 & m <> 1 & m <> 2 by D1,AS;
then 1 <= m by NAT_1:14;
then 1 < m by AS,D1,XXREAL_0:1;
then 1+1 <= m by NAT_1:13;
then 2 < m by AS,D1,XXREAL_0:1;
then 2+1 <= m by NAT_1:13;
then D3: 2+1 -1 <= m-1 by XREAL_1:9;
then
D31: 1 < m -1 & m-1 <> 0 by XXREAL_0:2;
D4: n/(n+1) = 1 + 1/(m-1) by D2,D3,XCMPLX_1:60;
thus not n/(n+1) in INT
proof
assume n/(n+1) in INT;
then reconsider k = n/(n+1) as Integer;
D5: k-1 = 1/(m-1) by D4;
reconsider j = m-1 as Nat by D32;
not 1/j is Integer by D31,NAT_D:33;
hence contradiction by D5;
end;
end;
end;
registration
cluster prime non zero for Element of INT.Ring;
existence
proof
reconsider p = 2 as Element of INT.Ring by INT_1:def 2;
p <> 0.INT.Ring;
hence thesis by STRUCT_0:def 12,INT_2:28;
end;
end;
registration
cluster prime -> non zero for Element of INT.Ring;
coherence;
end;
LmDOMRNG:
for V, W being non empty 1-sorted, T being Function of V,W holds
dom T = [#]V & rng T c= [#]W
proof
let V, W be non empty 1-sorted, T be Function of V,W;
T is Element of Funcs([#]V,[#]W) by FUNCT_2:8;
hence thesis by FUNCT_2:92;
end;
theorem LmTF1:
for V being Z_Module, A being Subset of V
st A is linearly-independent
ex B being Subset of V st A c= B & B is linearly-independent &
(for v being VECTOR of V holds ex a being Element of INT.Ring
st a <> 0 & a * v in Lin(B))
proof
let V be Z_Module, A be Subset of V such that
A1: A is linearly-independent;
defpred P[set] means ex B being Subset of V st B = $1 & A c= B & B is
linearly-independent;
consider Q be set such that
A2: for Z being set holds Z in Q iff Z in bool(the carrier of V) & P[Z]
from XFAMILY:sch 1;
A3: now
let Z be set;
assume that
A4: Z <> {} and
A5: Z c= Q and
A6: Z is c=-linear;
set W = union Z;
W c= the carrier of V
proof
let x be object;
assume x in W;
then consider X be set such that
A7: x in X and
A8: X in Z by TARSKI:def 4;
X in bool(the carrier of V) by A2,A5,A8;
hence thesis by A7;
end;
then reconsider W as Subset of V;
A9: W is linearly-independent
proof
deffunc Q(object)={C where C is Subset of V: $1 in C & C in Z};
let l be Linear_Combination of W;
assume that
A10: Sum(l) = 0.V and
A11: Carrier(l) <> {};
consider f be Function such that
A12: dom f = Carrier(l) and
A13: for x being object st x in Carrier(l) holds f.x = Q(x)
from FUNCT_1:sch 3;
reconsider M = rng f as non empty set by A11,A12,RELAT_1:42;
set F = the Choice_Function of M;
set S = rng F;
A14:
now
assume {} in M;
then consider x be object such that
A15: x in dom f and
A16: f.x = {} by FUNCT_1:def 3;
Carrier(l) c= W by VECTSP_6:def 4;
then consider X be set such that
A17: x in X and
A18: X in Z by A12,A15,TARSKI:def 4;
reconsider X as Subset of V by A2,A5,A18;
X in {C where C is Subset of V: x in C & C in Z} by A17,A18;
hence contradiction by A12,A13,A15,A16;
end;
then
A19: dom F = M by RLVECT_3:28;
then dom F is finite by A12,FINSET_1:8;
then
A20: S is finite by FINSET_1:8;
A21:
now
let X be set;
assume X in S;
then consider x be object such that
A22: x in dom F and
A23: F.x = X by FUNCT_1:def 3;
consider y be object such that
A24: y in dom f & f.y = x by A22,FUNCT_1:def 3;
reconsider x as set by TARSKI:1;
A25: x = Q(y) by A12,A13,A24;
X in x by A14,A22,A23,ORDERS_1:89;
then ex C being Subset of V st C = X & y in C & C in Z by A25;
hence X in Z;
end;
A26:
now
let X,Y be set;
assume X in S & Y in S;
then X in Z & Y in Z by A21;
hence X c= Y or Y c= X by A6,ORDINAL1:def 8,XBOOLE_0:def 9;
end;
S <> {} by A19,RELAT_1:42;
then union S in Z by A20,A21,A26,CARD_2:62;
then consider B be Subset of V such that
A27: B = union S and
A c= B and
A28: B is linearly-independent by A2,A5;
Carrier(l) c= union S
proof
let x be object;
set X = f.x;
assume A29: x in Carrier(l);
then
A30: f.x = {C where C is Subset of V: x in C & C in Z} by A13;
A31: f.x in M by A12,A29,FUNCT_1:def 3;
then F.X in X by A14,ORDERS_1:89;
then
A32: ex C being Subset of V st F.X = C & x in C & C in Z by A30;
F.X in S by A19,A31,FUNCT_1:def 3;
hence thesis by A32,TARSKI:def 4;
end;
then l is Linear_Combination of B by A27,VECTSP_6:def 4;
hence thesis by A10,A11,A28;
end;
set x = the Element of Z;
x in Q by A4,A5;
then
A33: ex B being Subset of V st B = x & A c= B & B is linearly-independent
by A2;
x c= W by A4,ZFMISC_1:74;
hence union Z in Q by A2,A9,A33,XBOOLE_1:1;
end;
Q <> {} by A1,A2;
then consider X be set such that
A34: X in Q and
A35: for Z being set st Z in Q & Z <> X holds not X c= Z by A3,ORDERS_1:67;
consider B be Subset of V such that
A36: B = X and
A37: A c= B and
A38: B is linearly-independent by A2,A34;
take B;
thus A c= B & B is linearly-independent by A37,A38;
assume not for v being VECTOR of V holds ex a being Element of INT.Ring
st a <> 0 & a * v in Lin(B);
then consider v be VECTOR of V such that
A39: for a being Element of INT.Ring st a <> 0 holds not a * v in Lin(B);
A40: B \/ {v} is linearly-independent
proof
let l be Linear_Combination of B \/ {v};
assume A41: Sum(l) = 0.V;
now
per cases;
suppose
B1: v in Carrier(l);
reconsider i0 = 0 as Element of INT.Ring;
deffunc G(VECTOR of V)=i0;
deffunc L(VECTOR of V)=l.$1;
consider f be Function of V, INT.Ring such that
A42: f.v = i0 and
A43: for u being VECTOR of V st u <> v holds f.u = L(u)
from FUNCT_2:sch 6;
reconsider f as Element of Funcs(the carrier of V, the carrier of
INT.Ring) by FUNCT_2:8;
now
let u be VECTOR of V;
assume not u in Carrier(l) \ {v};
then not u in Carrier(l) or u in {v} by XBOOLE_0:def 5;
then l.u = 0.INT.Ring & u <> v or u = v by TARSKI:def 1;
hence f.u = 0.INT.Ring by A42,A43;
end;
then reconsider f as Linear_Combination of V by VECTSP_6:def 1;
Carrier(f) c= B
proof
let x be object;
A44: Carrier(l) c= B \/ {v} by VECTSP_6:def 4;
assume x in Carrier(f);
then consider u be VECTOR of V such that
A45: u = x and
A46: f.u <> 0.INT.Ring;
f.u = l.u by A42,A43,A46;
then u in Carrier(l) by A46;
then u in B or u in {v} by A44,XBOOLE_0:def 3;
hence thesis by A42,A45,A46,TARSKI:def 1;
end;
then reconsider f as Linear_Combination of B by VECTSP_6:def 4;
reconsider lv = -l.v as Element of INT.Ring;
consider g be Function of V, INT.Ring such that
A47: g.v = lv and
A48: for u being VECTOR of V st u <> v holds g.u = G(u)
from FUNCT_2:sch 6;
reconsider g as Element of Funcs(the carrier of V, the carrier of
INT.Ring) by FUNCT_2:8;
now
let u be VECTOR of V;
assume not u in {v};
then u <> v by TARSKI:def 1;
hence g.u = 0.INT.Ring by A48;
end;
then reconsider g as Linear_Combination of V by VECTSP_6:def 1;
Carrier(g) c= {v}
proof
let x be object;
assume x in Carrier(g);
then ex u being VECTOR of V st x = u & g.u <> 0.INT.Ring;
then x = v by A48;
hence thesis by TARSKI:def 1;
end;
then reconsider g as Linear_Combination of {v} by VECTSP_6:def 4;
f - g = l
proof
let u be VECTOR of V;
now
per cases;
suppose
A50: v = u;
thus (f - g).u = f.u - g.u by ZMODUL02:39
.= l.u by A42,A47,A50;
end;
suppose
A51: v <> u;
thus (f - g).u = f.u - g.u by ZMODUL02:39
.= l.u - g.u by A43,A51
.= l.u - 0 by A48,A51
.= l.u;
end;
end;
hence thesis;
end;
then 0.V = Sum(f) - Sum(g) by A41,ZMODUL02:55;
then B2: Sum(f) = 0.V + Sum(g) by RLSUB_2:61
.= (- l.v) * v by A47,ZMODUL02:21;
-l.v <> 0 by B1,ZMODUL02:8;
hence thesis by A39,B2,ZMODUL02:64;
end;
suppose
A52: not v in Carrier(l);
Carrier(l) c= B
proof
let x be object;
assume
A53: x in Carrier(l);
Carrier(l) c= B \/ {v} by VECTSP_6:def 4;
then x in B or x in {v} by A53,XBOOLE_0:def 3;
hence thesis by A52,A53,TARSKI:def 1;
end;
then l is Linear_Combination of B by VECTSP_6:def 4;
hence thesis by A38,A41;
end;
end;
hence thesis;
end;
v in {v} by TARSKI:def 1;
then
A54: v in B \/ {v} by XBOOLE_0:def 3;
not (1.INT.Ring) * v in Lin(B) by A39;
then not v in Lin(B);
then A55: not v in B by ZMODUL02:65;
B c= B \/ {v} by XBOOLE_1:7;
then B \/ {v} in Q by A2,A37,A40,XBOOLE_1:1;
hence contradiction by A35,A36,A54,A55,XBOOLE_1:7;
end;
theorem LmTF1C:
for V being Z_Module, I being finite Subset of V, W being Submodule of V
st for v being VECTOR of V st v in I holds
ex a being Element of INT.Ring st a <> 0.INT.Ring & a*v in W
ex a being Element of INT.Ring st a <> 0.INT.Ring
& for v being VECTOR of V st v in I holds a*v in W
proof
let V be Z_Module, I be finite Subset of V, W be Submodule of V;
defpred P[Nat] means
for I being finite Subset of V st card I = $1
& for v being VECTOR of V st v in I holds
ex a being Element of INT.Ring st a <> 0.INT.Ring & a*v in W
holds
ex a being Element of INT.Ring st a <> 0.INT.Ring
& for v being VECTOR of V st v in I holds a*v in W;
P1: P[0]
proof
let I be finite Subset of V;
assume that
A0: card I = 0 and
for v being VECTOR of V
st v in I holds ex a being Element of INT.Ring st a <> 0.INT.Ring &
a*v in W;
reconsider a = 1.INT.Ring as Element of INT.Ring;
take a;
thus a <> 0.INT.Ring;
thus for v being VECTOR of V st v in I holds a*v in W by A0;
end;
P2: for n being Nat st P[n] holds P[n+1]
proof
let n be Nat such that
B1: P[n];
let I be finite Subset of V;
assume that
A0: card I = n+1 and
A1: for v being VECTOR of V
st v in I holds ex a being Element of INT.Ring st a <> 0.INT.Ring &
a*v in W;
I is non empty by A0;
then consider u be object such that
B3: u in I by XBOOLE_0:def 1;
reconsider u as VECTOR of V by B3;
set Iu = I \ {u};
{u} is Subset of I by B3,SUBSET_1:41;
then B6: card(Iu) = n+1 - card({u}) by A0,CARD_2:44
.= n+1 - 1 by CARD_1:30
.= n;
reconsider Iu as finite Subset of V;
for v being VECTOR of V
st v in Iu holds ex a being Element of INT.Ring st a <> 0.INT.Ring &
a*v in W
proof
let v be VECTOR of V;
assume v in Iu;
then v in I & not v in {u} by XBOOLE_0:def 5;
hence thesis by A1;
end;
then consider b be Element of INT.Ring such that
A3: b <> 0.INT.Ring and
A4: for v being VECTOR of V
st v in Iu holds b*v in W by B1,B6;
consider au be Element of INT.Ring such that
A5: au <> 0.INT.Ring and
A6: au*u in W by A1,B3;
set a = au*b;
take a;
thus a <> 0.INT.Ring by A3,A5;
thus for v being VECTOR of V st v in I holds a*v in W
proof
let v be VECTOR of V;
assume D1: v in I;
per cases;
suppose v = u; then
a*v = (b*au)*u .= b*(au*u) by VECTSP_1:def 16;
hence a*v in W by A6,ZMODUL01:37;
end;
suppose v <> u;
then D3: b*v in W by A4,D1,ZFMISC_1:56;
a*v = au*(b*v) by VECTSP_1:def 16;
hence a*v in W by D3,ZMODUL01:37;
end;
end;
end;
X1: for n being Nat holds P[n] from NAT_1:sch 2(P1,P2);
assume
X2: for v being VECTOR of V
st v in I holds ex a being Element of INT.Ring st a <> 0.INT.Ring &
a*v in W;
card I is Nat;
hence thesis by X1,X2;
end;
LmTF1B:
for V being Z_Module, I being finite Subset of V, W being Submodule of V,
a being Element of INT.Ring st a <> 0.INT.Ring
& for v being VECTOR of V st v in I holds a*v in W
holds for v being VECTOR of V st v in Lin(I) holds a * v in W
proof
let V be Z_Module, I be finite Subset of V, W be Submodule of V,
a be Element of INT.Ring;
assume that a <> 0.INT.Ring and
AS2: for v being VECTOR of V st v in I holds a*v in W;
defpred P[Nat] means
for I being finite Subset of V st card I = $1
& for v being VECTOR of V st v in I holds a*v in W
holds for v being VECTOR of V st v in Lin(I) holds a * v in W;
P1: P[0]
proof
let I be finite Subset of V;
assume that
A0: card I = 0 and
for v being VECTOR of V st v in I holds a*v in W;
I = {}(the carrier of V) by A0; then
P1: Lin(I) = (0).V by ZMODUL02:67;
thus for v being VECTOR of V st v in Lin(I) holds a*v in W
proof
let v be VECTOR of V;
assume v in Lin(I);
then v in {0.V} by P1,VECTSP_4:def 3;
then v = 0.V by TARSKI:def 1;
then a*v = 0.V by ZMODUL01:1
.= 0.W by ZMODUL01:26;
hence a*v in W;
end;
end;
P2: for n being Nat st P[n] holds P[n+1]
proof
let n be Nat such that
B1: P[n];
let I be finite Subset of V;
assume that
A0: card I = n+1
and
A1: for v being VECTOR of V st v in I holds a*v in W;
I is non empty by A0;
then consider u be object such that
B3: u in I by XBOOLE_0:def 1;
reconsider u as VECTOR of V by B3;
set Iu = I \ {u};
{u} is Subset of I by B3,SUBSET_1:41;
then B6: card(Iu) = n+1 - card({u}) by A0,CARD_2:44
.= n+1 - 1 by CARD_1:30
.= n;
reconsider Iu as finite Subset of V;
set Ku = {u};
E1: I = Iu \/ Ku by B3,XBOOLE_1:45,ZFMISC_1:31;
E3: Lin(I) = Lin(Iu) + Lin(Ku) by E1,ZMODUL02:72;
A4: for v being VECTOR of V st v in Iu holds a*v in W
proof
let v be VECTOR of V;
assume v in Iu;
then v in I & not v in {u} by XBOOLE_0:def 5;
hence thesis by A1;
end;
thus for v being VECTOR of V st v in Lin(I) holds a*v in W
proof
let v be VECTOR of V;
assume v in Lin(I);
then consider v1, v2 be VECTOR of V such that
F1: v1 in Lin(Iu) and
F2: v2 in Lin(Ku) and
F3: v = v1+v2 by E3,ZMODUL01:92;
F4: a*v1 in W by F1,A4,B1,B6;
consider i be Element of INT.Ring such that
F5: v2 = i*u by F2,ZMODUL06:19;
F6: a*v2 = (a*i)*u by F5,VECTSP_1:def 16
.= (i*a)*u
.= i*(a*u) by VECTSP_1:def 16;
F7: a*v2 in W by A1,B3,F6,ZMODUL01:37;
a*v = a*(v1+v2) = a*v1 + a*v2 by F3,VECTSP_1:def 14;
hence a*v in W by ZMODUL01:36,F7,F4;
end;
end;
X1: for n being Nat holds P[n] from NAT_1:sch 2(P1,P2);
card I is Nat;
hence thesis by X1,AS2;
end;
theorem LmTF1D:
for V being finite-rank free Z_Module,
I being linearly-independent Subset of V
holds I is finite
proof
let V be finite-rank free Z_Module, I be linearly-independent Subset of V;
set IV = the Basis of V;
card(I) c= card(IV) by ZMODUL04:20;
hence thesis;
end;
registration
let V be finite-rank free Z_Module;
cluster linearly-independent -> finite for Subset of V;
coherence by LmTF1D;
end;
LmTF1A:
for V being finite-rank free Z_Module,
A being Subset of V
st A is linearly-independent
ex B being finite Subset of V,
a being Element of INT.Ring
st a <> 0.INT.Ring & A c= B & B is linearly-independent &
for v being VECTOR of V holds a * v in Lin(B)
proof
let V be finite-rank free Z_Module, A be Subset of V;
assume A is linearly-independent;
then consider B be Subset of V such that
P1: A c= B and
P2: B is linearly-independent and
P3: for v being VECTOR of V holds ex a being Element of INT.Ring
st a <> 0.INT.Ring & a * v in Lin(B) by LmTF1;
reconsider B as finite Subset of V by P2;
consider I be finite Subset of V such that
A1: I is Basis of V by ZMODUL03:def 3;
A2: I is linearly-independent & Lin(I) = (Omega).V by A1,VECTSP_7:def 3;
for v being VECTOR of V
st v in I holds ex a being Element of INT.Ring st
a <> 0.INT.Ring & a*v in Lin(B) by P3; then
consider a be Element of INT.Ring such that
B1: a <> 0.INT.Ring and
B2: for v being VECTOR of V
st v in I holds a*v in Lin(B) by LmTF1C;
take B, a;
thus a <> 0.INT.Ring & A c= B & B is linearly-independent by P1,B1,P2;
thus for v being VECTOR of V holds a * v in Lin(B)
proof
let v be VECTOR of V;
v in (Omega).V;
hence thesis by A2,B1,B2,LmTF1B;
end;
end;
theorem LmRankSX11:
for V being finite-rank free Z_Module,
A being linearly-independent Subset of V holds
ex I being finite linearly-independent Subset of V,
a being Element of INT.Ring
st a <> 0.INT.Ring & A c= I & a (*) V is Submodule of Lin(I)
proof
let V be finite-rank free Z_Module,
A be linearly-independent Subset of V;
consider I be finite Subset of V, a be Element of INT.Ring such that
P0: a <> 0.INT.Ring and
P1: A c= I and
P2: I is linearly-independent and
P3: for v being VECTOR of V holds a * v in Lin(I) by LmTF1A;
reconsider I as finite linearly-independent Subset of V by P2;
take I, a;
thus a <> 0.INT.Ring & A c= I by P0,P1;
for v being VECTOR of V st v in a (*) V holds v in Lin(I)
proof
let v be VECTOR of V;
assume v in a (*) V;
then consider w be VECTOR of V such that
P4: v = a * w;
thus v in Lin(I) by P3,P4;
end;
hence a (*) V is Submodule of Lin(I) by ZMODUL01:44;
end;
theorem LmRankSX1:
for V being finite-rank free Z_Module,
A being linearly-independent Subset of V holds
ex I being finite linearly-independent Subset of V
st A c= I & rank(V) = card(I)
proof
let V be finite-rank free Z_Module,
A be linearly-independent Subset of V;
consider I be finite linearly-independent Subset of V,
a be Element of INT.Ring such that
A1: a <> 0 & A c= I & a (*) V is Submodule of Lin(I) by LmRankSX11;
take I;
A3: V is finite-rank free Submodule of V by ZMODUL01:32;
rank (a (*) V) <= rank Lin(I) by A1,ZMODUL05:2;
then
A2: rank (V) <= rank Lin(I) by A1,A3,ZMODUL06:52;
rank (Lin(I)) <= rank (V) by ZMODUL05:2;
then rank (Lin(I)) = rank (V) by A2,XXREAL_0:1;
hence thesis by A1,ZMODUL05:3;
end;
theorem LmRankSX2:
for V being torsion-free Z_Module,
W1, W2 being finite-rank free Submodule of V,
I1 being Basis of W1 holds
ex I being finite linearly-independent Subset of V
st I is Subset of W1 + W2 & I1 c= I
& rank(W1 + W2) = rank(Lin(I))
proof
let V be torsion-free Z_Module,
W1, W2 be finite-rank free Submodule of V,
I1 be Basis of W1;
A2: W1 is Submodule of W1 + W2 by ZMODUL01:97;
then I1 c= the carrier of W1 & the carrier of W1 c= the carrier of W1 + W2
by VECTSP_4:def 2;
then I1 c= the carrier of W1 + W2;
then reconsider II1 = I1 as Subset of W1 + W2;
reconsider II1 as finite Subset of W1 + W2;
reconsider II1 as finite linearly-independent Subset of W1 + W2
by A2,VECTSP_7:def 3,ZMODUL03:15;
consider II be finite linearly-independent Subset of W1 + W2 such that
A3: II1 c= II & rank(W1 + W2) = card(II) by LmRankSX1;
II c= the carrier of W1 + W2 & the carrier of W1 + W2 c= the carrier of V
by VECTSP_4:def 2;
then reconsider I = II as Subset of V by XBOOLE_1:1;
reconsider I as finite linearly-independent Subset of V by ZMODUL03:15;
rank(W1 + W2) = rank(Lin(I)) by A3,ZMODUL05:3;
hence thesis by A3;
end;
theorem
for V being torsion-free Z_Module,
W1, W2 being finite-rank free Submodule of V
st W2 is Submodule of W1 holds
ex W3 being finite-rank free Submodule of V
st rank(W1) = rank(W2) + rank(W3) & W2 /\ W3 = (0).V
& W3 is Submodule of W1
proof
let V be torsion-free Z_Module,
W1, W2 be finite-rank free Submodule of V such that
A0: W2 is Submodule of W1;
set III2 = the Basis of W2;
III2 c= the carrier of W2 & the carrier of W2 c= the carrier of W1
by A0,VECTSP_4:def 2;
then reconsider II2 = III2 as Subset of W1 by XBOOLE_1:1;
reconsider II2 as finite linearly-independent Subset of W1
by A0,VECTSP_7:def 3,ZMODUL03:15;
consider II1 be finite linearly-independent Subset of W1 such that
A1: II2 c= II1 & rank(W1) = card(II1) by LmRankSX1;
II1 c= the carrier of W1 & the carrier of W1 c= the carrier of V
by VECTSP_4:def 2;
then II1 c= the carrier of V;
then reconsider I1 = II1 as Subset of V;
reconsider I1 as finite Subset of V;
reconsider I1 as finite linearly-independent Subset of V by ZMODUL03:15;
set II3 = II1 \ II2;
II2 c= the carrier of W1 & the carrier of W1 c= the carrier of V
by VECTSP_4:def 2;
then II2 c= the carrier of V;
then reconsider I2 = II2 as Subset of V;
reconsider I2 as finite Subset of V;
reconsider I2 as finite linearly-independent Subset of V by ZMODUL03:15;
II3 c= the carrier of W1 & the carrier of W1 c= the carrier of V
by VECTSP_4:def 2;
then II3 c= the carrier of V;
then reconsider I3 = II3 as Subset of V;
II3 is linearly-independent by XBOOLE_1:36,ZMODUL02:56;
then reconsider I3 as linearly-independent Subset of V by ZMODUL03:15;
reconsider I3 as finite linearly-independent Subset of V;
A3: W2 /\ Lin(I3) = (0).V
proof
B1: (Omega).W2 = Lin(III2) by VECTSP_7:def 3
.= Lin(I2) by ZMODUL03:20;
reconsider W2s = (Omega).W2 as finite-rank free Submodule of V
by ZMODUL01:42;
(Omega).Lin(I3) = Lin(I3);
then B2: W2 /\ Lin(I3) = Lin(I2) /\ Lin(I3) by B1,ZMODUL04:23;
I2 c= I1 & I3 = I1 \ I2 by A1;
hence W2 /\ Lin(I3) = (0).V by B2,ZMODUL06:4;
end;
card(II3) = card(II1) - card(II2) by A1,CARD_2:44
.= rank(W1) - rank(W2) by A1,ZMODUL03:def 5;
then A6: rank(Lin(I3)) = rank(W1) - rank(W2) by ZMODUL05:3;
A11: Lin(I3) is Submodule of Lin(I1) by XBOOLE_1:36,ZMODUL02:70;
Lin(II1) is Submodule of W1;
then A7: Lin(I1) is Submodule of W1 by ZMODUL03:20;
take Lin(I3);
thus thesis by A3,A6,A7,A11,ZMODUL01:42;
end;
theorem
for V being torsion-free Z_Module,
W1, W2 being finite-rank free Submodule of V holds
ex W3 being finite-rank free Submodule of V
st rank(W1 + W2) = rank(W1) + rank(W3) & W1 /\ W3 = (0).V
& W3 is Submodule of W1 + W2
proof
let V be torsion-free Z_Module,
W1, W2 be finite-rank free Submodule of V;
set I1 = the Basis of W1;
consider I be finite linearly-independent Subset of V such that
A1: I is Subset of W1 + W2 & I1 c= I
& rank(W1 + W2) = rank(Lin(I)) by LmRankSX2;
set I2 = I \ I1;
I1 c= the carrier of W1 & the carrier of W1 c= the carrier of V
by VECTSP_4:def 2;
then I1 c= the carrier of V;
then reconsider II1 = I1 as Subset of V;
reconsider II1 as finite Subset of V;
A10: II1 is linearly-independent by VECTSP_7:def 3,ZMODUL03:15;
reconsider II2 = I2 as finite linearly-independent Subset of V
by XBOOLE_1:36,ZMODUL02:56;
A3: W1 /\ Lin(II2) = (0).V
proof
B1: (Omega).W1 = Lin(I1) by VECTSP_7:def 3
.= Lin(II1) by ZMODUL03:20;
reconsider W1s = (Omega).W1 as finite-rank free Submodule of V
by ZMODUL01:42;
(Omega).Lin(II2) = Lin(II2);
then W1 /\ Lin(II2) = Lin(II1) /\ Lin(II2) by B1,ZMODUL04:23;
hence thesis by A1,A10,ZMODUL06:4;
end;
A4: card(I) = rank(W1 + W2) by A1,ZMODUL05:3;
card(II2) = card(I) - card(I1) by A1,CARD_2:44
.= rank(W1 + W2) - rank(W1) by A4,ZMODUL03:def 5;
then A6: rank(Lin(II2)) = rank(W1 + W2) - rank(W1) by ZMODUL05:3;
A11: Lin(II2) is Submodule of Lin(I) by XBOOLE_1:36,ZMODUL02:70;
reconsider II = I as Subset of W1 + W2 by A1;
Lin(II) is Submodule of W1 + W2;
then A7: Lin(I) is Submodule of W1 + W2 by ZMODUL03:20;
take Lin(II2);
thus thesis by A3,A6,A7,A11,ZMODUL01:42;
end;
theorem
for V being finite-rank free Z_Module, W1, W2 being Submodule of V holds
rank(W1 /\ W2) >= rank W1 + rank W2 - rank V
proof
let V be finite-rank free Z_Module, W1, W2 be Submodule of V;
A1: rank(W1 + W2) <= rank V &
rank V + (rank(W1 /\ W2) - rank V) = rank(W1 /\ W2) by ZMODUL05:2;
rank W1 + rank W2 - rank V = rank(W1 + W2) + rank(W1 /\ W2) - rank V
by ZMODUL06:62
.= rank(W1 + W2) + (rank(W1 /\ W2) - rank V);
hence thesis by A1,XREAL_1:6;
end;
definition
let V be LeftMod of INT.Ring;
func torsion_part(V) -> strict Subspace of V means
:defTorsionPart:
the carrier of it = { v where v is Vector of V : v is torsion };
existence
proof
set X = {v where v is Vector of V : v is torsion };
A1: for x being object st x in X holds x in the carrier of V
proof
let x be object such that
B1: x in X;
consider y be Vector of V such that
B2: y = x & y is torsion by B1;
thus x in the carrier of V by B2;
end;
A2: for x being Vector of V st x in X holds x is torsion
proof
let x be Vector of V such that
B1: x in X;
consider y be Vector of V such that
B2: y = x & y is torsion by B1;
thus thesis by B2;
end;
X c= the carrier of V by A1;
then reconsider X as Subset of V;
A4: for v, u being Vector of V st v in X & u in X holds v + u in X
proof
let v, u be Vector of V such that
B1: v in X & u in X;
v is torsion & u is torsion by A2,B1;
then v + u is torsion by ZMODUL06:5;
hence thesis;
end;
for i being Element of INT.Ring,
v being Vector of V st v in X holds i*v in X
proof
let i be Element of INT.Ring, v be Vector of V such that
B1: v in X;
i*v is torsion by A2,B1,ZMODUL06:8;
hence thesis;
end;
then A6: X is linearly-closed by A4;
0.V in X;
then reconsider X as non empty Subset of V;
consider W be strict Subspace of V such that
A7: X = the carrier of W by A6,ZMODUL01:50;
take W;
thus thesis by A7;
end;
uniqueness by ZMODUL01:45;
end;
theorem LmTP1:
for V being Z_Module, v being Vector of V holds
v is torsion iff v in torsion_part(V)
proof
let V be Z_Module, v be Vector of V;
set W = torsion_part(V);
hereby
assume v is torsion;
then v in { v where v is Vector of V : v is torsion };
hence v in W by defTorsionPart;
end;
assume v in W;
then v in { v where v is Vector of V : v is torsion } by defTorsionPart;
then consider vv be Vector of V such that
A2: vv = v & vv is torsion;
thus v is torsion by A2;
end;
theorem
for V being Z_Module holds
V is torsion-free iff torsion_part(V) = (0).V
proof
let V be Z_Module;
set W = torsion_part(V);
hereby
assume A1: V is torsion-free;
for x being object holds x in the carrier of W implies x in {0.V}
proof
let x be object;
assume B11: x in the carrier of W;
then B1: x in W;
reconsider xx = x as VECTOR of V by B11,ZMODUL01:25;
xx is torsion by B1,LmTP1;
then x = 0.V by A1;
hence x in {0.V} by TARSKI:def 1;
end;
then A3: the carrier of W c= {0.V};
0.V in W by ZMODUL01:33;
then {0.V} c= the carrier of W by ZFMISC_1:31;
hence W = (0).V by A3,XBOOLE_0:def 10,VECTSP_4:def 3;
end;
assume W = (0).V;
then A2: the carrier of W = {0.V} by VECTSP_4:def 3;
for v being VECTOR of V holds
v is torsion implies v = 0.V
proof
let v be VECTOR of V;
assume v is torsion;
then v in W by LmTP1;
hence v = 0.V by A2,TARSKI:def 1;
end;
hence V is torsion-free;
end;
ThTF1:
for V being Z_Module holds VectQuot(V,torsion_part(V)) is torsion-free
proof
let V be Z_Module;
set W = torsion_part(V);
set ZQ = VectQuot(V,W);
for v being Vector of ZQ st v <> 0.ZQ holds not v is torsion
proof
let v be Vector of ZQ;
assume AS: v <> 0.ZQ;
assume v is torsion;
then consider i be Element of INT.Ring such that
P1: i <> 0 & i*v = 0.ZQ;
P3: v is Element of CosetSet(V,W) by VECTSP10:def 6;
then v in CosetSet(V,W);
then ex A being Coset of W st v = A;
then consider a be VECTOR of V such that
A3: v = a+W by VECTSP_4:def 6;
A4: i*v = (lmultCoset(V,W) ).(i,v) by VECTSP10:def 6
.=i*a +W by VECTSP10:def 5,A3,P3;
i*v = zeroCoset(V,W) by P1,VECTSP10:def 6
.= the carrier of W;
then i*a in W by ZMODUL01:63,A4;
then i*a in { v where v is VECTOR of V : v is torsion }
by defTorsionPart;
then ex w being VECTOR of V st i*a=w & w is torsion;
then consider j be Element of INT.Ring such that
A5: j <> 0 & j*(i*a) = 0.V;
(j*i)*a = 0.V by A5,VECTSP_1:def 16;
then a is torsion by A5,P1;
then a in { v where v is VECTOR of V : v is torsion };
then a in W by defTorsionPart;
then v = zeroCoset(V,W) by A3,ZMODUL01:63;
hence contradiction by AS,VECTSP10:def 6;
end;
hence thesis;
end;
registration
let V be Z_Module;
cluster VectQuot(V,torsion_part(V)) -> torsion-free;
coherence by ThTF1;
end;
definition
let R be Ring;
let V be LeftMod of R;
let W be Subspace of V;
func ZQMorph(V, W) -> linear-transformation of V, VectQuot(V,W) means
:defMophVW:
for v being Element of V holds it.v = v + W;
existence
proof
defpred P[Element of V,Element of VectQuot(V,W)] means
$2 = $1+W;
A11: for v being Element of V holds
ex y being Element of VectQuot(V,W) st P[v,y]
proof
let v be Element of V;
reconsider y = v + W as Coset of W by VECTSP_4:def 6;
y in CosetSet(V,W);
then reconsider y as Element of VectQuot(V,W) by VECTSP10:def 6;
take y;
thus thesis;
end;
consider f be Function of V, VectQuot(V,W) such that
A15: for v being Element of V holds P[v,f.v] from FUNCT_2:sch 3(A11);
for x, y being Vector of V holds f.(x+y) = (f.x)+(f.y)
proof
let x, y be Vector of V;
A2: f.x = x+W by A15;
A3: f.y = y+W by A15;
reconsider A = x+W as Element of CosetSet(V,W) by A2,VECTSP10:def 6;
reconsider B = y+W as Element of CosetSet(V,W) by A3,VECTSP10:def 6;
thus f.(x+y) = (x+y)+ W by A15
.= (addCoset(V,W)).(A,B) by VECTSP10:def 3
.= (f.x)+(f.y) by A2,A3,VECTSP10:def 6;
end;
then
A16: f is additive;
for a being Element of R,
x being Element of V holds f.(a*x) = a*(f.x)
proof
let a be Element of R, x be Element of V;
A2: f.x = x+W by A15;
reconsider A = x+W as Element of CosetSet(V,W) by A2,VECTSP10:def 6;
thus f.(a*x) = (a*x) + W by A15
.= (lmultCoset(V,W)).(a,A) by VECTSP10:def 5
.= a*(f.x) by A2,VECTSP10:def 6;
end;
then f is homogeneous;
hence thesis by A15,A16;
end;
uniqueness
proof
let f1, f2 be linear-transformation of V,VectQuot(V,W);
assume AS1:
for v being Element of V holds f1.v = v + W;
assume AS2:
for v being Element of V holds f2.v = v + W;
for v being Element of V holds f1.v = f2.v
proof
let v be Element of V;
thus f1.v = v + W by AS1
.= f2.v by AS2;
end;
hence f1 = f2 by FUNCT_2:def 8;
end;
end;
registration
let R be Ring;
let V be LeftMod of R, W be Subspace of V;
cluster ZQMorph(V,W) -> onto;
coherence
proof
for y being object st y in the carrier of (VectQuot(V,W))
ex x being object st x in the carrier of V & y = (ZQMorph(V,W)).x
proof
let y be object;
assume y in the carrier of (VectQuot(V,W));
then reconsider A = y as Element of CosetSet(V,W) by VECTSP10:def 6;
A in CosetSet(V,W);
then consider A0 be Coset of W such that
P0: A = A0;
consider v be VECTOR of V such that
P1: A0 = v + W by VECTSP_4:def 6;
(ZQMorph(V,W)).v = y by P0,P1,defMophVW;
hence thesis;
end;
then rng (ZQMorph(V,W)) = the carrier of VectQuot(V,W) by FUNCT_2:10;
hence thesis by FUNCT_2:def 3;
end;
end;
theorem
for V, W being Z_Module,
T being linear-transformation of V,W,
s being FinSequence of V,
t being FinSequence of W
st len s = len t & for i being Element of NAT
st i in dom s holds ex si being VECTOR of V
st si = s.i & t.i = T.si holds
Sum(t) = T.(Sum(s))
proof
let V, W be Z_Module,
T be linear-transformation of V,W;
XX: T is additive;
defpred P[Nat] means
for s being FinSequence of V,
t being FinSequence of W
st len s = $1 & len s = len t
& for i being Element of NAT
st i in dom s holds ex si being VECTOR of V
st si = s.i & t.i = T.si
holds Sum(t) = T.(Sum(s));
A1: P[0]
proof
let s be FinSequence of V,
t be FinSequence of W;
assume that A2: len s = 0 & len s = len t and
for i being Element of NAT
st i in dom s holds ex si being VECTOR of V
st si = s.i & t.i = T.si;
s = <*>(the carrier of V) by A2;
then Sum(s) = 0.V by RLVECT_1:43;
then
A3: T.(Sum(s)) = 0.W by ZMODUL05:19;
t = <*>(the carrier of W) by A2;
hence thesis by A3,RLVECT_1:43;
end;
A4: for k being Nat st P[k] holds P[k+1]
proof
let k be Nat;
assume A5: P[k];
now
let s be FinSequence of V,
t be FinSequence of W;
assume that
A6: len s = k+1 & len s = len t and
A7: for i being Element of NAT
st i in dom s holds ex si being VECTOR of V
st si = s.i & t.i = T.si;
reconsider s1 = s | k as FinSequence of V;
A8: dom s = Seg (k+1) by A6,FINSEQ_1:def 3;
A9: dom t = Seg (k+1) by A6,FINSEQ_1:def 3;
A10: len s1 = k by A6,FINSEQ_1:59,NAT_1:11;
A11: dom s1 = Seg (len s1) by FINSEQ_1:def 3
.= Seg k by A6,FINSEQ_1:59,NAT_1:11;
then
A12: s1 = s |dom s1 by FINSEQ_1:def 16;
reconsider t1 = t | k as FinSequence of W;
A13: dom t1 = Seg (len t1) by FINSEQ_1:def 3
.= Seg k by A6,FINSEQ_1:59,NAT_1:11;
then
A14: t1 = t |dom t1 by FINSEQ_1:def 16;
k in NAT by ORDINAL1:def 12;
then
A15: len t1 = k by A13,FINSEQ_1:def 3;
s.(len s) in rng s by A6,A8,FINSEQ_1:4,FUNCT_1:3;
then reconsider vs=s.(len s) as Element of V;
t.(len t) in rng t by A6,A9,FINSEQ_1:4,FUNCT_1:3;
then reconsider vt = t.(len t) as Element of W;
A16: len s1 = k & len s1 = len t1 by A10,A13,FINSEQ_1:def 3;
A17: for i being Element of NAT
st i in dom s1 holds ex si being VECTOR of V
st si = s1.i & t1.i = T.si
proof
let i be Element of NAT;
assume A18: i in dom s1;
Seg k c= Seg (k+1) by FINSEQ_1:5,NAT_1:11;
then consider si be VECTOR of V such that
A19: si = s.i & t.i = T.si by A7,A11,A8,A18;
take si;
thus si = s1.i by A12,A18,A19,FUNCT_1:49;
thus t1.i = T.si by A14,A11,A13,A18,A19,FUNCT_1:49;
end;
A20: Sum(t1) = T.(Sum(s1)) by A5,A16,A17;
A21: len s = len s1 + 1 by A6,FINSEQ_1:59,NAT_1:11;
consider ssi be VECTOR of V such that
A22: ssi = s.(len s) & t.(len s) = T.(ssi) by A6,A7,A8,FINSEQ_1:4;
thus Sum(t) = Sum(t1) + vt by A6,A14,A15,RLVECT_1:38
.= T.(Sum(s1)+vs) by A6,A20,A22,XX
.= T.(Sum(s)) by A12,A21,RLVECT_1:38;
end;
hence P[k+1];
end;
for k being Nat holds P[k] from NAT_1:sch 2(A1,A4);
hence thesis;
end;
registration
let V be finitely-generated Z_Module, W be Submodule of V;
cluster VectQuot(V,W) -> finitely-generated;
coherence
proof
consider A be finite Subset of V such that
A1: Lin(A) = the ModuleStr of V by ZMODUL03:def 4;
set T = ZQMorph(V,W);
reconsider B = T.: A as
finite Subset of VectQuot(V,W);
A2: T.: (the carrier of Lin(A)) c= the carrier of Lin(B) by ZMODUL06:40;
A3: rng T = the carrier of VectQuot(V,W) by FUNCT_2:def 3;
X1: rng T = T.:(dom T) by RELAT_1:113
.= T.: (the carrier of Lin(A)) by A1,FUNCT_2:def 1;
the carrier of Lin(B) c=the carrier of VectQuot(V,W)
by VECTSP_4:def 2;
hence thesis by A2,A3,X1,XBOOLE_0:def 10,ZMODUL01:47;
end;
end;
registration
let V be finitely-generated Z_Module;
cluster VectQuot(V,torsion_part(V)) -> free;
correctness;
end;
begin :: 2. $\mathbb Z$-module generated the rational number field
definition
func Rat-Module -> ModuleStr over INT.Ring equals
ModuleStr (# the carrier of F_Rat, the addF of F_Rat, the ZeroF of F_Rat,
Int-mult-left(F_Rat) #);
coherence;
end;
registration
cluster Rat-Module -> non empty;
coherence;
end;
registration
cluster Rat-Module -> Abelian add-associative
right_zeroed right_complementable scalar-distributive vector-distributive
scalar-associative scalar-unital;
correctness
proof
set ZS = Rat-Module;
reconsider ZS as non empty ModuleStr over INT.Ring;
set AG = the carrier of F_Rat;
set MLI = Int-mult-left(F_Rat);
A1: for v, w being Element of ZS holds v + w = w + v
proof
let v, w be Element of ZS;
reconsider v1 = v, w1 = w as Element of F_Rat;
thus v + w = v1 + w1
.= w1 + v1
.= w + v;
end;
A2: 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 u1 = u, v1 = v, w1 = w as Element of F_Rat;
thus (u + v) + w = u1+v1+w1
.= u1+(v1+w1)
.= u+(v+w);
end;
A5: for v being Element of ZS holds v + 0.ZS = v
proof
let v be Element of ZS;
reconsider v1 = v as Element of F_Rat;
thus v + 0.ZS = v1 + 0.F_Rat
.= v;
end;
A6: for v being Vector of ZS holds v is right_complementable
proof
let v be Vector of ZS;
take (-1.INT.Ring) * v;
reconsider v1 = v as Element of F_Rat;
set i0 = 0.INT.Ring;
set i1 = 1.INT.Ring;
set i2 = -1.INT.Ring;
0.F_Rat = MLI.(i1+i2,v1) by ZMODUL01:152
.= MLI.(i1,v1)+ MLI.(i2,v1) by ZMODUL01:159
.= v+(-1.INT.Ring)*v by ZMODUL01:155;
hence thesis;
end;
A8: for a, b being Element of INT.Ring, v being Vector of ZS
holds (a + b) * v = a * v + b * v
proof
let a, b be Element of INT.Ring;
let v be Vector of ZS;
reconsider a1=a,b1=b as Element of INT.Ring;
reconsider v1=v as Element of F_Rat;
thus (a + b) * v = (MLI.(a1,v1)) + (MLI.(b1,v1)) by ZMODUL01:159
.= a*v + b*v;
end;
for a being Element of INT.Ring, v, w being Vector of ZS
holds a * (v + w) = a * v + a * w
proof
let a be Element of INT.Ring;
let v, w be Vector of ZS;
reconsider a1=a as Element of INT.Ring;
reconsider v1 = v, w1 = w as Element of F_Rat;
thus a * (v+w) = MLI.(a,(v1+w1))
.= MLI.(a1,v1) + MLI.(a1,w1) by ZMODUL01:161
.= a*v + a*w;
end;
hence thesis by A1,A2,A5,A6,A8,ZMODUL01:163,155,
RLVECT_1:def 2,def 3,def 4;
end;
end;
theorem LMTFRat1:
for v being Element of F_Rat,v1 be Rational
st v = v1 holds
for n being Nat holds (Nat-mult-left(F_Rat)).(n,v) = n*v1
proof
let v be Element of F_Rat,v1 be Rational;
assume A1: v = v1;
defpred P[Nat] means
(Nat-mult-left(F_Rat)).($1,v) =$1*v1;
(Nat-mult-left(F_Rat)).(0,v) = 0.F_Rat by BINOM:def 3
.= 0 * v1;
then
X1: P[0];
X2: for n being Nat st P[n] holds P[n+1]
proof
let n be Nat;
assume X22: P[n];
(Nat-mult-left(F_Rat)).(n+1,v) = v + (Nat-mult-left(F_Rat)).(n,v)
by BINOM:def 3
.= v1 + n*v1 by A1,X22
.= (n+1)*v1;
hence thesis;
end;
for n being Nat holds P[n] from NAT_1:sch 2(X1,X2);
hence thesis;
end;
theorem LMTFRat2:
for x being Integer, v being Element of F_Rat, v1 being Rational
st v = v1 holds (Int-mult-left(F_Rat)).(x,v) = x*v1
proof
let x be Integer, v be Element of F_Rat, v1 be Rational;
assume A1: v = v1;
reconsider xx = x as Element of INT.Ring by INT_1:def 2;
per cases;
suppose C1: x >= 0;
then reconsider x0 = x as Element of NAT by INT_1:3;
thus (Int-mult-left(F_Rat)).(x,v) = (Nat-mult-left F_Rat).(xx,v)
by C1,ZMODUL01:def 20
.= x0*v1 by LMTFRat1,A1
.= x*v1;
end;
suppose C2: x < 0;
then reconsider x0 = -x as Element of NAT by INT_1:3;
thus (Int-mult-left(F_Rat)).(x,v)
= (Nat-mult-left F_Rat) . (-xx,-v) by C2,ZMODUL01:def 20
.= x0*(-v1) by A1,LMTFRat1
.= x*v1;
end;
end;
registration
cluster Rat-Module -> torsion-free;
correctness
proof
set V = Rat-Module;
for v being VECTOR of V st v <> 0.V holds not v is torsion
proof
let v be VECTOR of V;
assume AS: v <> 0.V;
assume v is torsion;
then
consider i be Element of INT.Ring such that
P1: i <> 0.INT.Ring & i*v = 0.V;
reconsider v1 = v as Rational;
i*v1 = 0 by LMTFRat2,P1;
hence contradiction by AS,P1;
end;
hence thesis;
end;
end;
registration
cluster Rat-Module -> non trivial;
correctness;
end;
theorem LMThFRat31:
for s being Element of Rat-Module holds Lin{s} <> Rat-Module
proof
set ZS = Rat-Module;
let s be Element of ZS;
assume AS: Lin{s} = ZS;
consider m, n be Integer such that
P2: n > 0 & s = m/n by RAT_1:1;
per cases;
suppose m = 1 or m = -1;
then per cases;
suppose D1: m = 1;
reconsider t = 1 /(n+1) as Element of ZS by RAT_1:def 1;
t in Lin{s} by AS;
then consider l be Linear_Combination of {s} such that
P3: t = Sum(l) by ZMODUL02:64;
P4: Sum(l) = l.s * s by ZMODUL02:21;
reconsider k = l.s as Integer;
P5: 1 /(n+1) = k/n by D1,P2,P3,P4,LMTFRat2;
k = n/(n+1) by P2,P5,XCMPLX_1:87;
hence contradiction by LMThFRat31X,P2;
end;
suppose D2: m = -1;
reconsider t = (-1) /(n+1) as Element of ZS by RAT_1:def 1;
t in Lin{s} by AS;
then consider l be Linear_Combination of {s} such that
P3: t = Sum(l) by ZMODUL02:64;
P4: Sum(l) = l.s * s by ZMODUL02:21;
reconsider k = l.s as Integer;
(-1) /(n+1) = k* (m/n) by P2,P3,P4,LMTFRat2
.= -k/n by D2; then
k = n/(n+1) by P2,XCMPLX_1:87;
hence contradiction by LMThFRat31X,P2;
end;
end;
suppose C2: m <>1 & m <> -1;
reconsider t = (m+1)/n as Element of ZS by RAT_1:def 1;
t in Lin{s} by AS;
then consider l be Linear_Combination of {s} such that
P3: t = Sum(l) by ZMODUL02:64;
P4: Sum(l) = l.s * s by ZMODUL02:21;
reconsider k = l.s as Integer;
P5: (m+1)/n = k* (m/n) by P2,P3,P4,LMTFRat2;
m+1 = (m+1)/n * n by P2,XCMPLX_1:87
.= k* ((m/n) *n) by P5
.= k*m by P2,XCMPLX_1:87;
then m*(k-1) = 1;
hence contradiction by C2,INT_1:9;
end;
end;
theorem LMThFRat32:
for s, t being Element of Rat-Module st s <> t
holds not {s,t} is linearly-independent
proof
set ZS = Rat-Module;
let s, t be Element of ZS;
assume AS: s <> t;
assume P1: {s,t} is linearly-independent;
consider m, n be Integer such that
P2: n > 0 & s = m/n by RAT_1:1;
consider p, q be Integer such that
P3: q > 0 & t = p/q by RAT_1:1;
reconsider b = n*p as Element of INT.Ring by INT_1:def 2;
reconsider a = q*m as Element of INT.Ring by INT_1:def 2;
P4: p <> 0.INT.Ring by AS,P1,P3,ZMODUL02:62;
b * s = (n*p)*(m/n) by LMTFRat2,P2
.= p*m by P2,XCMPLX_1:90
.= (q*m)*(p/q) by P3,XCMPLX_1:90
.= a*t by LMTFRat2,P3;
hence contradiction by AS,P1,P2,P4,ZMODUL02:62;
end;
registration
cluster Rat-Module -> non free;
correctness
proof
set ZS = Rat-Module;
assume ZS is free;
then consider A be Subset of ZS such that
p1: A is base;
per cases;
suppose P2:
not (ex s, t being Element of ZS
st s in A & t in A & s <> t);
A <> {}
proof
assume A = {};
then A = {}(the carrier of ZS);
then Lin(A) = (0).ZS by ZMODUL02:67;
hence contradiction by p1;
end;
then consider s be object such that
P21: s in A by XBOOLE_0:def 1;
reconsider s as Element of ZS by P21;
P23: {s} c= A by ZFMISC_1:31,P21;
now
let z be object;
assume P22: z in A;
then reconsider z0 = z as Element of ZS;
z0 = s by P21,P22,P2;
hence z in {s} by TARSKI:def 1;
end;
then A c= {s};
then A = {s} by P23,XBOOLE_0:def 10;
hence contradiction by p1,LMThFRat31;
end;
suppose ex s, t being Element of ZS
st s in A & t in A & s <> t;
then consider s, t be Element of ZS such that
P4: s in A & t in A & s <> t;
{s,t} c= A by ZFMISC_1:32,P4;
hence contradiction by p1,P4,LMThFRat32,ZMODUL02:56;
end;
end;
end;
theorem
for A being finite Subset of Rat-Module holds
ex n being Integer st n <> 0 &
for s being Element of Rat-Module st s in Lin(A) holds
ex m being Integer st s = m/n
proof
set ZS = Rat-Module;
defpred P[Nat] means
for A being finite Subset of ZS st card A = $1 holds
ex n being Integer st n <> 0 &
for s being Element of ZS st s in Lin(A) holds
ex m being Integer st s = m/n;
P0: P[0]
proof
let A be finite Subset of ZS;
assume card A = 0;
then
P2: A = {}(the carrier of ZS);
P3: the carrier of ((0).ZS) = {0.ZS} by VECTSP_4:def 3;
reconsider n = 1 as Integer;
take n;
thus n <> 0;
let s be Element of ZS;
assume s in Lin(A); then
P4: s in (0).ZS by P2,ZMODUL02:67;
reconsider m = 0 as Integer;
take m;
thus s = m/n by P3,P4,TARSKI:def 1;
end;
P1: for k being Nat st P[k] holds P[k+1]
proof
let k be Nat;
assume P11: P[k];
let A be finite Subset of ZS;
assume B3: card A = k+1;
then A <> {};
then consider v be object such that
B4: v in A by XBOOLE_0:7;
reconsider v as VECTOR of ZS by B4;
set Av = A \ {v};
B6: {v} is Subset of A by B4,SUBSET_1:41;
then card(Av) = k+1 - card({v}) by B3,CARD_2:44
.= k+1 - 1 by CARD_1:30
.= k;
then consider nk be Integer such that
B8: nk <> 0 &
for s being Element of ZS st s in Lin(Av) holds
ex mk being Integer st s = mk/nk by P11;
consider mv, nv be Integer such that
B9: nv > 0 & v = mv/nv by RAT_1:1;
reconsider n = nk*nv as Integer;
take n;
thus n <> 0 by B8,B9;
A = Av \/ {v} by B6,XBOOLE_1:45;
then
B11: Lin(A) = Lin(Av) + Lin({v}) by ZMODUL02:72;
let s be Element of ZS;
assume s in Lin(A);
then consider sk, sv be VECTOR of ZS such that
B12: sk in Lin(Av) & sv in Lin({v}) & s = sk+sv by ZMODUL01:92,B11;
consider mk be Integer such that
B13: sk = mk/nk by B8,B12;
consider l be Linear_Combination of {v} such that
B14: sv = Sum(l) by B12,ZMODUL02:64;
B15: Sum(l) = l.v * v by ZMODUL02:21;
reconsider k = l.v as Integer;
B16: sv = k*(mv/nv) by B9,B14,B15,LMTFRat2;
reconsider m = mk*nv + k*mv*nk as Integer;
take m;
reconsider s1 = mk/nk as Rational;
reconsider ss1= s1 as Element of F_Rat by RAT_1:def 1;
reconsider mn = mv/nv as Rational;
reconsider s2 = k*mn as Rational;
reconsider ss2 = s2 as Element of F_Rat by RAT_1:def 2;
reconsider sss1 = ss1, sss2 = ss2 as Element of F_Real
by TARSKI:def 3,GAUSSINT:13;
XX1: ss1+ss2 = sss1+sss2
.= (mk/nk) + (k*(mv/nv));
thus s = ((mk*nv)/(nk*nv)) + ((k*mv)/nv)
by B9,B12,B13,B16,XX1,XCMPLX_1:91
.= ((mk*nv)/(nk*nv)) + ((k*mv*nk)/(nv*nk)) by B8,XCMPLX_1:91
.= m/n;
end;
P2: for k being Nat holds P[k] from NAT_1:sch 2(P0,P1);
let A be finite Subset of ZS;
card A is Nat;
hence ex n being Integer st n <> 0 &
for s being Element of ZS st s in Lin(A) holds
ex m being Integer st s = m/n by P2;
end;
registration
cluster Rat-Module -> non finitely-generated;
correctness;
end;
theorem
for A being finite Subset of Rat-Module holds
rank(Lin(A)) <= 1
proof
set ZS = Rat-Module;
defpred P[Nat] means
for A being finite Subset of ZS st card(A) = $1 holds rank(Lin(A)) <= 1;
A1: P[0]
proof
let A be finite Subset of ZS such that
B1: card(A) = 0;
A = {}(the carrier of ZS) by B1;
then Lin(A) = (0).ZS by ZMODUL02:67
.= (0).Lin(A) by ZMODUL01:51;
then (Omega).Lin(A) = (0).Lin(A);
hence thesis by ZMODUL05:1;
end;
A2: for n being Nat st P[n] holds P[n+1]
proof
let n be Nat such that
B1: P[n];
let A be finite Subset of ZS such that
B2: card(A) = n + 1;
A <> {} by B2;
then consider x be object such that
B3: x in A by XBOOLE_0:7;
reconsider x as VECTOR of ZS by B3;
B5: card(A \ {x}) = card(A) - card{x} by B3,ZFMISC_1:31,CARD_2:44
.= n+1 - 1 by B2,CARD_1:30
.= n;
B6: Lin(A \ {x}) + Lin{x} = Lin((A \ {x}) \/ {x}) by ZMODUL02:72
.= Lin(A \/ {x}) by XBOOLE_1:39
.= Lin(A) by B3,ZFMISC_1:40;
per cases by B1,B5,NAT_1:25;
suppose rank(Lin(A \ {x})) = 0;
then
C2: (Omega).Lin(A \ {x}) = (0).Lin(A \ {x}) by ZMODUL05:1
.= (0).ZS by ZMODUL01:51;
per cases;
suppose x = 0.ZS;
then Lin{x} = (0).ZS by ZMODUL06:22;
then Lin(A \ {x}) + Lin{x} = (0).ZS by C2,ZMODUL01:99;
then (Omega).Lin(A) = (0).Lin(A) by B6,ZMODUL01:51;
hence thesis by ZMODUL05:1;
end;
suppose D1: x <> 0.ZS;
reconsider Linx = Lin{x} as free Submodule of ZS;
x in Lin(A) by B3,ZMODUL02:65;
then reconsider xx = x as VECTOR of Lin(A);
Lin(A) = Lin{x} by B6,C2,ZMODUL01:99
.= Lin{xx} by ZMODUL03:20;
then D3: (Omega).Lin(A) = Lin{xx};
xx <> 0.Lin(A) by D1,ZMODUL01:26;
hence thesis by D3,ZMODUL05:5;
end;
end;
suppose rank(Lin(A \ {x})) = 1;
then consider axl be VECTOR of Lin(A \ {x}) such that
C2: axl <> 0.Lin(A \ {x}) & (Omega).Lin(A \ {x}) = Lin{axl}
by ZMODUL05:5;
reconsider ax = axl as VECTOR of ZS by ZMODUL01:25;
C3: ax <> 0.ZS by C2,ZMODUL01:26;
C4: Lin(A \ {x}) = Lin{ax} by C2,ZMODUL03:20;
C5: {ax} is linearly-independent by C3,ZMODUL02:59;
per cases;
suppose x = 0.ZS;
then Lin{x} = (0).ZS by ZMODUL06:22;
then Lin(A \ {x}) + Lin{x} = Lin(A \ {x}) by ZMODUL01:99;
hence thesis by B1,B5,B6;
end;
suppose x = ax;
then Lin(A \ {x}) + Lin{x} = Lin(A \ {x}) by C4,ZMODUL01:95;
hence thesis by B1,B5,B6;
end;
suppose D1: x <> 0.ZS & x <> ax;
then D2: {x} is linearly-independent by ZMODUL02:59;
{ax, x} is linearly-dependent by D1,LMThFRat32;
then D3: {ax} \/ {x} is linearly-dependent by ENUMSET1:1;
{ax} /\ {x} = {} by D1,XBOOLE_0:def 7,ZFMISC_1:11;
then D4: Lin{ax} /\ Lin{x} <> (0).ZS by C5,D2,D3,ZMODUL06:23;
consider y be VECTOR of ZS such that
D5: y <> 0.ZS & Lin{ax} + Lin{x} = Lin{y}
by C3,D1,D4,ZMODUL06:28;
D6: y <> 0.Lin(A) by D5,ZMODUL01:26;
y in Lin(A) by B6,C4,D5,ZMODUL06:20;
then reconsider yy = y as VECTOR of Lin(A);
(Omega).Lin(A) = Lin{yy} by B6,C4,D5,ZMODUL03:20;
hence thesis by D6,ZMODUL05:5;
end;
end;
end;
A3: for n being Nat holds P[n] from NAT_1:sch 2(A1,A2);
let A be finite Subset of ZS;
set n = card(A);
P[n] by A3;
hence thesis;
end;
begin :: 3. The rank-nullity theorem
reserve V,W for finite-rank free Z_Module;
reserve T for linear-transformation of V,W;
registration
let W be finite-rank free Z_Module, V be Z_Module;
let T be linear-transformation of V,W;
cluster im T -> finite-rank free;
correctness;
end;
definition
let W be finite-rank free Z_Module;
let V be Z_Module;
let T be linear-transformation of V,W;
func rank(T) -> Nat equals
rank (im T);
coherence;
end;
definition
let V be finite-rank free Z_Module;
let W be Z_Module;
let T be linear-transformation of V,W;
func nullity(T) -> Nat equals
rank (ker T);
coherence;
end;
theorem ZM05Th35:
for V being finite-rank free Z_Module, A being Subset of V,
B being linearly-independent Subset of V,
T being linear-transformation of V,W
st rank(V) = card(B) & A is Basis of ker T & A c= B holds
T | (B \ A) is one-to-one
proof
let V be finite-rank free Z_Module,
A be Subset of V, B be linearly-independent Subset of V,
T be linear-transformation of V,W such that
rank(V) = card(B) and
A1: A is Basis of ker T and
A2: A c= B;
reconsider A9 = A as Subset of V;
set f = T | (B \ A);
let x1, x2 be object such that
A3: x1 in dom f and
A4: x2 in dom f and
A5: f.x1 = f.x2 and
A6: x1 <> x2;
x2 in dom T by A4,RELAT_1:57;
then reconsider x2 as Element of V;
x1 in dom T by A3,RELAT_1:57;
then reconsider x1 as Element of V;
A7: not x1 in (A9 \/ {x2})
proof
assume
A8: x1 in A9 \/ {x2};
per cases by A8,XBOOLE_0:def 3;
suppose
x1 in A9;
hence contradiction by A3,XBOOLE_0:def 5;
end;
suppose
x1 in {x2};
hence contradiction by A6,TARSKI:def 1;
end;
end;
A9: f.x2 = T.x2 by A4,FUNCT_1:49;
reconsider A as Subset of (ker T) by A1;
reconsider A as Basis of (ker T) by A1;
A10: ker T = Lin A by VECTSP_7:def 3;
f.x1 = T.x1 by A3,FUNCT_1:49;
then x1 - x2 in ker T by A5,A9,ZMODUL05:27;
then x1 - x2 in Lin A9 by A10,ZMODUL03:20; then
A11: x1 in Lin (A9 \/ {x2}) by ZMODUL05:28;
{x2} \/ {x1} = {x1,x2} by ENUMSET1:1; then
A12: (A9 \/ {x2}) \/ {x1} = A9 \/ {x1,x2} by XBOOLE_1:4;
{x1,x2} c= B
proof
let z be object such that
A13: z in {x1,x2};
per cases by A13,TARSKI:def 2;
suppose
z = x1;
hence thesis by A3,XBOOLE_0:def 5;
end;
suppose
z = x2;
hence thesis by A4,XBOOLE_0:def 5;
end;
end;
then A9 \/ {x1,x2} c= B by A2,XBOOLE_1:8;
hence thesis by A7,A11,A12,ZMODUL02:56,ZMODUL05:32;
end;
theorem ZM05Th59:
for V being finite-rank free Z_Module,
A being Subset of V,
B being linearly-independent Subset of V,
T being linear-transformation of V,W,
l being Linear_Combination of B \ A
st rank(V) = card(B) & A is Basis of ker T & A c= B
holds T.(Sum l) = Sum(T@*l)
proof
let V be finite-rank free Z_Module,
A be Subset of V, B be linearly-independent Subset of V,
T be linear-transformation of V,W,
l be Linear_Combination of B \ A;
assume rank(V) = card(B) & A is Basis of ker T & A c= B;
then
A1: T | (B \ A) is one-to-one by ZM05Th35;
A2: (T | (B \ A)) | (Carrier l) = T | (Carrier l)
by RELAT_1:74,VECTSP_6:def 4; then
A3: T | (Carrier l) is one-to-one by A1,FUNCT_1:52;
consider G be FinSequence of V such that
A4: G is one-to-one and
A5: rng G = Carrier l and
A6: Sum l = Sum (l (#) G) by VECTSP_6:def 6;
set H = T*G;
reconsider H as FinSequence of W;
A7: rng H = T .: (Carrier l) by A5,RELAT_1:127
.= Carrier(T@*l) by A3,ZMODUL05:56;
dom T = [#]V by LmDOMRNG;
then H is one-to-one by A1,A2,A4,A5,FUNCT_1:52,RANKNULL:1;
then
A8: Sum (T@*l) = Sum ((T@*l) (#) H) by A7,VECTSP_6:def 6;
T*(l (#) G) = (T@*l) (#) H by A3,A5,ZMODUL05:55;
hence thesis by A6,A8,ZMODUL05:16;
end;
theorem LMTh441:
for R being Ring
for V, W being LeftMod of R, T being linear-transformation of V, W,
A being Subset of V
st A c= the carrier of (ker T)
holds Lin(T .: A) = (0).W
proof
let R be Ring;
let V, W be LeftMod of R,
T be linear-transformation of V, W,
A be Subset of V;
assume
A1: A c= the carrier of (ker T);
per cases;
suppose A = {};
then T .: A = {}(the carrier of W);
hence Lin(T .: A) = (0).W by MOD_3:6;
end;
suppose A <> {};
then consider a be object such that
A6: a in A by XBOOLE_0:def 1;
A8: a in (ker T) by A1,A6;
reconsider a as Vector of V by A6;
A9: T.a = 0.W by A8,RANKNULL:10;
for x being object holds x in T.:A iff x in {0.W}
proof
let x be object;
hereby
assume x in T.:A;
then consider z be Element of V such that
A4: z in A & x=T.z by FUNCT_2:65;
z in ker T by A1,A4;
then T.z = 0.W by RANKNULL:10;
hence x in {0.W} by TARSKI:def 1,A4;
end;
assume x in {0.W};
then x = T.a by A9,TARSKI:def 1;
hence x in T.:A by FUNCT_2:35,A6;
end;
then T.:A = {0.W} by TARSKI:2;
hence Lin(T .: A) = (0).W by ZMODUL06:22;
end;
end;
theorem LMTh44:
for R being Ring
for V, W being LeftMod of R,
T being linear-transformation of V, W,
A, B, X being Subset of V
st A c= the carrier of (ker T) & X = B \/ A
holds Lin(T .: X) = Lin(T.: B)
proof
let R be Ring;
let V, W be LeftMod of R,
T be linear-transformation of V, W,
A, B, X be Subset of V;
assume that
A1: A c= the carrier of (ker T) and
A2: X = B \/ A;
P1: T .: X = (T.:B) \/ (T.:A) by A2,RELAT_1:120;
thus Lin(T .: X) = Lin(T.:B) + Lin(T.:A) by P1,MOD_3:12
.= Lin(T.:B) + (0).W by LMTh441,A1
.= Lin(T.:B) by VECTSP_5:9;
end;
:: Rank-nullity theorem
theorem Th44:
for V, W being finite-rank free Z_Module,
T being linear-transformation of V, W
holds rank V = rank(T) + nullity(T)
proof
let V, W be finite-rank free Z_Module,
T be linear-transformation of V,W;
set A = the finite Basis of ker T;
reconsider A9 = A as Subset of V by ZMODUL05:29;
reconsider A9 as finite linearly-independent Subset of V
by VECTSP_7:def 3,ZMODUL03:15;
consider B9 be finite linearly-independent Subset of V,
a be Element of INT.Ring such that
A1: a <> 0.INT.Ring & A9 c= B9 & a (*) V is Submodule of Lin(B9)
by LmRankSX11;
X1: V is finite-rank free Submodule of V by ZMODUL01:32;
rank(a (*) V) <= rank(Lin(B9)) by A1,ZMODUL05:2;
then X2: rank(V) <= rank(Lin(B9)) by A1,X1,ZMODUL06:52;
rank(Lin(B9)) <= rank(V) by ZMODUL05:2;
then rank(Lin(B9)) = rank(V) by X2,XXREAL_0:1;
then X0: rank(V) = card(B9) by ZMODUL05:3;
reconsider X = B9 \ A9 as finite Subset of B9 by XBOOLE_1:36;
reconsider X as finite Subset of V;
A2: B9 = A9 \/ X by A1,XBOOLE_1:45;
reconsider C = T .: X as finite Subset of W;
A3: T|X is one-to-one by A1,X0,ZM05Th35;
C is linearly-independent
proof
assume C is linearly-dependent;
then consider l be Linear_Combination of C such that
A5: Carrier l <> {} and
A6: Sum l = 0.W;
ex m being Linear_Combination of X st l = T@*m
proof
reconsider l9 = l as Linear_Combination of T .: X;
set m = T#(l9);
take m;
thus thesis by A3,ZMODUL05:60;
end;
then consider m be Linear_Combination of B9 \ A9 such that
A7: l = T@*m;
T.(Sum m) = 0.W by A1,A6,A7,X0,ZM05Th59;
then Sum m in ker T by ZMODUL05:20;
then Sum m in Lin A by VECTSP_7:def 3;
then Sum m in Lin A9 by ZMODUL03:20;
then consider n be Linear_Combination of A9 such that
A8: Sum m = Sum n by ZMODUL02:64;
A9: Carrier (m - n) c= (Carrier m) \/ (Carrier n) & (B9 \ A9) \/ A9 = B9
by A1,ZMODUL02:40,XBOOLE_1:45;
A10: Carrier m c= B9 \ A9 & Carrier n c= A by VECTSP_6:def 4;
then (Carrier m) \/ (Carrier n) c= (B9 \ A9) \/ A by XBOOLE_1:13;
then Carrier (m - n) c= B9 by A9;
then reconsider o = m - n as Linear_Combination of B9
by VECTSP_6:def 4;
(Sum m) - (Sum n) = 0.V by A8,VECTSP_1:19;
then Sum (m - n) = 0.V by ZMODUL02:55; then
A12: Carrier o = {} by VECTSP_7:def 1;
A9 misses B9 \ A9 by XBOOLE_1:79;
then Carrier (m - n) = (Carrier m) \/ (Carrier n)
by A10,XBOOLE_1:64,ZMODUL05:48;
then Carrier m = {} by A12;
then T .: (Carrier m) = {};
hence thesis by A5,A7,XBOOLE_1:3,ZMODUL05:def 8;
end;
then reconsider C as finite linearly-independent Subset of W;
dom T = [#]V by LmDOMRNG;
then X c= dom (T|X) by RELAT_1:62;
then X,(T|X) .: X are_equipotent by A3,CARD_1:33;
then X,C are_equipotent by RELAT_1:129;
then
A13: card C = card X by CARD_1:5;
reconsider aT = a (*) (im T) as Submodule of W by ZMODUL01:42;
L1: Lin(T.: B9) = Lin(T .: X) by A2,LMTh44;
for v being VECTOR of W st v in aT holds v in Lin(C)
proof
let v be VECTOR of W;
assume v in aT;
then consider tw be VECTOR of (im T) such that
X1: v = a * tw;
tw is VECTOR of W & tw in (im T) by ZMODUL01:25;
then consider w be VECTOR of V such that
X2: tw = T.w by ZMODUL05:23;
X3: v = a*T.w by X1,X2,ZMODUL01:29
.= T.(a*w) by MOD_2:def 2;
a*w in a*V;
then reconsider aw = a*w as VECTOR of a (*) V;
aw in a (*) V;
then aw in Lin(B9) by A1,ZMODUL01:24;
then T.aw in T.:(the carrier of Lin(B9)) by FUNCT_2:35;
hence v in Lin(C) by L1,X3,TARSKI:def 3,ZMODUL06:40;
end;
then a (*) (im T) is Submodule of Lin(C) by ZMODUL01:44;
then rank(a (*) (im T)) <= rank(Lin(C)) by ZMODUL05:2;
then X4: rank(im T) <= rank(Lin(C)) by A1,ZMODUL06:52;
reconsider CC = C as Subset of im T by ZMODUL05:22;
Lin(CC) is Submodule of im T;
then Lin(C) is Submodule of im T by ZMODUL03:20;
then rank(Lin(C)) <= rank(im T) by ZMODUL05:2;
then X5: rank T = rank(Lin(C)) by X4,XXREAL_0:1
.= card C by ZMODUL05:3;
nullity T = card A by ZMODUL03:def 5;
hence thesis by A2,A13,X0,X5,CARD_2:40,XBOOLE_1:79;
end;
theorem
for V, W being finite-rank free Z_Module,
T being linear-transformation of V, W
st T is one-to-one holds rank V = rank T
proof
let V, W be finite-rank free Z_Module,
T be linear-transformation of V,W;
assume T is one-to-one;
then ker T = (0).V by ZMODUL05:25; then
A1: nullity(T) = 0 by ZMODUL05:26;
rank V = rank(T) + nullity(T) by Th44
.= rank(T) by A1;
hence thesis;
end;
::: canonical decomposition
definition
let R be Ring;
let V, W be LeftMod of R;
let T be linear-transformation of V, W;
func Zdecom(T) -> linear-transformation of VectQuot(V,ker T), im T
means :defdecom:
it is bijective &
for v being Element of V holds it.((ZQMorph(V,ker T)).v) = T.v;
existence
proof
set KT = ker T;
XX: T is additive & T is homogeneous;
YY: rng (ZQMorph(V,KT)) = the carrier of VectQuot(V, KT)
by FUNCT_2:def 3;
defpred P[object,object] means
ex v being Element of V st $1=(ZQMorph(V,KT)).v & $2 = T.v;
A11: for z being Element of VectQuot(V,KT) holds
ex y being Element of im T st P[z,y]
proof
let z be Element of VectQuot(V, KT);
consider v be Element of V such that
A12: z = (ZQMorph(V,KT)).v by FUNCT_2:113,YY;
set y = T.v;
dom T = [#]V by LmDOMRNG;
then y in T .: [#]V by FUNCT_1:def 6;
then y in [#](im T) by RANKNULL:def 2;
then reconsider y = T.v as Element of im T;
take y;
thus thesis by A12;
end;
consider f be Function of
the carrier of VectQuot(V,KT),the carrier of im T such that
A15: for z being Element of VectQuot(V,KT) holds P[z,f.z]
from FUNCT_2:sch 3(A11);
A16: for v being Element of V holds f.((ZQMorph(V,KT)).v) = T.v
proof
let v1 be Element of V;
set z = (ZQMorph(V,KT)).v1;
reconsider z as Element of VectQuot(V,KT);
consider v2 be Element of V such that
Q1: z = (ZQMorph(V,KT)).v2 & f.z = T.v2 by A15;
(ZQMorph(V,KT)).v1 = v1+KT by defMophVW;
then
Q3: v1+KT = v2 + KT by Q1,defMophVW;
Q4: v1 in v1+KT by VECTSP_4:44;
A23: v2 in v1 + KT by Q3,VECTSP_4:44;
T.v1 - T.v2 = T.(v1 - v2) by ZMODUL05:18
.= 0.W by A23,Q4,VECTSP_4:63,RANKNULL:10;
hence thesis by Q1,RLVECT_1:21;
end;
for x, y being Vector of VectQuot(V, ker T)
holds f.(x+y) = (f.x) + (f.y)
proof
let x, y be Vector of VectQuot(V, KT);
consider v be Element of V such that
A17: x = (ZQMorph(V,KT)).v by FUNCT_2:113,YY;
consider w be Element of V such that
A18: y = (ZQMorph(V,KT)).w by FUNCT_2:113,YY;
A19: (ZQMorph(V,KT)).v = v+KT by defMophVW;
A20: (ZQMorph(V,KT)).w = w+KT by defMophVW;
reconsider A = v+KT as Element of CosetSet(V,KT) by A19,VECTSP10:def 6;
reconsider B = w+KT as Element of CosetSet(V,KT) by A20,VECTSP10:def 6;
x+y = (addCoset(V,KT)).(A,B) by A17,A18,A19,A20,VECTSP10:def 6
.= (v+w)+ KT by VECTSP10:def 3; then
A22: x+y = (ZQMorph(V,KT)).(v+w) by defMophVW;
A23: T.v = f.x by A16,A17;
A24: T.w = f.y by A16,A18;
thus f.(x+y) = T.(v+w) by A16,A22
.= T.v + T.w by XX
.= f.x + f.y by A23,A24,VECTSP_4:13;
end; then
A25: f is additive;
for a being Element of R, x being Element of VectQuot(V,KT)
holds f.(a*x) = a*(f.x)
proof
let a be Element of R, x be Element of VectQuot(V,KT);
consider v be Element of V such that
A2: x = (ZQMorph(V,KT)).v & f.x = T.v by A15;
(ZQMorph(V,KT)).(a*v) = a*x by A2,MOD_2:def 2;
hence f.(a*x) = T.(a*v) by A16
.= a*(T.v) by XX
.= a*(f.x) by A2,VECTSP_4:14;
end; then
A17: f is homogeneous;
for y being object st y in the carrier of im T
ex x being object st x in the carrier of VectQuot(V,KT) & y = f.x
proof
let y be object;
assume LA0: y in the carrier of im T;
the carrier of im T c= the carrier of W by VECTSP_4:def 2;
then reconsider y0 = y as Element of W by LA0;
y0 in im T by LA0;
then consider v be Element of V such that
LA1: y0 = T.v by RANKNULL:13;
f.((ZQMorph(V,KT)).v) =y by A16,LA1;
hence thesis;
end; then
rng f = the carrier of im T by FUNCT_2:10; then
A18: f is onto by FUNCT_2:def 3;
for x1, x2 being object st
x1 in the carrier of VectQuot(V,KT)
& x2 in the carrier of VectQuot(V,KT)
& f.x1 = f.x2 holds x1 = x2
proof
let x1, x2 be object;
assume A19: x1 in the carrier of VectQuot(V,KT)
& x2 in the carrier of VectQuot(V,KT) & f.x1 = f.x2;
reconsider xx1 = x1 as Element of VectQuot(V,KT) by A19;
reconsider xx2 = x2 as Element of VectQuot(V,KT) by A19;
consider v1 be Element of V such that
A20: xx1 = (ZQMorph(V,KT)).v1 & f.xx1 = T.v1 by A15;
consider v2 be Element of V such that
A21: xx2 = (ZQMorph(V,KT)).v2 & f.xx2 = T.v2 by A15;
A23: v1-v2 in ker T by A19,A20,A21,RANKNULL:17;
A24:(ZQMorph(V,KT)).v1 = v1+KT by defMophVW;
A25:(ZQMorph(V,KT)).v2 = v2+KT by defMophVW;
(v1-v2) +v2 = v1 -(v2-v2) by RLVECT_1:29
.= v1 - 0.V by RLVECT_1:15
.= v1;
then v1 in v2+ KT by A23;
hence thesis by A24,A25,A21,A20,VECTSP_4:55;
end;
then f is one-to-one by FUNCT_2:19;
hence thesis by A18,A16,A17,A25;
end;
uniqueness
proof
let f1, f2 be linear-transformation of VectQuot(V,ker T),im T;
assume AS1:
f1 is one-to-one & f1 is onto &
for v being Element of V holds f1.((ZQMorph(V,ker T)).v) = T.v;
assume AS2:
f2 is one-to-one & f2 is onto &
for v being Element of V holds f2.((ZQMorph(V,ker T)).v) = T.v;
YY: rng (ZQMorph(V,ker T)) = the carrier of VectQuot(V,ker T)
by FUNCT_2:def 3;
for v being Element of VectQuot(V, ker T) holds f1.v = f2.v
proof
let v be Element of VectQuot(V, ker T);
consider z be Element of V such that
A12: v = (ZQMorph(V,ker T)).z by FUNCT_2:113,YY;
thus f1.v = T.z by A12,AS1
.= f2.v by A12,AS2;
end;
hence f1 = f2 by FUNCT_2:def 8;
end;
end;
theorem
for R being Ring
for V, W being LeftMod of R,
T being linear-transformation of V, W holds
T = Zdecom(T) * ZQMorph(V, ker T)
proof
let R be Ring;
let V, W be LeftMod of R;
let T be linear-transformation of V, W;
set g = Zdecom(T) * ZQMorph(V,ker T);
A1: dom g = the carrier of V by FUNCT_2:def 1;
the carrier of (im T) c= the carrier of W by VECTSP_4:def 2;
then rng g c= the carrier of W;
then reconsider g as Function of V, W by FUNCT_2:2,A1;
for z being Element of V holds T.z = g.z
proof
let z be Element of V;
thus T.z = (Zdecom(T)).((ZQMorph(V,ker T)).z) by defdecom
.= g.z by FUNCT_2:15;
end;
hence thesis by FUNCT_2:def 8;
end;
theorem LMFirst1:
for R being Ring
for V, U, W being LeftMod of R,
f being linear-transformation of V, U,
g being linear-transformation of U, W holds
g*f is linear-transformation of V, W
proof
let R be Ring;
let V, U, W be LeftMod of R,
f be linear-transformation of V, U,
g be linear-transformation of U, W;
set gf = g*f;
for a being Element of R,
x being Element of V holds gf.(a*x) = a*(gf.x)
proof
let a be Element of R, x be Element of V;
P3: f is homogeneous;
P4: g is homogeneous;
thus gf.(a*x) = g.(f.(a*x)) by FUNCT_2:15
.= g.(a*f.x) by P3
.= a*g.(f.x) by P4
.= a*gf.x by FUNCT_2:15;
end;
then gf is homogeneous;
hence thesis;
end;
definition
let R be Ring;
let V, U, W be LeftMod of R,
f be linear-transformation of V, U,
g be linear-transformation of U, W;
redefine func g*f -> linear-transformation of V, W; :: redefines * (FUNCT_1, synonym) → * (RELAT_1, synonym) → (#) (RELAT_1, definition)
correctness by LMFirst1;
end;
theorem LMFirst2:
for R being Ring
for V, W being LeftMod of R,
f being linear-transformation of V, W holds
the carrier of ker f = f"{0.W}
proof
let R be Ring;
let V, W be LeftMod of R,
f be linear-transformation of V, W;
A0: [#](ker f) = { u where u is Element of V : f.u = 0.W }
by RANKNULL:def 1;
for x being object holds
x in the carrier of ker f iff x in f"{0.W}
proof
let x be object;
hereby
assume x in the carrier of ker f;
then consider v be Vector of V such that
A2: x = v & f.v = 0.W by A0;
f.x in {0.W} by A2,TARSKI:def 1;
hence x in f"{0.W} by FUNCT_2:38,A2;
end;
assume A11: x in f"{0.W};
then
A1: x in the carrier of V & f.x in {0.W} by FUNCT_2:38;
reconsider v = x as Vector of V by A11;
f.v = 0.W by A1,TARSKI:def 1;
hence x in the carrier of ker f by A0;
end;
hence thesis by TARSKI:2;
end;
theorem LMFirst3:
for R being Ring
for V, U, W being LeftMod of R,
f being linear-transformation of V, U,
g being linear-transformation of U, W holds
the carrier of ker (g*f) = f"(the carrier of ker g)
proof
let R be Ring;
let V, U, W be LeftMod of R,
f be linear-transformation of V, U,
g be linear-transformation of U, W;
thus the carrier of ker (g*f) = (g*f)"{0.W} by LMFirst2
.= f"(g"{0.W}) by RELAT_1:146
.= f"(the carrier of ker g) by LMFirst2;
end;
theorem LMFirst4:
for R being Ring
for V, W being LeftMod of R, f being linear-transformation of V, W
st f is onto holds
im f = (Omega).W
proof
let R be Ring;
let V, W be LeftMod of R, f be linear-transformation of V, W;
assume f is onto; then
B1: rng f = the carrier of W by FUNCT_2:def 3;
B2: dom f = the carrier of V by FUNCT_2:def 1;
the carrier of im f = [#]im f
.= f .: [#]V by RANKNULL:def 2
.= the carrier of (Omega).W by B1,B2,RELAT_1:113;
hence thesis by VECTSP_4:29;
end;
theorem LMFirst5:
for R being Ring
for V being LeftMod of R, W being Subspace of V holds
ker ZQMorph(V, W) = (Omega).W
proof
let R be Ring;
let V be LeftMod of R, W be Subspace of V;
set f = ZQMorph(V, W);
reconsider Ws = (Omega).W as strict Subspace of V by VECTSP_4:26;
for x being object holds
x in f" {0.VectQuot(V, W)} iff x in the carrier of W
proof
let x be object;
hereby
assume A11: x in f" {0.VectQuot(V, W)}; then
A1: x in the carrier of V & f.x in {0.VectQuot(V, W)}
by FUNCT_2:38;
reconsider v = x as Vector of V by A11;
f.v = 0.VectQuot(V, W) by A1,TARSKI:def 1
.= zeroCoset(V,W) by VECTSP10:def 6
.= the carrier of W;
then v + W = the carrier of W by defMophVW;
then v in W by VECTSP_4:49;
hence x in the carrier of W;
end;
assume B1: x in the carrier of W;
B4: the carrier of W c= the carrier of V by VECTSP_4:def 2;
then reconsider v = x as Vector of V by B1;
B2: v in W by B1;
f.v = v + W by defMophVW
.= zeroCoset(V,W) by B2,VECTSP_4:49
.= 0.VectQuot(V, W) by VECTSP10:def 6;
then f.x in {0.VectQuot(V, W)} by TARSKI:def 1;
hence x in f" {0.VectQuot(V, W)} by B1,B4,FUNCT_2:38;
end;
then f" {0.VectQuot(V, W)} = the carrier of W by TARSKI:2;
then ker f = Ws by LMFirst2,VECTSP_4:29;
hence thesis;
end;
theorem LmStrict11a:
for R being Ring
for V being LeftMod of R, W being Subspace of V,
Ws being strict Subspace of V,
v being Vector of V st Ws = (Omega).W holds
v + W = v + Ws
proof
let R be Ring;
let V be LeftMod of R, W be Subspace of V, Ws be strict Subspace of V,
v be Vector of V such that
A1: Ws = (Omega).W;
for x being object holds x in v + W iff x in v + Ws
proof
let x be object;
hereby
assume B1: x in v + W;
then reconsider xx = x as Vector of V;
consider u be Vector of V such that
B2: xx = v + u & u in W by B1;
u in Ws by A1,B2;
hence x in v + Ws by B2;
end;
assume B1: x in v + Ws;
then reconsider xx = x as Vector of V;
consider u be Vector of V such that
B2: xx = v + u & u in Ws by B1;
u in W by A1,B2;
hence x in v + W by B2;
end;
hence thesis by TARSKI:2;
end;
theorem LmStrict11:
for R being Ring
for V being LeftMod of R, W being Subspace of V,
Ws being strict Subspace of V,
A being object st Ws = (Omega).W holds
A is Coset of W iff A is Coset of Ws
proof
let R be Ring;
let V be LeftMod of R, W be Subspace of V, Ws be strict Subspace of V,
A be object such that
A1: Ws = (Omega).W;
hereby
assume A is Coset of W;
then consider v be Vector of V such that
B1: A = v + W by VECTSP_4:def 6;
A = v + Ws by A1,B1,LmStrict11a;
hence A is Coset of Ws by VECTSP_4:def 6;
end;
assume A is Coset of Ws;
then consider v be Vector of V such that
B1: A = v + Ws by VECTSP_4:def 6;
A = v + W by A1,B1,LmStrict11a;
hence A is Coset of W by VECTSP_4:def 6;
end;
theorem LmStrict1:
for R being Ring
for V being LeftMod of R, W being Subspace of V,
Ws being strict Subspace of V
st Ws = (Omega).W holds
CosetSet(V, W) = CosetSet(V, Ws)
proof
let R be Ring;
let V be LeftMod of R, W be Subspace of V, Ws be strict Subspace of V
such that
A1: Ws = (Omega).W;
for A being object holds A in CosetSet(V, W) iff A in CosetSet(V, Ws)
proof
let A be object;
hereby
assume A in CosetSet(V, W);
then consider AA be Coset of W such that
C1: A = AA;
AA is Coset of Ws by A1,LmStrict11;
hence A in CosetSet(V, Ws) by C1;
end;
assume A in CosetSet(V, Ws);
then consider AA be Coset of Ws such that
C1: A = AA;
AA is Coset of W by A1,LmStrict11;
hence A in CosetSet(V, W) by C1;
end;
hence thesis by TARSKI:2;
end;
theorem LmStrict2:
for R being Ring
for V being LeftMod of R, W being Subspace of V,
Ws being strict Subspace of V
st Ws = (Omega).W holds
addCoset(V, W) = addCoset(V, Ws)
proof
let R be Ring;
let V be LeftMod of R, W be Subspace of V, Ws be strict Subspace of V;
assume AS: Ws = (Omega).W;
set f1 = addCoset(V, W);
set f2 = addCoset(V, Ws);
set C = CosetSet(V,W);
set Cs = CosetSet(V,Ws);
A14: CosetSet(V,W) = CosetSet(V,Ws) by AS,LmStrict1;
now
let A, B be Element of C;
A in C;
then consider A1 be Coset of W such that
A17: A1 = A;
consider a be Vector of V such that
A18: A1 = a+W by VECTSP_4:def 6;
B in C;
then consider B1 be Coset of W such that
A19: B1 = B;
consider b be Vector of V such that
A20: B1 = b+W by VECTSP_4:def 6;
reconsider As = A as Element of Cs by AS,LmStrict1;
A21: As = a+Ws by AS,A17,A18,LmStrict11a;
reconsider Bs = B as Element of Cs by AS,LmStrict1;
A22: Bs = b+Ws by AS,A19,A20,LmStrict11a;
thus f1.(A,B) = a+b + W by A17,A19,A18,A20,VECTSP10:def 3
.= a+b+Ws by LmStrict11a,AS
.= f2.(A,B) by A21,A22,VECTSP10:def 3;
end;
hence thesis by A14,BINOP_1:2;
end;
theorem LmStrict3:
for R being Ring
for V being LeftMod of R, W being Subspace of V,
Ws being strict Subspace of V
st Ws = (Omega).W holds
lmultCoset(V, W) = lmultCoset(V, Ws)
proof
let R be Ring;
let V be LeftMod of R, W be Subspace of V, Ws be strict Subspace of V;
assume AS: Ws = (Omega).W;
set f1 = lmultCoset(V, W);
set f2 = lmultCoset(V, Ws);
set C = CosetSet(V,W);
set Cs = CosetSet(V,Ws);
A14: CosetSet(V,W) = CosetSet(V,Ws) by AS,LmStrict1;
now
let z be Element of R;
let A be Element of C;
A in C;
then consider A1 be Coset of W such that
A17: A1 = A;
consider a be Vector of V such that
A18: A1 = a + W by VECTSP_4:def 6;
reconsider As = A as Element of Cs by AS,LmStrict1;
A21:As = a + Ws by AS,A17,A18,LmStrict11a;
thus f1.(z,A) = z*a + W by A17,A18,VECTSP10:def 5
.= z*a+Ws by LmStrict11a,AS
.= f2.(z,A) by A21,VECTSP10:def 5;
end;
hence thesis by A14,BINOP_1:2;
end;
theorem ThStrict1:
for R being Ring
for V being LeftMod of R, W being Subspace of V,
Ws being strict Subspace of V st Ws = (Omega).W holds
VectQuot(V, W) = VectQuot(V, Ws)
proof
let R be Ring;
let V be LeftMod of R, W be Subspace of V, Ws be strict Subspace of V
such that
A1: Ws = (Omega).W;
set Z1 = VectQuot(V, W);
set Z2 = VectQuot(V, Ws);
A2: the carrier of Z1 = CosetSet(V, W) by VECTSP10:def 6
.= CosetSet(V, Ws) by A1,LmStrict1
.= the carrier of Z2 by VECTSP10:def 6;
A3: the addF of Z1 = addCoset(V, W) by VECTSP10:def 6
.= addCoset(V, Ws) by A1,LmStrict2
.= the addF of Z2 by VECTSP10:def 6;
A4: 0.Z1 = zeroCoset(V, W) by VECTSP10:def 6
.= zeroCoset(V, Ws) by A1
.= 0.Z2 by VECTSP10:def 6;
the lmult of Z1 = lmultCoset(V, W) by VECTSP10:def 6
.= lmultCoset(V, Ws) by A1,LmStrict3
.= the lmult of Z2 by VECTSP10:def 6;
hence thesis by A2,A3,A4;
end;
theorem
for R being Ring
for V, U being LeftMod of R, V1 being Submodule of V,
U1 being Submodule of U,
f being linear-transformation of V, U
st f is onto & the carrier of V1 = f" (the carrier of U1)
holds ex F being linear-transformation of
VectQuot(V, V1), VectQuot(U, U1) st F is bijective
proof
let R be Ring;
let V, U be LeftMod of R, V1 be Submodule of V, U1 be Submodule of U,
f be linear-transformation of V, U;
assume AS: f is onto & the carrier of V1 = f" (the carrier of U1);
set g = ZQMorph(U,U1);
reconsider V1s = (Omega).V1 as strict Submodule of V by ZMODUL01:42;
P2: g*f is onto by AS,FUNCT_2:27;
P5: VectQuot(V, V1) = VectQuot(V, V1s) by ThStrict1;
the carrier of ker (g*f) = f"(the carrier of ker g) by LMFirst3
.= f"(the carrier of (Omega).U1) by LMFirst5
.= the carrier of V1s by AS; then
P3: ker (g*f) = V1s by ZMODUL01:45;
P4: im (g*f) = (Omega).VectQuot(U, U1) by P2,LMFirst4
.= VectQuot(U, U1);
then reconsider F = Zdecom(g*f) as linear-transformation of
VectQuot(V, V1), VectQuot(U, U1) by P3,P5;
take F;
Zdecom(g*f) is bijective by defdecom;
hence F is bijective by P4;
end;
theorem
for R being Ring
for V being LeftMod of R, W1, W2 being Submodule of V,
U1 being Submodule of W1 + W2, U2 being strict Submodule of W1
st U1 = W2 & U2 = W1 /\ W2 holds
ex F being linear-transformation of
VectQuot(W1 + W2, U1), VectQuot(W1, U2)
st F is bijective
proof
let R be Ring;
let V be LeftMod of R, W1, W2 be Submodule of V,
U1 be Submodule of W1 + W2,
U2 be strict Submodule of W1 such that
A1: U1 = W2 & U2 = W1 /\ W2;
set Z1 = VectQuot(W1 + W2, U1);
set Z2 = VectQuot(W1, U2);
defpred P[object, object] means
ex v being Element of W1 + W2 st $1 = v & $2 = v + U1;
A2: for z being Element of W1 holds
ex y being Element of Z1 st P[z,y]
proof
let z be Element of W1;
reconsider zv = z as Element of V by ZMODUL01:25;
zv in W1;
then zv in W1 + W2 by ZMODUL01:93;
then reconsider zz = zv as Element of W1 + W2;
set y = zz + U1;
y is Coset of U1 by VECTSP_4:def 6;
then y in CosetSet(W1 + W2, U1);
then reconsider yy = y as Element of Z1 by VECTSP10:def 6;
take yy;
thus thesis;
end;
consider f be Function of
the carrier of W1, the carrier of Z1 such that
A3: for z being Element of W1 holds P[z,f.z] from FUNCT_2:sch 3(A2);
f is linear-transformation of W1, Z1
proof
for x, y being Element of W1 holds f.(x+y) = (f.x) + (f.y)
proof
let x, y be Element of W1;
consider xx be Element of W1 + W2 such that
C1: x = xx & f.x = xx + U1 by A3;
consider yy be Element of W1 + W2 such that
C2: y = yy & f.y = yy + U1 by A3;
consider xy be Element of W1 + W2 such that
C3: x + y = xy & f.(x+y) = xy + U1 by A3;
reconsider xv = x, yv = y as Element of V by ZMODUL01:25;
xx + U1 is Coset of U1 & yy + U1 is Coset of U1 by VECTSP_4:def 6;
then xx + U1 in CosetSet(W1 + W2, U1) &
yy + U1 in CosetSet(W1 + W2, U1);
then reconsider xU = xx + U1, yU = yy + U1
as Element of CosetSet(W1 + W2, U1);
C4: xx + yy = xv + yv by C1,C2,ZMODUL01:28
.= xy by C3,ZMODUL01:28;
thus (f.x) + (f.y) = addCoset(W1 + W2, U1).(xU, yU)
by C1,C2,VECTSP10:def 6
.= f.(x+y) by C3,C4,VECTSP10:def 3;
end;
then B1: f is additive;
for a being Element of R,
x being Element of W1 holds f.(a*x) = a*(f.x)
proof
let a be Element of R, x be Element of W1;
consider xx be Element of W1 + W2 such that
C1: x = xx & f.x = xx + U1 by A3;
consider ax be Element of W1 + W2 such that
C2: a * x = ax & f.(a*x) = ax + U1 by A3;
reconsider xv = x as Element of V by ZMODUL01:25;
C3: a * xx = a * xv by C1,ZMODUL01:29
.= ax by C2,ZMODUL01:29;
xx + U1 is Coset of U1 by VECTSP_4:def 6;
then xx + U1 in CosetSet(W1 + W2, U1);
then reconsider xU = xx + U1 as Element of CosetSet(W1 + W2, U1);
thus f.(a*x) = lmultCoset(W1 + W2, U1).(a, xU) by C2,C3,VECTSP10:def 5
.= a*(f.x) by C1,VECTSP10:def 6;
end;
then f is homogeneous;
hence thesis by B1;
end;
then reconsider f as linear-transformation of W1, Z1;
A4: ker f = U2
proof
for v being Element of W1 holds v in ker f iff v in U2
proof
let v be Element of W1;
hereby
assume v in ker f;
then C1: f.v = 0.Z1 by RANKNULL:10;
consider vv be Element of W1 + W2 such that
C2: v = vv & f.v = vv + U1 by A3;
vv + U1 = zeroCoset(W1 + W2, U1) by C1,C2,VECTSP10:def 6
.= the carrier of U1;
then C3: v in W2 by A1,C2,ZMODUL01:63;
v in W1;
hence v in U2 by A1,C3,ZMODUL01:94;
end;
assume C1: v in U2;
consider vv be Element of W1 + W2 such that
C2: v = vv & f.v = vv + U1 by A3;
vv in U1 by A1,C1,C2,ZMODUL01:94;
then f.v = zeroCoset(W1 + W2, U1) by C2,ZMODUL01:63
.= 0.Z1 by VECTSP10:def 6;
hence v in ker f by RANKNULL:10;
end;
hence thesis by ZMODUL01:46;
end;
A5: im f = VectQuot(W1 + W2, U1)
proof
for y being object st y in the carrier of Z1
holds f"{y} <> {}
proof
let y be object such that
C2: y in the carrier of Z1;
y in CosetSet(W1 + W2, U1) by C2,VECTSP10:def 6;
then consider yy be Coset of U1 such that
C8: y = yy;
consider z be Element of W1 + W2 such that
C3: y = z + U1 by C8,VECTSP_4:def 6;
z in W1 + W2;
then consider z1, z2 be Element of V such that
C4: z1 in W1 & z2 in W2 & z = z1 + z2 by ZMODUL01:92;
reconsider zz1 = z1 as Element of W1 by C4;
consider zzz1 be Element of W1 + W2 such that
C6: zz1 = zzz1 & f.zz1 = zzz1 + U1 by A3;
z2 in W1 + W2 by C4,ZMODUL01:93;
then reconsider zzz2 = z2 as Element of W1 + W2;
C7: z = zzz1 + zzz2 by C4,C6,ZMODUL01:28;
y = f.zz1 by A1,C3,C4,C6,C7,ZMODUL01:65;
then f.zz1 in {y} by TARSKI:def 1;
hence f"{y} <> {} by FUNCT_2:38;
end;
then B1: rng f = the carrier of Z1 by FUNCT_2:41;
B2: dom f = the carrier of W1 by FUNCT_2:def 1;
the carrier of im f = [#]im f
.= f .: [#]W1 by RANKNULL:def 2
.= the carrier of Z1 by B1,B2,RELAT_1:113;
hence thesis by ZMODUL01:47;
end;
reconsider F = Zdecom(f) as linear-transformation of Z2, Z1 by A4,A5;
consider FI be linear-transformation of Z1, Z2 such that
X1: FI = F" & FI is bijective by A4,A5,defdecom,ZMODUL06:42;
take FI;
thus thesis by X1;
end;
theorem
for R being Ring
for V being LeftMod of R, W1 being Submodule of V,
W2 being Submodule of W1,
U1 being Submodule of V, U2 being Submodule of VectQuot(V, U1)
st U1 = W2 & U2 = VectQuot(W1, W2)
holds ex F being linear-transformation of
VectQuot(VectQuot(V, U1), U2), VectQuot(V, W1)
st F is bijective
proof
let R be Ring;
let V be LeftMod of R, W1 be Submodule of V, W2 be Submodule of W1,
U1 be Submodule of V, U2 be Submodule of VectQuot(V, U1);
assume A1: U1 = W2 & U2 = VectQuot(W1, W2);
set Z1 = VectQuot(VectQuot(V, U1), U2);
set Z2 = VectQuot(V, W1);
YY: rng (ZQMorph(V,U1)) = the carrier of VectQuot(V,U1)
by FUNCT_2:def 3;
defpred P[object, object] means
ex v being Element of V st $1 = v + U1 & $2 = v + W1;
A2: for z being Element of VectQuot(V, U1) holds
ex y being Element of VectQuot(V, W1) st P[z,y]
proof
let z be Element of VectQuot(V, U1);
consider v be Element of V such that
A17: z = (ZQMorph(V,U1)).v by FUNCT_2:113,YY;
A19: (ZQMorph(V,U1)).v = v + U1 by defMophVW;
set y = v + W1;
y is Coset of W1 by VECTSP_4:def 6;
then y in CosetSet(V, W1);
then reconsider y as Element of VectQuot(V, W1) by VECTSP10:def 6;
take y;
thus thesis by A17,A19;
end;
consider f be Function of VectQuot(V, U1), VectQuot(V, W1)
such that
A3: for z being Element of VectQuot(V, U1)
holds P[z,f.z] from FUNCT_2:sch 3(A2);
f is linear-transformation of VectQuot(V, U1), VectQuot(V, W1)
proof
for x, y being Element of VectQuot(V, U1)
holds f.(x+y) = (f.x) + (f.y)
proof
let x, y be Element of VectQuot(V, U1);
consider xx be Element of V such that
C1: x = xx + U1 & f.x = xx + W1 by A3;
consider yy be Element of V such that
C2: y = yy + U1 & f.y = yy + W1 by A3;
consider xy be Element of V such that
C3: x + y = xy + U1 & f.(x+y) = xy + W1 by A3;
reconsider xU = xx + U1, yU = yy + U1
as Element of CosetSet(V, U1) by C1,C2,VECTSP10:def 6;
reconsider fxU = xx + W1, fyU = yy + W1
as Element of CosetSet(V, W1) by C1,C2,VECTSP10:def 6;
xy + U1 = addCoset(V, U1).(xU, yU) by C3,C1,C2,VECTSP10:def 6
.= (xx + yy) + U1 by VECTSP10:def 3;
then (xx + yy) in xy + U1 by ZMODUL01:58;
then consider w be Vector of V such that
D21: xx + yy = xy + w & w in U1;
w in W1 by A1,D21,ZMODUL01:24;
then
D3: xx + yy in xy + W1 by D21;
xx + yy in (xx + yy)+W1 by ZMODUL01:58;
then
C4: xy + W1 = (xx + yy) + W1 by D3,ZMODUL01:68;
thus
(f.x) + (f.y) = addCoset(V, W1).(fxU, fyU) by C1,C2,VECTSP10:def 6
.= f.(x+y) by C4,C3,VECTSP10:def 3;
end;
then B1: f is additive;
for a being Element of R,
x being Element of VectQuot(V, U1)
holds f.(a*x) = a*(f.x)
proof
let a be Element of R, x be Element of VectQuot(V, U1);
consider xx be Element of V such that
C1: x = xx + U1 & f.x = xx + W1 by A3;
consider ax be Element of V such that
C3: a*x = ax + U1 & f.(a*x) = ax + W1 by A3;
reconsider xU = xx + U1 as Element of CosetSet(V, U1)
by C1,VECTSP10:def 6;
reconsider fxU = xx + W1 as Element of CosetSet(V, W1)
by C1,VECTSP10:def 6;
ax + U1 = lmultCoset(V, U1).(a,xU) by C3,C1,VECTSP10:def 6
.= (a*xx) + U1 by VECTSP10:def 5;
then (a*xx) in ax + U1 by ZMODUL01:58;
then consider w be Vector of V such that
D21: a*xx = ax+ w & w in U1;
w in W1 by A1,D21,ZMODUL01:24;
then
D3: a*xx in ax + W1 by D21;
a*xx in (a*xx) + W1 by ZMODUL01:58; then
C4: ax + W1 = (a*xx) + W1 by D3,ZMODUL01:68;
thus a*(f.x) = lmultCoset(V, W1).(a,fxU) by C1,VECTSP10:def 6
.= f.(a*x) by C4,C3,VECTSP10:def 5;
end;
then f is homogeneous;
hence thesis by B1;
end;
then reconsider f as linear-transformation of VectQuot(V, U1),
VectQuot(V, W1);
A4: ker f = U2
proof
for v being Element of VectQuot(V, U1)
holds v in ker f iff v in U2
proof
let v be Element of VectQuot(V, U1);
hereby
assume v in ker f;
then C1: f.v = 0.VectQuot(V, W1) by RANKNULL:10;
consider vv be Element of V such that
C2: v = vv + U1 & f.v = vv + W1 by A3;
vv + W1 = zeroCoset(V, W1) by C1,C2,VECTSP10:def 6
.= the carrier of W1;
then vv in W1 by ZMODUL01:63;
then reconsider vv1 = vv as Vector of W1;
for x being object holds x in vv + U1 iff x in vv1 + W2
proof
let x be object;
hereby
assume x in vv + U1;
then consider w3 be Vector of V such that
X1: x = vv + w3 & w3 in U1;
w3 in W1 by A1,X1,ZMODUL01:24;
then reconsider ww3 = w3 as Vector of W1;
X2: vv + w3 = vv1 + ww3 by ZMODUL01:28;
thus x in vv1+W2 by A1,X1,X2;
end;
assume x in vv1 + W2;
then consider w2 be Vector of W1 such that
X1: x = vv1 + w2 & w2 in W2;
w2 in V by A1,X1,ZMODUL01:24;
then reconsider ww2 = w2 as Vector of V;
X2: vv + ww2 = vv1 + w2 by ZMODUL01:28;
thus x in vv+U1 by A1,X1,X2;
end;
then v = vv1 + W2 by C2,TARSKI:2;
then v is Coset of W2 by VECTSP_4:def 6;
then v in CosetSet(W1, W2);
hence v in U2 by A1,VECTSP10:def 6;
end;
assume v in U2;
then v in CosetSet(W1, W2) by A1,VECTSP10:def 6;
then ex A being Coset of W2 st v = A;
then consider vv1 be Vector of W1 such that
X1: v = vv1 + W2 by VECTSP_4:def 6;
consider vv be Element of V such that
C2: v = vv + U1 & f.v = vv + W1 by A3;
vv in vv1 + W2 by C2,X1,ZMODUL01:58;
then vv in W1;
then f.v = zeroCoset(V, W1) by C2,ZMODUL01:63
.= 0.VectQuot(V, W1) by VECTSP10:def 6;
hence v in ker f by RANKNULL:10;
end;
hence thesis by A1,ZMODUL01:46;
end;
A5: im f = VectQuot(V, W1)
proof
for y being object st y in the carrier of VectQuot(V, W1)
holds f"{y} <> {}
proof
let y be object such that
C2: y in the carrier of VectQuot(V, W1);
y in CosetSet(V, W1) by C2,VECTSP10:def 6;
then consider yy be Coset of W1 such that
C8: y = yy;
consider z be Element of V such that
C3: y = z + W1 by C8,VECTSP_4:def 6;
z + U1 is Coset of U1 by VECTSP_4:def 6;
then z + U1 in CosetSet(V,U1);
then reconsider y1 = z + U1 as Vector of VectQuot(V, U1)
by VECTSP10:def 6;
consider z1 be Element of V such that
C6: y1 = z1 + U1 & f.y1 = z1 + W1 by A3;
z1 in z1 + U1 by ZMODUL01:58;
then consider w be Vector of V such that
D21: z1 = z+ w & w in U1 by C6;
w in W1 by A1,D21,ZMODUL01:24; then
D3: z1 in z + W1 by D21;
z1 in z1+W1 by ZMODUL01:58;
then y = f.y1 by C3,C6,D3,ZMODUL01:68;
then f.y1 in {y} by TARSKI:def 1;
hence f"{y} <> {} by FUNCT_2:38;
end;
then B1: rng f = the carrier of VectQuot(V, W1) by FUNCT_2:41;
B2: dom f = the carrier of VectQuot(V, U1) by FUNCT_2:def 1;
the carrier of im f = [#]im f
.= f .: [#]VectQuot(V, U1) by RANKNULL:def 2
.= the carrier of VectQuot(V, W1) by B1,B2,RELAT_1:113;
hence thesis by ZMODUL01:47;
end;
reconsider F = Zdecom(f) as linear-transformation of Z1, Z2
by A4,A5;
take F;
thus thesis by A4,A5,defdecom;
end;
registration
let V be Z_Module;
let a be non zero Element of INT.Ring;
cluster VectQuot(V, a (*) V) -> torsion;
correctness
proof
set W = a (*) V;
for x being Vector of VectQuot(V, W) holds x is torsion
proof
let x be Vector of VectQuot(V, W);
a <> 0.INT.Ring; then
a <> 0; then
a * x = (a mod a) * x by ZMODUL02:2
.= 0.VectQuot(V, W) by INT_1:50,ZMODUL01:1;
hence thesis;
end;
hence thesis;
end;
end;
theorem ThTrivial1:
for R being Ring
for V being trivial LeftMod of R holds (Omega).V = (0).V
proof
let R be Ring;
let V be trivial LeftMod of R;
assume (Omega).V <> (0).V;
then consider v be Vector of V such that
A1: v in (Omega).V & v <> 0.V by ZMODUL04:24;
reconsider v as Vector of V;
V is non trivial by A1;
hence contradiction;
end;
theorem ThTrivial2:
for R being Ring
for V being LeftMod of R, v being Vector of V st v <> 0.V holds
Lin{v} is non trivial
proof
let R be Ring;
let V be LeftMod of R, v be Vector of V such that
A1: v <> 0.V;
{v} <> {0.V} by A1,ZFMISC_1:3;
then Lin{v} <> (0).V by MOD_3:7;
then (Omega).Lin{v} <> (0).Lin{v} by VECTSP_4:36;
hence thesis by ThTrivial1;
end;
theorem LMCLUS1:
ex V being Z_Module, p being Element of INT.Ring
st p <> 0.INT.Ring & VectQuot(V, p (*) V) is non trivial
proof
reconsider V = ModuleStr(# the carrier of INT.Ring,
the addF of INT.Ring, the ZeroF of INT.Ring, Int-mult-left(INT.Ring) #)
as Z_Module by ZMODUL01:164;
reconsider p = 2 as Element of INT.Ring by INT_1:def 2;
take V, p;
thus p <> 0.INT.Ring;
thus VectQuot(V, p (*) V) is non trivial
proof
reconsider i = 1.INT.Ring as Vector of V;
i + p (*) V is Coset of p (*) V by VECTSP_4:def 6;
then i + p (*) V in CosetSet(V,p (*) V);
then reconsider B = i + p (*) V as Element of CosetSet(V, p (*) V);
reconsider u = B as Vector of VectQuot(V, p (*) V)
by VECTSP10:def 6;
u <> 0.VectQuot(V, p (*) V)
proof
assume u = 0.VectQuot(V, p (*) V);
then i + p (*) V = zeroCoset(V, p (*) V) by VECTSP10:def 6
.= the carrier of p (*) V;
then i in p (*) V by ZMODUL01:63;
then consider w be Vector of V such that
P1: i = p*w;
reconsider w0 = w as Element of INT.Ring;
p*w = p*w0 by ZMODUL06:14;
then 1/2 = w0 by P1;
hence contradiction by NAT_D:33;
end;
hence thesis;
end;
end;
registration
cluster non trivial for torsion Z_Module;
correctness
proof
consider V being Z_Module, p being Element of INT.Ring such that
A1: p <> 0.INT.Ring & VectQuot(V, p (*) V) is non trivial by LMCLUS1;
reconsider pp = p as non zero Element of INT.Ring by A1,STRUCT_0:def 12;
set W = VectQuot(V, pp (*) V);
W is non trivial by A1;
hence thesis;
end;
end;
registration
cluster non torsion-free for Z_Module;
correctness
proof
set V = the non trivial torsion Z_Module;
set v = the non zero Vector of V;
take V;
thus thesis;
end;
end;
registration
let V be non torsion-free Z_Module;
cluster non zero torsion for Vector of V;
correctness
proof
ex v being Vector of V st v is non zero torsion
proof
assume B1: for v being Vector of V holds v is zero or v is non torsion;
for v being Vector of V st v <> 0.V holds v is non torsion
proof
let v be Vector of V such that
C1: v <> 0.V;
v is non zero by C1;
hence thesis by B1;
end;
then V is torsion-free;
hence contradiction;
end;
then consider v be Vector of V such that
A1: v is non zero torsion;
take v;
thus thesis by A1;
end;
end;
registration
cluster non trivial for finitely-generated Z_Module;
correctness
proof
set V = the non trivial Z_Module;
(Omega).V <> (0).V;
then consider v be Vector of V such that
A1: v in (Omega).V & v <> 0.V by ZMODUL04:24;
take Lin{v};
thus thesis by A1,ThTrivial2;
end;
end;
theorem ThTFX:
for V being Z_Module holds
V is torsion-free iff (Omega).V is torsion-free
proof
let V be Z_Module;
thus V is torsion-free implies (Omega).V is torsion-free;
assume A1: (Omega).V is torsion-free;
for v being Vector of V st v <> 0.V holds v is non torsion
proof
let v be Vector of V such that
B1: v <> 0.V;
reconsider vv = v as Vector of (Omega).V;
B2: vv is non torsion by A1,B1;
for i being Element of INT.Ring st i <> 0.INT.Ring holds i * v <> 0.V
proof
let i be Element of INT.Ring such that
C1: i <> 0.INT.Ring;
i * vv <> 0.(Omega).V by B2,C1;
hence thesis;
end;
hence thesis;
end;
hence V is torsion-free;
end;
registration
cluster -> non trivial for non torsion-free Z_Module;
correctness
proof
let V be non torsion-free Z_Module;
assume V is trivial;
then (Omega).V = (0).V by ThTrivial1;
hence contradiction by ThTFX;
end;
end;
registration
cluster non trivial for finitely-generated torsion-free Z_Module;
correctness
proof
set V = the non trivial torsion-free Z_Module;
set v = the non zero Vector of V;
take Lin{v};
v <> 0.V;
hence thesis by ThTrivial2;
end;
end;
registration
let V be non trivial finitely-generated torsion-free Z_Module,
p be prime Element of INT.Ring;
cluster VectQuot(V, p (*) V) -> non trivial;
coherence
proof
set I = the Basis of V;
card(I) > 0
proof
assume card(I) <= 0;
then I = {}(the carrier of V);
then Lin(I) = (0).V by ZMODUL02:67;
then (Omega).V = (0).V by VECTSP_7:def 3;
hence contradiction;
end;
then I is non empty;
then consider v be object such that
A1: v in I by XBOOLE_0:def 1;
reconsider v as Vector of V by A1;
V is Submodule of V & I is linearly-independent &
(Omega).V = Lin(I) by ZMODUL01:32,VECTSP_7:def 3;
then (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 A1,ZMODUL06:24;
then
A6: v is non torsion by ZMODUL06:def 3;
reconsider pp = p as Element of INT.Ring;
assume VectQuot(V, p (*) V) is trivial;
then ZQMorph(V, p (*) V).v = 0.VectQuot(V, p (*) V)
.= zeroCoset(V, p (*) V) by VECTSP10:def 6
.= the carrier of p (*) V;
then v + p (*) V = the carrier of p (*) V by defMophVW;
then v in p (*) V by ZMODUL01:63;
then consider u be Vector of V such that
A3: v = pp * u;
(I \ {v}) \/ {v} = I \/ {v} by XBOOLE_1:39
.= I by A1,XBOOLE_1:12,ZFMISC_1:31;
then Lin(I) = Lin(I \ {v}) + Lin{v} by ZMODUL02:72;
then consider u1, u2 be Vector of V such that
B4: u1 in Lin(I \ {v}) & u2 in Lin{v} & u = u1 + u2
by ZMODUL01:92,ZMODUL03:14;
B5: v = pp * u1 + pp * u2 by A3,B4,VECTSP_1:def 14;
B6: pp*u1 in Lin(I \ {v}) by B4,ZMODUL01:37;
B7: pp*u2 in Lin ({v}) by B4,ZMODUL01:37;
consider iu2 be Element of INT.Ring such that
B8: u2 = iu2 * v by B4,ZMODUL06:19;
B9: pp*u2 = (pp*iu2)*v by B8,VECTSP_1:def 16;
B10: V is_the_direct_sum_of Lin(I \ {v}),Lin{v} by A1,ZMODUL04:33;
B11: v = (1.INT.Ring)*v + 0.V;
B12: v in Lin{v} by ZMODUL06:20;
0.V in Lin(I \ {v}) by ZMODUL01:33;
then (1.INT.Ring)*v -(pp*iu2)*v = (pp*iu2)*v - (pp*iu2)*v
by B5,B11,B6,B7,B9,B10,B12,ZMODUL01:134;
then (1.INT.Ring-(pp*iu2)) * v = (pp*iu2)*v - (pp*iu2)*v by ZMODUL01:9;
then 1.INT.Ring-(pp*iu2) = 0 by A6,RLVECT_1:15;
then 1/p is Integer by XCMPLX_1:89;
hence contradiction by INT_2:def 4,NAT_D:33;
end;
end;
registration
cluster finitely-generated for torsion Z_Module;
correctness
proof
set V = the non trivial finitely-generated torsion-free Z_Module;
set p = the prime Element of INT.Ring;
reconsider pp = p as non zero Element of INT.Ring;
set W = VectQuot(V, pp (*) V);
W is torsion;
hence thesis;
end;
end;
registration
cluster non trivial for finitely-generated torsion Z_Module;
correctness
proof
set V = the non trivial finitely-generated torsion-free Z_Module;
set p = the prime Element of INT.Ring;
reconsider pp = p as prime non zero Element of INT.Ring;
set W = VectQuot(V, pp (*) V);
W is non trivial;
hence thesis;
end;
end;
registration
let V be non trivial finitely-generated torsion-free Z_Module,
p be prime Element of INT.Ring;
cluster VectQuot(V, p (*) V) -> finitely-generated torsion;
correctness;
end;
registration
let V be non torsion Z_Module;
cluster VectQuot(V, torsion_part(V)) -> non trivial;
correctness
proof
assume AS: VectQuot(V, torsion_part(V)) is trivial;
consider v be Vector of V such that
P1: not v is torsion by ZMODUL06:def 2;
v + torsion_part(V) is Coset of torsion_part(V) by VECTSP_4:def 6;
then v + torsion_part(V) in CosetSet(V,torsion_part(V));
then reconsider B = v + torsion_part(V)
as Element of CosetSet(V,torsion_part(V));
reconsider u = B as Vector of VectQuot(V, torsion_part(V))
by VECTSP10:def 6;
u = 0.(VectQuot(V, torsion_part(V))) by AS
.= zeroCoset(V, torsion_part(V)) by VECTSP10:def 6
.= the carrier of torsion_part(V);
then v in torsion_part(V) by ZMODUL01:63;
then v in { v where v is Vector of V : v is torsion } by defTorsionPart;
then ex u being Vector of V st v = u & u is torsion;
hence contradiction by P1;
end;
end;