:: Free $\mathbb Z$-module
:: by Yuichi Futa , Hiroyuki Okazaki and Yasunari Shidama
::
:: Received August 6, 2012
:: Copyright (c) 2012-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 NUMBERS, FINSEQ_1, SUBSET_1, STRUCT_0, FUNCT_1, XBOOLE_0,
ALGSTR_0, RELAT_1, PARTFUN1, ARYTM_3, CARD_3, ORDINAL4, PRELAMB,
CLASSES1, XXREAL_0, TARSKI, CARD_1, SUPINF_2, 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, MSAFREE2,
INT_3, VECTSP_1, NEWTON, MONOID_0, VECTSP10, EC_PF_1, ZMODUL02, RLVECT_5,
INT_2, MESFUNC1, MOD_3;
notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, RELAT_1, FUNCT_1, ORDINAL1,
RELSET_1, PARTFUN1, BINOP_1, FUNCT_2, DOMAIN_1, FINSET_1, ORDERS_1,
CARD_1, CLASSES1, NUMBERS, XCMPLX_0, XXREAL_0, INT_1, NAT_1, FINSEQ_1,
FINSEQ_3, NEWTON, STRUCT_0, ALGSTR_0, GROUP_1, RLVECT_1, VECTSP_1,
VECTSP_2, VECTSP_4, INT_2, VECTSP_6, VECTSP_9, MATRLIN, INT_3, BINOM,
EC_PF_1, VECTSP_7, ZMODUL01, ZMODUL02;
constructors BINOP_2, BINOM, UPROOTS, RELSET_1, ORDERS_1, REALSET1, VECTSP_2,
RLVECT_2, REAL_1, CLASSES1, FUNCT_7, NAT_D, GR_CY_1, EUCLID, VECTSP_6,
VECTSP_9, VECTSP10, ALGSTR_1, ZMODUL01, ZMODUL02, BINOP_1, VECTSP_7,
VECTSP_4, NEWTON;
registrations SUBSET_1, FUNCT_1, RELSET_1, FUNCT_2, FINSET_1, NUMBERS,
XREAL_0, STRUCT_0, MEMBERED, FINSEQ_1, CARD_1, INT_1, XBOOLE_0, XXREAL_0,
NAT_1, INT_3, RELAT_1, ALGSTR_1, VECTSP_1, ZMODUL02, ORDINAL1, VECTSP_7,
ZMODUL01, VECTSP_2, MOD_3;
requirements REAL, NUMERALS, BOOLE, SUBSET, ARITHM;
begin :: 1. Free Z-module
reserve x, y, y1, y2 for set;
reserve V for Z_Module;
reserve u, v, w for Vector of V;
reserve F, G, H, I for FinSequence of V;
reserve W, W1, W2, W3 for Submodule of V;
registration
cluster non trivial for Z_Module;
end;
registration
let V be Z_Module;
cluster linearly-independent for finite Subset of V;
end;
theorem :: ZMODUL03:1
for u being Vector of V holds
ex l being Linear_Combination of V st l.u = 1 &
for v being Vector of V st v <> u holds l.v = 0;
theorem :: ZMODUL03:2
for G be Z_Module, i being Element of INT.Ring,
w be Element of INT, v be Element of G
st G = ModuleStr(# the carrier of INT.Ring, the addF of INT.Ring,
the ZeroF of INT.Ring, Int-mult-left(INT.Ring) #) & v = w
holds i*v = i*w;
definition
::$CD
:: let IT be Z_Module;
:: attr IT is free means :Def1:
:: ex A being Subset of IT
:: st A is linearly-independent & Lin(A) = the ModuleStr of IT;
end;
registration let V;
cluster (0).V -> free;
end;
registration
cluster strict free for Z_Module;
end;
registration
let V be Z_Module;
cluster strict free for Submodule of V;
end;
registration
let V be free Z_Module;
cluster base for Subset of V;
end;
definition
let V be free Z_Module;
mode Basis of V is base Subset of V;
::$CD
end;
registration
cluster -> Mult-cancelable for free Z_Module;
end;
registration
cluster free for non trivial Z_Module;
end;
reserve KL1, KL2 for Linear_Combination of V;
reserve X for Subset of V;
theorem :: ZMODUL03:3
X is linearly-independent & Carrier(KL1) c= X & Carrier(KL2) c= X
& Sum(KL1) = Sum(KL2) implies KL1 = KL2;
theorem :: ZMODUL03:4
for V being free 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 * v in Lin(B));
theorem :: ZMODUL03:5
for L being Linear_Combination of V for F, G being FinSequence of V
for P being Permutation of dom F st G = F*P holds
Sum(L (#) F) = Sum(L (#) G);
theorem :: ZMODUL03:6
for L being Linear_Combination of V for F being FinSequence of V st
Carrier(L) misses rng F holds Sum(L (#) F) = 0.V;
theorem :: ZMODUL03:7
for F being FinSequence of V st F is one-to-one
for L being Linear_Combination of V st Carrier(L) c= rng F holds
Sum(L (#) F) = Sum(L);
theorem :: ZMODUL03:8
for L being Linear_Combination of V for F being FinSequence of V holds
ex K being Linear_Combination of V st
Carrier(K) = rng F /\ Carrier(L) & L (#) F = K (#) F;
theorem :: ZMODUL03:9
for L being Linear_Combination of V for A being Subset of V
for F being FinSequence of V st rng F c= the carrier of Lin(A) holds
ex K being Linear_Combination of A st Sum(L (#) F) = Sum(K);
theorem :: ZMODUL03:10
for L being Linear_Combination of V for A being Subset of V st
Carrier(L) c= the carrier of Lin(A) holds
ex K being Linear_Combination of A st Sum(L) = Sum(K);
theorem :: ZMODUL03:11
for L being Linear_Combination of V st Carrier(L) c= the carrier
of W for K being Linear_Combination of W st K = L|the carrier of W holds
Carrier(L) = Carrier(K) & Sum(L) = Sum(K);
theorem :: ZMODUL03:12
for K being Linear_Combination of W holds
ex L being Linear_Combination of V st
Carrier(K) = Carrier(L) & Sum(K) = Sum(L);
theorem :: ZMODUL03:13
for L being Linear_Combination of V st
Carrier(L) c= the carrier of W
ex K being Linear_Combination of W
st Carrier(K) = Carrier(L) & Sum(K) = Sum (L);
theorem :: ZMODUL03:14
for V being free Z_Module for I being Basis of V, v being Vector of V
holds v in Lin(I);
theorem :: ZMODUL03:15
for A being Subset of W st A is linearly-independent holds
A is linearly-independent Subset of V;
theorem :: ZMODUL03:16
for A being Subset of V st A is linearly-independent &
A c= the carrier of W holds A is linearly-independent Subset of W;
theorem :: ZMODUL03:17
for V being Z_Module
for A being Subset of V st A is linearly-independent
for v being Vector of V st v in A for B being Subset of V st B = A \ {v}
holds not v in Lin(B);
theorem :: ZMODUL03:18
for V being free Z_Module for I being Basis of V
for A being non empty Subset of V st A misses I
for B being Subset of V st B = I \/ A holds B is linearly-dependent;
theorem :: ZMODUL03:19
for A being Subset of V st A c= the carrier of W holds
Lin(A) is Submodule of W;
theorem :: ZMODUL03:20
for A being Subset of V, B being Subset of W st A = B holds Lin(A) = Lin(B);
registration
let V be Z_Module, A be linearly-independent Subset of V;
cluster Lin(A) -> free;
end;
registration
let V be free Z_Module;
cluster (Omega).V -> strict free;
end;
begin :: Finite-rank free Z-module
definition
let IT be free Z_Module;
attr IT is finite-rank means
:: ZMODUL03:def 3
ex A being finite Subset of IT st A is Basis of IT;
end;
registration let V;
cluster (0).V -> finite-rank;
end;
registration
cluster strict finite-rank for free Z_Module;
end;
registration
let V be Z_Module;
cluster strict finite-rank for free Submodule of V;
end;
registration
let V be Z_Module, A be finite linearly-independent Subset of V;
cluster Lin(A) -> finite-rank;
end;
definition
let V be Z_Module;
attr V is finitely-generated means
:: ZMODUL03:def 4
ex A being finite Subset of V st Lin(A) = the ModuleStr of V;
end;
registration let V;
cluster (0).V -> finitely-generated;
end;
registration
cluster strict finitely-generated free for Z_Module;
end;
registration let V be finite-rank free Z_Module;
cluster -> finite for Basis of V;
end;
begin :: Rank of a finite-rank free Z-module
theorem :: ZMODUL03:21
for p being prime Element of INT.Ring,
V being free Z_Module, I being Basis of V,
u1, u2 being Vector of V
st u1 <> u2 & u1 in I & u2 in I holds
ZMtoMQV(V,p,u1) <> ZMtoMQV(V,p,u2);
theorem :: ZMODUL03:22
for p being prime Element of INT.Ring, V being Z_Module,
ZQ being VectSp of GF(p), vq being Vector of ZQ
st ZQ = Z_MQ_VectSp(V,p)
holds ex v being Vector of V st vq = ZMtoMQV(V,p,v);
theorem :: ZMODUL03:23
for p being prime Element of INT.Ring, V being Z_Module,
I being Subset of V,
lq being Linear_Combination of Z_MQ_VectSp(V,p)
holds ex l being Linear_Combination of I
st for v being Vector of V st v in I holds
ex w be Vector of V st w in I & w in ZMtoMQV(V,p,v)
& l.w = lq.(ZMtoMQV(V,p,v));
theorem :: ZMODUL03:24
for p being prime Element of INT.Ring, V being free Z_Module,
I being Basis of V,
lq being Linear_Combination of Z_MQ_VectSp(V,p)
holds ex l being Linear_Combination of I
st for v being Vector of V st v in I holds
l.v = lq.(ZMtoMQV(V,p,v));
theorem :: ZMODUL03:25
for p being prime Element of INT.Ring, V being free Z_Module,
I being Basis of V,
X be non empty Subset of Z_MQ_VectSp(V,p)
st X = {ZMtoMQV(V,p,u) where u is Vector of V : u in I} holds
ex F be Function of X, the carrier of V
st (for u be Vector of V st u in I holds F.(ZMtoMQV(V,p,u)) = u)
& F is one-to-one & dom F = X & rng F = I;
theorem :: ZMODUL03:26
for p being prime Element of INT.Ring, V being free Z_Module,
I being Basis of V holds
card ( {ZMtoMQV(V,p,u) where u is Vector of V : u in I} )
= card(I);
theorem :: ZMODUL03:27
for p being prime Element of INT.Ring, V being free Z_Module holds
ZMtoMQV(V,p,0. V) = 0.(Z_MQ_VectSp(V,p));
theorem :: ZMODUL03:28
for p being prime Element of INT.Ring, V being free Z_Module,
s,t be Element of V holds
ZMtoMQV(V,p,s)+ZMtoMQV(V,p,t) = ZMtoMQV(V,p,s+t);
theorem :: ZMODUL03:29
for p being prime Element of INT.Ring, V being free Z_Module,
s be FinSequence of V,
t be FinSequence of Z_MQ_VectSp(V,p)
st len s = len t & for i be Element of NAT
st i in dom s holds ex si be Vector of V
st si = s.i & t.i = ZMtoMQV(V,p,si) holds
Sum(t) = ZMtoMQV(V,p,Sum(s));
theorem :: ZMODUL03:30
for p being prime Element of INT.Ring, V being free Z_Module,
s be Element of V,
a be Element of INT.Ring,
b be Element of GF(p) st a = b holds
b*ZMtoMQV(V,p,s) = ZMtoMQV(V,p,a*s);
theorem :: ZMODUL03:31
for p being prime Element of INT.Ring,
V being free Z_Module, I being Basis of V,
l being Linear_Combination of I,
IQ being Subset of Z_MQ_VectSp(V,p),
lq being Linear_Combination of IQ
st IQ = {ZMtoMQV(V,p,u) where u is Vector of V : u in I} &
(for v being Vector of V st v in I holds
l.v = lq.(ZMtoMQV(V,p,v)) ) holds
Sum(lq) = ZMtoMQV(V,p,Sum(l));
theorem :: ZMODUL03:32
for p being prime Element of INT.Ring,
V being free Z_Module, I being Basis of V,
IQ being Subset of Z_MQ_VectSp(V,p)
st IQ = {ZMtoMQV(V,p,u) where u is Vector of V : u in I}
holds IQ is linearly-independent;
theorem :: ZMODUL03:33
for p being prime Element of INT.Ring, V being free Z_Module,
I being Subset of V,
IQ being Subset of Z_MQ_VectSp(V,p)
st IQ = {ZMtoMQV(V,p,u) where u is Vector of V : u in I} holds
(for s be FinSequence of V
st (for i be Element of NAT
st i in dom s holds ex si be Vector of V
st si=s.i & ZMtoMQV(V,p,si) in Lin(IQ))
holds ZMtoMQV(V,p,Sum(s)) in Lin(IQ));
theorem :: ZMODUL03:34
for p being prime Element of INT.Ring,
V being free Z_Module, I being Basis of V,
IQ being Subset of Z_MQ_VectSp(V,p),
l be Linear_Combination of I
st IQ = {ZMtoMQV(V,p,u) where u is Vector of V : u in I} holds
ZMtoMQV(V,p,Sum(l)) in Lin(IQ);
theorem :: ZMODUL03:35
for p being prime Element of INT.Ring,
V being free Z_Module, I being Basis of V,
IQ being Subset of Z_MQ_VectSp(V,p)
st IQ = {ZMtoMQV(V,p,u) where u is Vector of V : u in I} holds
IQ is Basis of Z_MQ_VectSp(V,p);
registration
let p be prime Element of INT.Ring, V be finite-rank free Z_Module;
cluster Z_MQ_VectSp(V,p) -> finite-dimensional;
end;
theorem :: ZMODUL03:36
for V be finite-rank free Z_Module
holds for A, B being Basis of V holds
card A = card B;
definition
let V be finite-rank free Z_Module;
func rank(V) -> Nat means
:: ZMODUL03:def 5
for I being Basis of V holds it = card I;
end;
theorem :: ZMODUL03:37
for p be prime Element of INT.Ring, V be finite-rank free Z_Module holds
rank V = dim Z_MQ_VectSp(V,p);