:: 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-2018 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, FUNCSDOM,
VECTSP_2, BINOP_1, LATTICES, VECTSP10;
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_2, VECTSP_4,
VECTSP_5, VECTSP_6, INT_3, VECTSP_7, VECTSP_9, VECTSP10, MATRLIN, BINOM,
ZMODUL01, ZMODUL02, RANKNULL, 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, RANKNULL;
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, VECTSP10, VECTSP11, VECTSP_1;
requirements REAL, NUMERALS, BOOLE, SUBSET, ARITHM;
begin :: 1. Torsion $\mathbb{Z}$-module and torsion-free $\mathbb{Z}$-module
theorem :: ZMODUL06:1
for R being commutative Ring
for V being LeftMod of R, W being Subspace of V
holds (1.R) (*) W = (Omega).W;
theorem :: ZMODUL06:2
for R being Ring
for V being LeftMod of R, W1, W2, W3 being Subspace of V holds
W1 /\ W2 is Subspace of (W1 + W3) /\ W2;
theorem :: ZMODUL06:3
for R being Ring
for V being LeftMod of R, W1, W2, W3 being Subspace 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 Subspace of V;
reserve v, u for Vector of V;
reserve i for Element of INT.Ring;
definition
let R be Ring;
let V be LeftMod of R, v be Vector of V;
attr v is torsion means
:: ZMODUL06:def 1
ex i being Element of R st i <> 0.R & 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 Subspace of V;
end;
registration
let R be Ring;
let V be LeftMod of R;
cluster (0).V -> trivial;
end;
registration
cluster -> non torsion for non trivial torsion-free Z_Module;
end;
registration
let R be Ring;
cluster trivial for LeftMod of R;
end;
registration
let K be Abelian add-associative right_zeroed right_complementable
associative left_unital distributive non degenerated
non empty doubleLoopStr;
cluster Abelian add-associative right_zeroed right_complementable
vector-distributive scalar-distributive scalar-associative scalar-unital
strict for non trivial ModuleStr over K;
end;
registration
let R be non degenerated non empty Ring;
let V be non trivial LeftMod of R;
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
for R being Ring
for V being LeftMod of R holds
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 Subspace 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 Subspace 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 Subspace 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 Subspace 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 Subspace 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 Subspace 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 Subspace of V;
cluster W + Lin{v} -> finitely-generated;
end;
registration
let V be Z_Module;
let W1, W2 be finitely-generated Subspace of V;
cluster W1 + W2 -> finitely-generated;
end;
theorem :: ZMODUL06:31
for R being Ring
for V being LeftMod of R, W being Subspace of V,
W1s, W2s being Subspace of W,
W1, W2 being Subspace 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 Subspace 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 Subspace 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 Subspace 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 Subspace 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 Subspace 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 Subspace 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 R being Ring
for V, W being LeftMod of R,
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 R being Ring
for X, Y be LeftMod of R, L be linear-transformation of X, Y
holds L.(0.X) = 0.Y;
theorem :: ZMODUL06:42
for R being Ring
for X, Y be LeftMod of R, 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 R being Ring
for X, Y be LeftMod of R, 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 R being Ring
for X, Y be LeftMod of R, 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 R being Ring
for X, Y be LeftMod of R, 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 R being Ring
for X, Y be LeftMod of R, 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 R being Ring
for Y be LeftMod of R, A be Subset of Y
holds Lin(A) is strict Subspace of (Omega).Y;
theorem :: ZMODUL06:48
for R being Ring
for X, Y be LeftMod of R, 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 Subspace 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 Subspace 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 Subspace 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 Subspace 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 Subspace 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 Subspace 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 Subspace 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 Subspace 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 Subspace 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 Subspace 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 Subspace 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 Subspace 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 Subspace 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 Subspace 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 Subspace 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 Subspace 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 Subspace of V
st rank(W1 + W2) = rank(W2) & W3 is Subspace of W1
holds rank(W3 + W2) = rank(W2);
theorem :: ZMODUL06:70
for V being torsion-free Z_Module,
W1, W2 being finite-rank free Subspace 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 Subspace of V
st rank(W1 /\ W2) = rank(W1)
holds ex a being Element of INT.Ring st a (*) W1 is Subspace of W2;