:: Torsion $\mathbb Z$-module and Torsion-free $\mathbb Z$-module
:: by Yuichi Futa , Hiroyuki Okazaki , Kazuhisa Nakasho and Yasunari Shidama
::
:: Received November 29, 2014
:: Copyright (c) 2014 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies GAUSSINT, NUMBERS, SUBSET_1, RLVECT_1, STRUCT_0, PBOOLE, FUNCT_4,
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, FUNCOP_1, RLSUB_1, ZFMISC_1, INT_1, RLVECT_2,
ZMODUL01, ZMODUL03, RLVECT_3, RMOD_2, RANKNULL, MSAFREE2, INT_3,
COMPLEX1, INT_2, VECTSP_1, MESFUNC1, XCMPLX_0, REALSET1, MONOID_0,
ZMODUL02, RLVECT_5, ZMODUL04, ZMODUL05, ZMODUL06, MOD_3;
notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, FUNCT_1, RELSET_1, PARTFUN1,
FUNCT_2, BINOP_1, DOMAIN_1, FUNCOP_1, FINSET_1, CARD_1, NUMBERS,
XCMPLX_0, XXREAL_0, NAT_1, INT_1, RAT_1, INT_2, REALSET1, FUNCT_4,
STRUCT_0, ALGSTR_0, RLVECT_1, GROUP_1, VECTSP_1, VECTSP_4, VECTSP_5,
VECTSP_6, INT_3, VECTSP_7, VECTSP_9, MATRLIN, BINOM, ZMODUL01, ZMODUL02,
ZMODUL03, GAUSSINT, MOD_2, ZMODUL04, ZMODUL05;
constructors BINOP_2, BINOM, UPROOTS, RELSET_1, ORDERS_1, REALSET1, FUNCT_4,
VECTSP_6, VECTSP_9, VECTSP10, ALGSTR_1, ZMODUL04, ZMODUL05, INT_2,
ZMODUL01, ZMODUL02, MATRLIN, MOD_2, INT_3;
registrations SUBSET_1, FUNCT_1, RELSET_1, FUNCT_2, FINSET_1, NUMBERS,
XREAL_0, STRUCT_0, RLVECT_1, MEMBERED, CARD_1, INT_1, XBOOLE_0, ORDINAL1,
XXREAL_0, NAT_1, INT_3, RELAT_1, ZMODUL02, GAUSSINT, VECTSP_9, FUNCT_4,
RAT_1, XCMPLX_0, ZMODUL03, ZMODUL04, ZMODUL05, VECTSP_4, VECTSP_5, MOD_2,
VECTSP_2, VECTSP_7;
requirements REAL, NUMERALS, BOOLE, SUBSET, ARITHM;
begin :: 1. Torsion $\mathbb{Z}$-module and torsion-free $\mathbb{Z}$-module
theorem :: ZMODUL06:1
for V being Z_Module, W being Submodule of V
holds (1.INT.Ring) (*) W = (Omega).W;
theorem :: ZMODUL06:2
for V being Z_Module, W1, W2, W3 being Submodule of V holds
W1 /\ W2 is Submodule of (W1 + W3) /\ W2;
theorem :: ZMODUL06:3
for V being Z_Module, W1, W2, W3 being Submodule of V
st W1 /\ W2 <> (0).V holds (W1 + W3) /\ W2 <> (0).V;
theorem :: ZMODUL06:4
for V being Z_Module, I, I1 being linearly-independent Subset of V
st I1 c= I holds
Lin(I \ I1) /\ Lin(I1) = (0).V;
reserve V for Z_Module;
reserve W for Submodule of V;
reserve v, u for VECTOR of V;
reserve i for Element of INT.Ring;
definition
let V be Z_Module, v be VECTOR of V;
attr v is torsion means
:: ZMODUL06:def 1
ex i being Element of INT.Ring st i <> 0.INT.Ring & i*v = 0.V;
end;
registration let V be Z_Module;
cluster 0.V -> torsion;
end;
theorem :: ZMODUL06:5
v is torsion & u is torsion implies v + u is torsion;
theorem :: ZMODUL06:6
v is torsion implies -v is torsion;
theorem :: ZMODUL06:7
v is torsion & u is torsion implies v - u is torsion;
theorem :: ZMODUL06:8
v is torsion implies i * v is torsion;
theorem :: ZMODUL06:9
for v being VECTOR of V, w being VECTOR of W st v = w holds
v is torsion iff w is torsion;
registration
let V be Z_Module;
cluster torsion for VECTOR of V;
end;
theorem :: ZMODUL06:10
v is non torsion implies -v is non torsion;
theorem :: ZMODUL06:11
v is non torsion & i <> 0 implies i * v is non torsion;
theorem :: ZMODUL06:12
v is non torsion iff {v} is linearly-independent;
definition
let V be Z_Module;
attr V is torsion means
:: ZMODUL06:def 2
for v being VECTOR of V holds v is torsion;
end;
registration let V be Z_Module;
cluster (0).V -> torsion;
end;
registration
cluster torsion for Z_Module;
end;
theorem :: ZMODUL06:13
for v be Element of INT.Ring,v1 be Integer st v = v1 holds
for n be Nat holds (Nat-mult-left(INT.Ring)).(n,v) = n*v1;
theorem :: ZMODUL06:14
for x be Element of INT.Ring, v be Element of INT.Ring,
v1 be Integer
st v = v1 holds (Int-mult-left INT.Ring).(x,v) = x*v1;
registration
cluster non torsion for Z_Module;
end;
registration
let V be non torsion Z_Module;
cluster non torsion for VECTOR of V;
end;
definition
let V be Z_Module;
attr V is torsion-free means
:: ZMODUL06:def 3
for v being VECTOR of V st v <> 0.V holds v is non torsion;
end;
theorem :: ZMODUL06:15
V is Mult-cancelable iff V is torsion-free;
registration
cluster -> torsion-free for Mult-cancelable Z_Module;
end;
registration
cluster -> Mult-cancelable for torsion-free Z_Module;
end;
registration
cluster -> torsion-free for free Z_Module;
end;
registration
cluster torsion-free free for Z_Module;
end;
theorem :: ZMODUL06:16
for V being torsion-free Z_Module, v being VECTOR of V holds
v is torsion iff v = 0.V;
registration
let V be torsion-free Z_Module;
cluster -> torsion-free for Submodule of V;
end;
registration
let V be Z_Module;
cluster (0).V -> trivial;
end;
registration
cluster -> non torsion for non trivial torsion-free Z_Module;
end;
registration
cluster trivial for Z_Module;
end;
registration
let V be non trivial Z_Module;
cluster non zero for VECTOR of V;
end;
theorem :: ZMODUL06:17
v is non torsion iff Lin{v} is free & v <> 0.V;
registration
let V be non torsion Z_Module;
let v be non torsion VECTOR of V;
cluster Lin{v} -> free;
end;
theorem :: ZMODUL06:18
for V being Z_Module, A being Subset of V, v being VECTOR of V
st A is linearly-independent & v in A holds
v is non torsion;
theorem :: ZMODUL06:19
for u being object holds u in Lin{v} implies
ex i being Element of INT.Ring st u = i*v;
theorem :: ZMODUL06:20
v in Lin{v};
theorem :: ZMODUL06:21
i*v in Lin{v};
theorem :: ZMODUL06:22
Lin{0.V} = (0).V;
registration
let V be torsion-free Z_Module;
let v be VECTOR of V;
cluster Lin{v} -> free;
end;
theorem :: ZMODUL06:23
for A1, A2 being Subset of V
st A1 is linearly-independent & A2 is linearly-independent &
A1 /\ A2 = {} & A1 \/ A2 is linearly-dependent holds
Lin(A1) /\ Lin(A2) <> (0).V;
theorem :: ZMODUL06:24
for V being Z_Module, W being free Submodule of V,
I being Subset of V, v being VECTOR of V
st I is linearly-independent & Lin(I) = (Omega).W & v in I holds
(Omega).W = Lin(I \ {v}) + Lin{v} & Lin(I \ {v}) /\ Lin{v} = (0).V &
Lin(I \ {v}) is free & Lin{v} is free & v <> 0.V;
theorem :: ZMODUL06:25
for V being Z_Module, W being free Submodule of V holds
ex A being Subset of V st A is Subset of W &
A is linearly-independent & Lin(A) = (Omega).W;
theorem :: ZMODUL06:26
for V being Z_Module, W being finite-rank free Submodule of V holds
ex A being finite Subset of V st A is finite Subset of W &
A is linearly-independent & Lin(A) = (Omega).W & card(A) = rank(W);
theorem :: ZMODUL06:27
for V being torsion-free Z_Module, v1, v2 being VECTOR of V
st v1 <> 0.V & v2 <> 0.V & Lin{v1} /\ Lin{v2} <> (0).V
ex u being VECTOR of V st u <> 0.V & Lin{v1} /\ Lin{v2} = Lin{u};
theorem :: ZMODUL06:28
for V being torsion-free Z_Module, v1, v2 being VECTOR of V
st v1 <> 0.V & v2 <> 0.V & Lin{v1} /\ Lin{v2} <> (0).V
ex u being VECTOR of V st u <> 0.V & Lin{v1} + Lin{v2} = Lin{u};
theorem :: ZMODUL06:29
for V being torsion-free Z_Module, W being finite-rank free Submodule of V,
v, u being VECTOR of V
st v <> 0.V & u <> 0.V &
W /\ Lin{v} = (0).V & (W + Lin{u}) /\ Lin{v} <> (0).V &
Lin{u} /\ Lin{v} = (0).V
holds ex w1, w2 being VECTOR of V
st w1 <> 0.V & w2 <> 0.V &
(W + Lin{u}) + Lin{v} = (W + Lin{w1}) + Lin{w2} &
W /\ Lin{w1} <> (0).V & (W + Lin{w1}) /\ Lin{w2} = (0).V &
u in Lin{w1} + Lin{w2} & v in Lin{w1} + Lin{w2} &
w1 in Lin{u} + Lin{v} & w2 in Lin{u} + Lin{v};
theorem :: ZMODUL06:30
for V being torsion-free Z_Module, W being finite-rank free Submodule of V,
v being VECTOR of V
st v <> 0.V & W /\ Lin{v} <> (0).V holds
W + Lin{v} is free;
registration
let V be torsion-free Z_Module;
let v be VECTOR of V;
let W be finite-rank free Submodule of V;
cluster W + Lin{v} -> free;
end;
registration
let V be Z_Module;
let v be VECTOR of V;
let W be finitely-generated Submodule of V;
cluster W + Lin{v} -> finitely-generated;
end;
registration
let V be Z_Module;
let W1, W2 be finitely-generated Submodule of V;
cluster W1 + W2 -> finitely-generated;
end;
theorem :: ZMODUL06:31
for V being Z_Module, W being Submodule of V,
W1s, W2s being Submodule of W,
W1, W2 being Submodule of V
st W1s = W1 & W2s = W2
holds W1s + W2s = W1 + W2;
registration
let V be torsion-free Z_Module;
let U1, U2 be finite-rank free Submodule of V;
cluster U1 + U2 -> free;
end;
registration
cluster -> free for finitely-generated torsion-free Z_Module;
end;
begin :: 2. Rank of finite-rank free $\mathbb{Z}$-module
theorem :: ZMODUL06:32
for V being torsion-free Z_Module,
W1, W2 being finite-rank free Submodule of V
st W1 /\ W2 = (0).V holds rank(W1 + W2) = rank W1 + rank W2;
theorem :: ZMODUL06:33
for V being finite-rank free Z_Module,
W1, W2 being finite-rank free Submodule of V
st V is_the_direct_sum_of W1,W2 holds rank V = rank W1 + rank W2;
theorem :: ZMODUL06:34
for V being torsion-free Z_Module,
W1, W2 being finite-rank free Submodule of V holds
rank(W1 /\ W2) <= rank(W1);
theorem :: ZMODUL06:35
for V being torsion-free Z_Module, v being VECTOR of V st v <> 0.V
holds rank(Lin{v}) = 1;
theorem :: ZMODUL06:36
for V being Z_Module holds rank((0).V) = 0;
theorem :: ZMODUL06:37
for V being torsion-free Z_Module,
v, u being VECTOR of V st v <> 0.V & u <> 0.V & Lin{v} /\ Lin{u} <> (0).V
holds rank(Lin{v} + Lin{u}) = 1;
theorem :: ZMODUL06:38
for V being torsion-free Z_Module,
W being finite-rank free Submodule of V,
v being VECTOR of V st v <> 0.V & W /\ Lin{v} <> (0).V holds
rank(W + Lin{v}) = rank(W);
theorem :: ZMODUL06:39
for V being torsion-free Z_Module,
W1, W2 being finite-rank free Submodule of V,
v being VECTOR of V
st W1 /\ Lin{v} <> (0).V & W2 /\ Lin{v} <> (0).V
holds (W1 /\ W2) /\ Lin{v} <> (0).V;
theorem :: ZMODUL06:40
for V, W being Z_Module,
T be linear-transformation of V,W,
A being Subset of V
holds T.:(the carrier of Lin(A)) c= the carrier of Lin(T.: A);
theorem :: ZMODUL06:41
for X, Y be Z_Module, L be linear-transformation of X, Y
holds L.(0.X) = 0.Y;
theorem :: ZMODUL06:42
for X, Y be Z_Module, L be linear-transformation of X, Y
st L is bijective holds
ex K be linear-transformation of Y, X
st K = L" & K is bijective;
theorem :: ZMODUL06:43
for X, Y be Z_Module, l be Linear_Combination of X,
L be linear-transformation of X, Y st L is bijective
holds L@*l = l*L";
theorem :: ZMODUL06:44
for X, Y be Z_Module, X0 be Subset of X,
L be linear-transformation of X, Y,
l be Linear_Combination of L.:X0
st X0 = the carrier of X & L is one-to-one
holds L#l = l*L;
theorem :: ZMODUL06:45
for X, Y be Z_Module, A be Subset of X, L be linear-transformation of X, Y
st L is bijective
holds A is linearly-independent
iff L.:A is linearly-independent;
theorem :: ZMODUL06:46
for X, Y be Z_Module, A be Subset of X, T be linear-transformation of X, Y
st T is bijective holds
T.:(the carrier of Lin(A)) = the carrier of Lin(T.: A);
theorem :: ZMODUL06:47
for Y be Z_Module, A be Subset of Y
holds Lin(A) is strict Submodule of (Omega).Y;
theorem :: ZMODUL06:48
for X, Y be Z_Module, T be linear-transformation of X, Y
st T is bijective holds
X is free iff Y is free;
theorem :: ZMODUL06:49
for X, Y be free Z_Module, T be linear-transformation of X, Y,
A be Subset of X st T is bijective holds
A is Basis of X iff T.: A is Basis of Y;
theorem :: ZMODUL06:50
for X, Y be free Z_Module, T be linear-transformation of X, Y
st T is bijective holds
X is finite-rank iff Y is finite-rank;
theorem :: ZMODUL06:51
for X, Y be finite-rank free Z_Module, T be linear-transformation of X, Y
st T is bijective holds
rank(X) = rank(Y);
theorem :: ZMODUL06:52
for V being Z_Module, W being finite-rank free Submodule of V,
a being Element of INT.Ring st a <> 0.INT.Ring holds
rank(a (*) W) = rank(W);
theorem :: ZMODUL06:53
for V being Z_Module, W1, W2, W3 being finite-rank free Submodule of V,
a being Element of INT.Ring st a <> 0.INT.Ring & W3 = a (*) W1 holds
rank(W3 /\ W2) = rank(W1 /\ W2);
theorem :: ZMODUL06:54
for V being torsion-free Z_Module,
W1, W2, W3 being finite-rank free Submodule of V,
a being Element of INT.Ring st a <> 0.INT.Ring & W3 = a (*) W1 holds
rank(W3 + W2) = rank(W1 + W2);
theorem :: ZMODUL06:55
for V being torsion-free Z_Module,
W1, W2 being finite-rank free Submodule of V,
I being Basis of W1
st (for v being VECTOR of V st v in I holds (W1 /\ W2) /\ Lin{v} <> (0).V)
holds rank(W1 /\ W2) = rank(W1);
theorem :: ZMODUL06:56
for V being torsion-free Z_Module,
W1, W2 being finite-rank free Submodule of V,
I being Basis of W1
st rank(W1 /\ W2) < rank(W1) holds
ex v being VECTOR of V st v in I & (W1 /\ W2) /\ Lin{v} = (0).V;
theorem :: ZMODUL06:57
for V being torsion-free Z_Module,
W1, W2 being finite-rank free Submodule of V, I being Basis of W1
st rank(W1 /\ W2) = rank(W1) holds
(for v being VECTOR of V st v in I holds (W1 /\ W2) /\ Lin{v} <> (0).V);
theorem :: ZMODUL06:58
for V being torsion-free Z_Module,
W1, W2 being finite-rank free Submodule of V, I being Basis of W1
st (for v being VECTOR of V st v in I holds (W1 /\ W2) /\ Lin{v} <> (0).V)
holds rank(W1 + W2) = rank(W2);
theorem :: ZMODUL06:59
for V being torsion-free Z_Module,
W1, W2 being finite-rank free Submodule of V
st rank(W1 /\ W2) = rank(W1) holds
rank(W1 + W2) = rank(W2);
theorem :: ZMODUL06:60
for G be Field, V be VectSp of G, A being Subset of V
st A is linearly-independent holds
A is Basis of Lin(A);
theorem :: ZMODUL06:61
for V being Mult-cancelable finite-rank free Z_Module,
W1, W2 be finite-rank free Submodule of V holds
rank(W1 + W2) + rank(W1 /\ W2) = rank(W1) + rank(W2);
theorem :: ZMODUL06:62
for V being torsion-free Z_Module,
W1, W2 be finite-rank free Submodule of V holds
rank(W1 + W2) + rank(W1 /\ W2) = rank(W1) + rank(W2);
theorem :: ZMODUL06:63
for V being torsion-free Z_Module,
W1, W2 being finite-rank free Submodule of V
st rank(W1 + W2) = rank(W2) holds
rank(W1 /\ W2) = rank(W1);
theorem :: ZMODUL06:64
for V being torsion-free Z_Module,
W1, W2 being finite-rank free Submodule of V, v being VECTOR of V
st v <> 0.V & W1 /\ Lin{v} = (0).V & (W1 + W2) /\ Lin{v} = (0).V holds
rank((W1 + Lin{v}) /\ W2) = rank(W1 /\ W2);
theorem :: ZMODUL06:65
for V being torsion-free Z_Module, W being finite-rank free Submodule of V,
v being VECTOR of V st v <> 0.V & W /\ Lin{v} <> (0).V holds
rank(W /\ Lin{v}) = 1;
theorem :: ZMODUL06:66
for V being torsion-free Z_Module, W being finite-rank free Submodule of V,
v being VECTOR of V
st v <> 0.V & W /\ Lin{v} <> (0).V
holds
ex u being VECTOR of V st u <> 0.V & W /\ Lin{v} = Lin{u};
theorem :: ZMODUL06:67
for V being torsion-free Z_Module, W being finite-rank free Submodule of V,
u, v being VECTOR of V st W /\ Lin{v} = (0).V &
(W + Lin{u}) /\ Lin{v} <> (0).V
holds W /\ Lin{u} = (0).V;
theorem :: ZMODUL06:68
for V being torsion-free Z_Module,
W1, W2 being finite-rank free Submodule of V, v being VECTOR of V
st rank(W1 /\ W2) = rank(W1) & (W1 + W2) /\ Lin{v} <> (0).V holds
W2 /\ Lin{v} <> (0).V;
theorem :: ZMODUL06:69
for V being torsion-free Z_Module,
W1, W2, W3 being finite-rank free Submodule of V
st rank(W1 + W2) = rank(W2) & W3 is Submodule of W1
holds rank(W3 + W2) = rank(W2);
theorem :: ZMODUL06:70
for V being torsion-free Z_Module,
W1, W2 being finite-rank free Submodule of V, I being Basis of W1
st rank(W1 + W2) = rank(W2)
holds (for v being VECTOR of V st v in I holds (W1 /\ W2) /\ Lin{v} <> (0).V)
;
theorem :: ZMODUL06:71
for V being torsion-free Z_Module,
W1, W2 being finite-rank free Submodule of V
st rank(W1 /\ W2) = rank(W1)
holds ex a being Element of INT.Ring st a (*) W1 is Submodule of W2;