:: Torsion-part of $\mathbb Z$-module
:: by Yuichi Futa , Hiroyuki Okazaki and Yasunari Shidama
::
:: Received August 14, 2015
:: Copyright (c) 2015-2016 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies GAUSSINT, NUMBERS, 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, ZMODUL02, ZMODUL05, ZMODUL06, ZMODUL07, INT_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_4, VECTSP_5, VECTSP_6, VECTSP_7, MOD_2, BINOM, ZMODUL01, ZMODUL02,
ZMODUL03, GAUSSINT, ZMODUL05, ZMODUL06;
constructors BINOP_2, BINOM, UPROOTS, ORDERS_1, REALSET1, FINSEQOP, ALGSTR_1,
ZMODUL01, ZMODUL02, EC_PF_1, ZMODUL04, ZMODUL05, ZMODUL06;
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;
requirements REAL, NUMERALS, BOOLE, SUBSET, ARITHM;
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 :: ZMODUL07:1
for n being Integer st n <> 0 & n <> -1 & n <> -2
holds not n/(n+1) in INT;
registration
cluster prime non zero for Element of INT.Ring;
end;
registration
cluster prime -> non zero for Element of INT.Ring;
end;
theorem :: ZMODUL07:2
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));
theorem :: ZMODUL07:3
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;
theorem :: ZMODUL07:4
for V being finite-rank free Z_Module,
I being linearly-independent Subset of V
holds I is finite;
registration
let V be finite-rank free Z_Module;
cluster linearly-independent -> finite for Subset of V;
end;
theorem :: ZMODUL07:5
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);
theorem :: ZMODUL07:6
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);
theorem :: ZMODUL07:7
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));
theorem :: ZMODUL07:8
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;
theorem :: ZMODUL07:9
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;
theorem :: ZMODUL07:10
for V being finite-rank free Z_Module, W1, W2 being Submodule of V holds
rank(W1 /\ W2) >= rank W1 + rank W2 - rank V;
definition
let V be Z_Module;
func torsion_part(V) -> strict Submodule of V means
:: ZMODUL07:def 1
the carrier of it = { v where v is Vector of V : v is torsion };
end;
theorem :: ZMODUL07:11
for V being Z_Module, v being VECTOR of V holds
v is torsion iff v in torsion_part(V);
theorem :: ZMODUL07:12
for V being Z_Module holds
V is torsion-free iff torsion_part(V) = (0).V;
registration
let V be Z_Module;
cluster Z_ModuleQuot(V,torsion_part(V)) -> torsion-free;
end;
definition
let V be Z_Module;
let W be Submodule of V;
func ZQMorph(V, W) -> linear-transformation of V, Z_ModuleQuot(V,W)
means
:: ZMODUL07:def 2
for v being Element of V holds it.v = v + W;
end;
registration
let V be Z_Module, W be Submodule of V;
cluster ZQMorph(V,W) -> onto;
end;
theorem :: ZMODUL07:13
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));
registration
let V be finitely-generated Z_Module, W be Submodule of V;
cluster Z_ModuleQuot(V,W) -> finitely-generated;
end;
registration
let V be finitely-generated Z_Module;
cluster Z_ModuleQuot(V,torsion_part(V)) -> free;
end;
begin :: 2. $\mathbb Z$-module generated the rational number field
definition
func Rat-Module -> ModuleStr over INT.Ring equals
:: ZMODUL07:def 3
ModuleStr (# the carrier of F_Rat, the addF of F_Rat, the ZeroF of F_Rat,
Int-mult-left(F_Rat) #);
end;
registration
cluster Rat-Module -> non empty;
end;
registration
cluster Rat-Module -> Abelian add-associative
right_zeroed right_complementable scalar-distributive vector-distributive
scalar-associative scalar-unital;
end;
theorem :: ZMODUL07:14
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;
theorem :: ZMODUL07:15
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;
registration
cluster Rat-Module -> torsion-free;
end;
registration
cluster Rat-Module -> non trivial;
end;
theorem :: ZMODUL07:16
for s being Element of Rat-Module holds
Lin{s} <> Rat-Module;
theorem :: ZMODUL07:17
for s, t being Element of Rat-Module st s <> t
holds not {s,t} is linearly-independent;
registration
cluster Rat-Module -> non free;
end;
theorem :: ZMODUL07:18
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;
registration
cluster Rat-Module -> non finitely-generated;
end;
theorem :: ZMODUL07:19
for A being finite Subset of Rat-Module holds
rank(Lin(A)) <= 1;
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;
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
:: ZMODUL07:def 4
rank (im T);
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
:: ZMODUL07:def 5
rank (ker T);
end;
theorem :: ZMODUL07:20
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;
theorem :: ZMODUL07:21
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);
theorem :: ZMODUL07:22
for V, W being Z_Module, 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;
theorem :: ZMODUL07:23
for V, W being Z_Module,
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);
:: Rank-nullity theorem
theorem :: ZMODUL07:24
for V, W being finite-rank free Z_Module,
T being linear-transformation of V, W
holds rank V = rank(T) + nullity(T);
theorem :: ZMODUL07:25
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;
::: canonical decomposition
definition
let V, W be Z_Module;
let T be linear-transformation of V, W;
func Zdecom(T) -> linear-transformation of Z_ModuleQuot(V,ker T), im T
means
:: ZMODUL07:def 6
it is bijective &
for v being Element of V holds it.((ZQMorph(V,ker T)).v) = T.v;
end;
theorem :: ZMODUL07:26
for V, W being Z_Module, T being linear-transformation of V, W holds
T = Zdecom(T) * ZQMorph(V, ker T);
theorem :: ZMODUL07:27
for V, U, W being Z_Module,
f being linear-transformation of V, U,
g being linear-transformation of U, W holds
g*f is linear-transformation of V, W;
definition
let V, U, W be Z_Module,
f be linear-transformation of V, U,
g be linear-transformation of U, W;
redefine func g*f -> linear-transformation of V, W;
end;
theorem :: ZMODUL07:28
for V, W being Z_Module,
f being linear-transformation of V, W holds
the carrier of ker f = f"{0.W};
theorem :: ZMODUL07:29
for V, U, W being Z_Module,
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);
theorem :: ZMODUL07:30
for V, W being Z_Module, f being linear-transformation of V, W
st f is onto holds
im f = (Omega).W;
theorem :: ZMODUL07:31
for V being Z_Module, W being Submodule of V holds
ker ZQMorph(V, W) = (Omega).W;
theorem :: ZMODUL07:32
for V being Z_Module, W being Submodule of V, Ws being strict Submodule of V,
v being VECTOR of V st Ws = (Omega).W holds
v + W = v + Ws;
theorem :: ZMODUL07:33
for V being Z_Module, W being Submodule of V, Ws being strict Submodule of V,
A being object st Ws = (Omega).W holds
A is Coset of W iff A is Coset of Ws;
theorem :: ZMODUL07:34
for V being Z_Module, W being Submodule of V, Ws being strict Submodule of V
st Ws = (Omega).W holds
CosetSet(V, W) = CosetSet(V, Ws);
theorem :: ZMODUL07:35
for V being Z_Module, W being Submodule of V, Ws being strict Submodule of V
st Ws = (Omega).W holds
addCoset(V, W) = addCoset(V, Ws);
theorem :: ZMODUL07:36
for V being Z_Module, W being Submodule of V, Ws being strict Submodule of V
st Ws = (Omega).W holds
lmultCoset(V, W) = lmultCoset(V, Ws);
theorem :: ZMODUL07:37
for V being Z_Module, W being Submodule of V, Ws being strict Submodule of V
st Ws = (Omega).W holds
Z_ModuleQuot(V, W) = Z_ModuleQuot(V, Ws);
theorem :: ZMODUL07:38
for V, U being Z_Module, 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
Z_ModuleQuot(V, V1), Z_ModuleQuot(U, U1) st F is bijective;
theorem :: ZMODUL07:39
for V being Z_Module, 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
Z_ModuleQuot(W1 + W2, U1), Z_ModuleQuot(W1, U2)
st F is bijective;
theorem :: ZMODUL07:40
for V being Z_Module, W1 being Submodule of V, W2 being Submodule of W1,
U1 being Submodule of V, U2 being Submodule of Z_ModuleQuot(V, U1)
st U1 = W2 & U2 = Z_ModuleQuot(W1, W2)
holds ex F being linear-transformation of
Z_ModuleQuot(Z_ModuleQuot(V, U1), U2), Z_ModuleQuot(V, W1)
st F is bijective;
registration
let V be Z_Module;
let a be non zero Element of INT.Ring;
cluster Z_ModuleQuot(V, a (*) V) -> torsion;
end;
theorem :: ZMODUL07:41
for V being trivial Z_Module holds (Omega).V = (0).V;
theorem :: ZMODUL07:42
for V being Z_Module, v being VECTOR of V st v <> 0.V holds
Lin{v} is non trivial;
theorem :: ZMODUL07:43
ex V being Z_Module, p being Element of INT.Ring
st p <> 0.INT.Ring & Z_ModuleQuot(V, p (*) V) is non trivial;
registration
cluster non trivial for torsion Z_Module;
end;
registration
cluster non torsion-free for Z_Module;
end;
registration
let V be non torsion-free Z_Module;
cluster non zero torsion for Vector of V;
end;
registration
cluster non trivial for finitely-generated Z_Module;
end;
theorem :: ZMODUL07:44
for V being Z_Module holds
V is torsion-free iff (Omega).V is torsion-free;
registration
cluster -> non trivial for non torsion-free Z_Module;
end;
registration
cluster non trivial for finitely-generated torsion-free Z_Module;
end;
registration
let V be non trivial finitely-generated torsion-free Z_Module,
p be prime Element of INT.Ring;
cluster Z_ModuleQuot(V, p (*) V) -> non trivial;
end;
registration
cluster finitely-generated for torsion Z_Module;
end;
registration
cluster non trivial for finitely-generated torsion Z_Module;
end;
registration
let V be non trivial finitely-generated torsion-free Z_Module,
p be prime Element of INT.Ring;
cluster Z_ModuleQuot(V, p (*) V) -> finitely-generated torsion;
end;
registration
let V be non torsion Z_Module;
cluster Z_ModuleQuot(V, torsion_part(V)) -> non trivial;
end;