:: Submodule of free $\mathbb Z$-module
:: by Yuichi Futa , Hiroyuki Okazaki and Yasunari Shidama
::
:: Received December 31, 2013
:: Copyright (c) 2013-2021 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,
FUNCT_1, RAT_1, XBOOLE_0, ALGSTR_0, RELAT_1, ARYTM_3, CARD_3, RLSUB_2,
EQREL_1, PRELAMB, XXREAL_0, TARSKI, CARD_1, SUPINF_2, ARYTM_1, NAT_1,
FUNCT_2, FINSET_1, VALUED_1, RLSUB_1, BINOP_1, ZFMISC_1, INT_1, ORDINAL1,
RLVECT_2, ZMODUL01, ZMODUL03, RLVECT_3, RMOD_2, RANKNULL, MSAFREE2,
VECTSP_1, MESFUNC1, REALSET1, MONOID_0, VECTSP10, EC_PF_1, MOD_3,
ZMODUL02, RLVECT_5, ORDINAL2, ZMODUL04, INT_2, INT_3, 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, ORDINAL2, FINSET_1,
ORDERS_1, CARD_1, NUMBERS, XCMPLX_0, XXREAL_0, NAT_1, INT_1, INT_2,
RAT_1, REALSET1, FINSEQ_1, EQREL_1, STRUCT_0, ALGSTR_0, GROUP_1,
RLVECT_1, VECTSP_1, VECTSP_2, VECTSP_4, VECTSP_5, VECTSP_6, VECTSP_7,
VECTSP_9, MATRLIN, INT_3, EC_PF_1, ZMODUL01, ZMODUL02, ZMODUL03,
GAUSSINT, VECTSP10;
constructors BINOP_2, RELSET_1, ORDERS_1, REALSET1, GR_CY_1, VECTSP_6,
GROUP_1, REAL_1, RLVECT_2, VECTSP_2, VECTSP_9, VECTSP10, ALGSTR_1,
ZMODUL02, ORDINAL3, ZMODUL03, GAUSSINT, VECTSP_4, VECTSP_7, ZMODUL01,
VECTSP_5, INT_3, VFUNCT_1;
registrations SUBSET_1, FUNCT_1, RELSET_1, FUNCT_2, FINSET_1, NUMBERS,
XREAL_0, STRUCT_0, RLVECT_1, MEMBERED, FINSEQ_1, CARD_1, INT_1, XBOOLE_0,
ORDINAL1, XXREAL_0, NAT_1, INT_3, RELAT_1, ZMODUL02, GAUSSINT, EQREL_1,
RAT_1, XCMPLX_0, ZMODUL03, ZMODUL01, VECTSP_7;
requirements REAL, NUMERALS, BOOLE, SUBSET, ARITHM;
begin :: 1. Vector space of rational field generated by a free Z-module
reserve V for Z_Module;
reserve W, W1, W2 for Submodule of V;
theorem :: ZMODUL04:1
for R being Ring
for V being LeftMod of R, W1, W2 being Subspace of V,
WW1, WW2 being Subspace of W1 + W2
st WW1 = W1 & WW2 = W2 holds
W1 + W2 = WW1 + WW2;
theorem :: ZMODUL04:2
for R being Ring
for V being LeftMod of R, W1, W2 being Subspace of V,
WW1, WW2 being Subspace of W1 + W2
st WW1 = W1 & WW2 = W2 holds
W1 /\ W2 = WW1 /\ WW2;
registration ::: generalize for arbitrary products
let V be Z_Module;
cluster [:the carrier of V,INT \ {0}:] -> non empty;
end;
definition
let V be Z_Module;
assume V is Mult-cancelable;
func EQRZM(V) -> Equivalence_Relation of [:the carrier of V,INT \{0}:]
means
:: ZMODUL04:def 1
for S,T being object holds
[S,T] in it
iff ( S in [:the carrier of V,INT \{0}:]
& T in [:the carrier of V,INT \{0}:]
& ex z1,z2 be Element of V,i1,i2 be Element of INT.Ring
st S=[z1,i1] & T=[z2,i2] & i1 <> 0 & i2 <> 0 & i2*z1 = i1*z2);
end;
theorem :: ZMODUL04:3
for V be Z_Module,
z1, z2 be Element of V, i1, i2 be Element of INT.Ring
st V is Mult-cancelable holds
[[z1,i1],[z2,i2]] in EQRZM(V) iff
i1 <> 0 & i2 <> 0 & i2*z1 = i1*z2;
definition
let V be Z_Module;
assume V is Mult-cancelable;
func addCoset(V) -> BinOp of Class EQRZM(V) means
:: ZMODUL04:def 2
for A, B be object st A in Class EQRZM(V) & B in Class EQRZM(V) holds
for z1,z2 be Element of V,i1,i2 be Element of INT.Ring
st i1 <> 0.INT.Ring & i2 <> 0.INT.Ring
& A=Class(EQRZM(V),[z1,i1]) & B=Class(EQRZM(V),[z2,i2]) holds
it.(A,B) = Class(EQRZM(V),[i2*z1+i1*z2,i1*i2]);
end;
definition
let V be Z_Module;
assume V is Mult-cancelable;
func zeroCoset(V) -> Element of Class EQRZM(V) means
:: ZMODUL04:def 3
for i be Integer st i <> 0 holds it = Class(EQRZM(V),[0.V,i]);
end;
definition
let V be Z_Module;
assume V is Mult-cancelable;
func lmultCoset(V) -> Function of
[:the carrier of F_Rat, Class EQRZM(V):], Class EQRZM(V) means
:: ZMODUL04:def 4
for q be object, A be object st q in RAT & A in Class EQRZM(V) holds
for m,n,i be Integer, mm being Element of INT.Ring, z be Element of V
st m = mm & n <> 0 & q = m / n & i <> 0 & A = Class(EQRZM(V),[z,i])
holds it.(q,A) = Class(EQRZM(V),[mm*z,n*i]);
end;
theorem :: ZMODUL04:4
for V be Z_Module,
z be Element of V,
i, n be Element of INT.Ring
st i <> 0.INT.Ring & n <> 0.INT.Ring & V is Mult-cancelable holds
Class(EQRZM(V),[z,i]) = Class(EQRZM(V),[n*z,n*i]);
theorem :: ZMODUL04:5
for V be Z_Module,
v be Element of
ModuleStr (# Class EQRZM(V), addCoset(V), zeroCoset(V), lmultCoset(V) #)
st V is Mult-cancelable holds
ex i be Element of INT.Ring, z be Element of V
st i <> 0.INT.Ring & v = Class(EQRZM(V),[z,i]);
definition
let V be Z_Module;
assume V is Mult-cancelable;
func Z_MQ_VectSp(V) -> VectSp of F_Rat equals
:: ZMODUL04:def 5
ModuleStr (# Class EQRZM(V), addCoset(V), zeroCoset(V), lmultCoset(V) #);
end;
definition
let V be Z_Module;
assume V is Mult-cancelable;
func MorphsZQ(V) -> Function of V, Z_MQ_VectSp(V) means
:: ZMODUL04:def 6
it is one-to-one
& (for v be Element of V holds it.v = Class(EQRZM(V),[v,1]) )
& (for v,w be Element of V holds it.(v+w) = it.v + it.w)
& (for v be Element of V, i be Element of INT.Ring, q be Element of F_Rat
st i = q holds it.(i*v) = q*(it.v) )
& it.(0.V) = 0.(Z_MQ_VectSp(V));
end;
theorem :: ZMODUL04:6
for V be Z_Module st V is Mult-cancelable holds
for s be FinSequence of V,
t be FinSequence of Z_MQ_VectSp(V)
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 = (MorphsZQ(V)).si holds
Sum(t) = (MorphsZQ(V)).Sum(s);
theorem :: ZMODUL04:7
for V be Z_Module,
I being Subset of V,
IQ being Subset of Z_MQ_VectSp(V),
l be Linear_Combination of I,
lq being Linear_Combination of IQ
st V is Mult-cancelable
& IQ =(MorphsZQ(V)).:I
& l = lq*MorphsZQ(V) holds
Sum(lq) = (MorphsZQ(V)).(Sum(l));
theorem :: ZMODUL04:8
for V be Z_Module, IQ being Subset of Z_MQ_VectSp(V) holds
for lq being Linear_Combination of IQ holds
ex m be Integer, a be Element of F_Rat
st m <> 0 & m = a & rng (a * lq) c= INT;
theorem :: ZMODUL04:9
for V be Z_Module,
I being Subset of V,
IQ being Subset of Z_MQ_VectSp(V),
lq being Linear_Combination of IQ
st V is Mult-cancelable & IQ =(MorphsZQ(V)).:(I) holds
ex m be Element of INT.Ring, a be Element of F_Rat,
l be Linear_Combination of I
st m <> 0.INT.Ring & m = a & l = (a * lq) * (MorphsZQ(V))
& (MorphsZQ(V))"Carrier(lq) = Carrier(l);
theorem :: ZMODUL04:10
for V be Z_Module,
I being Subset of V,
IQ being Subset of Z_MQ_VectSp(V),
lq being Linear_Combination of IQ,
m be Integer, a be Element of F_Rat,
l be Linear_Combination of I
st V is Mult-cancelable & IQ =(MorphsZQ(V)).:(I)
& m <> 0 & m = a
& l = (a * lq) *(MorphsZQ(V))
holds a*(Sum(lq)) = (MorphsZQ(V)).(Sum(l));
theorem :: ZMODUL04:11
for V be Z_Module,
I being Subset of V,
IQ being Subset of Z_MQ_VectSp(V)
st V is Mult-cancelable & IQ =(MorphsZQ(V)).:(I)
& I is linearly-independent
holds IQ is linearly-independent;
theorem :: ZMODUL04:12
for V be Z_Module,
I being Subset of V,
l being Linear_Combination of I,
IQ being Subset of Z_MQ_VectSp(V)
st V is Mult-cancelable & IQ =(MorphsZQ(V)).:I holds
ex lq be Linear_Combination of IQ
st l = lq*(MorphsZQ(V)) &
Carrier(lq) = (MorphsZQ(V)).:(Carrier(l));
theorem :: ZMODUL04:13
for V be free Z_Module,
I being Subset of V,
IQ being Subset of Z_MQ_VectSp(V),
l be Linear_Combination of I,
i be Element of INT.Ring
st i <> 0.INT.Ring & IQ =(MorphsZQ(V)).:I
holds Class(EQRZM(V),[Sum(l),i]) in Lin(IQ);
theorem :: ZMODUL04:14
for V be free Z_Module,
I being Subset of V,
IQ being Subset of Z_MQ_VectSp(V)
st IQ =(MorphsZQ(V)).:I
holds card(I) = card(IQ);
theorem :: ZMODUL04:15
for V be free Z_Module,
I being Subset of V,
IQ being Subset of Z_MQ_VectSp(V)
st IQ =(MorphsZQ(V)).:I & I is Basis of V
holds IQ is Basis of Z_MQ_VectSp(V);
registration
let V be finite-rank free Z_Module;
cluster Z_MQ_VectSp(V) -> finite-dimensional;
end;
theorem :: ZMODUL04:16
for V be finite-rank free Z_Module holds
rank V = dim Z_MQ_VectSp(V);
theorem :: ZMODUL04:17
for V be free Z_Module, I, A be finite Subset of V
st I is Basis of V & card (I) + 1 = card (A)
holds A is linearly-dependent;
theorem :: ZMODUL04:18
for V be free Z_Module, A, B be Subset of V
st A is linearly-dependent & A c= B
holds B is linearly-dependent;
theorem :: ZMODUL04:19
for V be free Z_Module,D,A be Subset of V
st D is Basis of V & D is finite & card (D) c< card(A)
holds A is linearly-dependent;
theorem :: ZMODUL04:20
for V be free Z_Module, I, A be Subset of V
st I is Basis of V & I is finite & A is linearly-independent
holds card (A) c= card (I);
begin :: 2. Subspace of free $\mathbb Z$-module
theorem :: ZMODUL04:21
for V being Z_Module st (Omega).V is free holds V is free;
theorem :: ZMODUL04:22
for R being Ring
for V being LeftMod of R, W1, W2 being Subspace of V,
W1s, W2s being strict Subspace of V st W1s = (Omega).W1 & W2s = (Omega).W2
holds W1s + W2s = W1 + W2;
theorem :: ZMODUL04:23
for R being Ring
for V being LeftMod of R, W1, W2 being Subspace of V,
W1s, W2s being strict Subspace of V st W1s = (Omega).W1 & W2s = (Omega).W2
holds W1s /\ W2s = W1 /\ W2;
theorem :: ZMODUL04:24
for R being Ring
for V be LeftMod of R, W be strict Subspace of V st W <> (0).V holds
ex v be Vector of V st v in W & v <> 0.V;
theorem :: ZMODUL04:25
for K being Ring
for V being VectSp of K
for A being Subset of V, l1, l2 being Linear_Combination of A
st Carrier(l1) /\ Carrier(l2) = {} holds
Carrier(l1 + l2) = Carrier(l1) \/ Carrier(l2);
theorem :: ZMODUL04:26
for R being Ring
for V being VectSp of R
for A1, A2 being Subset of V, l being Linear_Combination of A1 \/ A2
st A1 /\ A2 = {} holds
ex l1 being Linear_Combination of A1, l2 being Linear_Combination of A2
st l = l1 + l2;
theorem :: ZMODUL04:27
for V being Z_Module, W1, W2 being free Subspace of V,
I1 being Basis of W1, I2 being Basis of W2 st V is_the_direct_sum_of W1,W2
holds I1 /\ I2 = {};
theorem :: ZMODUL04:28
for V being Z_Module, W1, W2 being free Subspace of V,
I1 being Basis of W1, I2 being Basis of W2, I being Subset of V
st V is_the_direct_sum_of W1,W2 & I = I1 \/ I2
holds Lin(I) = the ModuleStr of V;
theorem :: ZMODUL04:29
for V being LeftMod of INT.Ring, W1, W2 being free Subspace of V,
I1 being Basis of W1, I2 being Basis of W2, I being Subset of V
st V is_the_direct_sum_of W1,W2 & I = I1 \/ I2
holds I is linearly-independent;
theorem :: ZMODUL04:30
for V being Z_Module, W1, W2 being free Subspace of V
st V is_the_direct_sum_of W1,W2
holds V is free;
theorem :: ZMODUL04:31
for V being Z_Module, W1, W2 being free Subspace of V
st W1 /\ W2 = (0).V holds
W1 + W2 is free;
theorem :: ZMODUL04:32
for V being free Z_Module, I being Basis of V, v being Vector of V
st v in I holds
Lin(I \ {v}) is free & Lin{v} is free;
theorem :: ZMODUL04:33
for V being free Z_Module, I being Basis of V, v being Vector of V
st v in I holds
V is_the_direct_sum_of Lin(I \ {v}),Lin{v};
registration
let V be finite-rank free Z_Module;
cluster -> free for Subspace of V;
end;
theorem :: ZMODUL04:34
for V being Z_Module, W being Subspace of V,
W1, W2 being free Subspace of V st
W1 /\ W2 = (0).V & the ModuleStr of W = W1 + W2
holds W is free;
theorem :: ZMODUL04:35
for p being prime Element of INT.Ring, V being free Z_Module
st Z_MQ_VectSp(V,p) is finite-dimensional
holds V is finite-rank;
theorem :: ZMODUL04:36
for p being prime Element of INT.Ring, V being Z_Module,
s be Element of V, a be Element of INT.Ring, b be Element of GF(p)
st b = a mod p holds
b*ZMtoMQV(V,p,s) = ZMtoMQV(V,p,a*s);
theorem :: ZMODUL04:37
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),
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 :: ZMODUL04:38
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 Lin(I) = the ModuleStr of V &
IQ = {ZMtoMQV(V,p,u) where u is Vector of V : u in I} holds
Lin(IQ) = the ModuleStr of Z_MQ_VectSp(V,p);
theorem :: ZMODUL04:39
for V being finitely-generated free Z_Module
holds ex A being finite Subset of V st A is Basis of V;
registration
cluster -> finite-rank for finitely-generated free Z_Module;
end;
registration
cluster -> finitely-generated for finite-rank free Z_Module;
end;
theorem :: ZMODUL04:40
for V be finite-rank free Z_Module holds for A being Subset of V
st A is linearly-independent holds A is finite;
registration
let V be Z_Module, W1, W2 be finite-rank free Subspace of V;
cluster W1 /\ W2 -> free;
end;
registration
let V be Z_Module, W1, W2 be finite-rank free Subspace of V;
cluster W1 /\ W2 -> finite-rank;
end;
registration
let V be finite-rank free Z_Module;
cluster -> finite-rank for Subspace of V;
end;