:: Quotient Module of $\mathbb Z$-module
:: by Yuichi Futa , Hiroyuki Okazaki and Yasunari Shidama
::
:: Received May 7, 2012
:: Copyright (c) 2012-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 NUMBERS, FINSEQ_1, SUBSET_1, RLVECT_1, STRUCT_0, FUNCT_1,
XBOOLE_0, ALGSTR_0, RELAT_1, ARYTM_3, CARD_3, ORDINAL4, XXREAL_0, TARSKI,
CARD_1, SUPINF_2, ARYTM_1, NAT_1, FUNCT_2, FINSET_1, VALUED_1, RLSUB_1,
QC_LANG1, BINOP_1, ZFMISC_1, INT_1, RLVECT_2, ZMODUL01, ZMODUL02,
RLVECT_3, RMOD_2, INT_3, VECTSP_1, VECTSP_2, LOPBAN_1, MESFUNC1,
REALSET1, RSSPACE, MONOID_0, SETFAM_1, VECTSP10, EC_PF_1, INT_2,
ORDINAL1, FUNCSDOM, XCMPLX_0;
notations TARSKI, XBOOLE_0, ENUMSET1, ZFMISC_1, SUBSET_1, RELAT_1, FUNCT_1,
ORDINAL1, RELSET_1, PARTFUN1, FUNCT_2, BINOP_1, DOMAIN_1, FUNCOP_1,
FINSET_1, CARD_1, NUMBERS, XCMPLX_0, XXREAL_0, NAT_1, INT_1, INT_2,
REALSET1, FINSEQ_1, VALUED_1, FINSEQ_4, STRUCT_0, ALGSTR_0, RLVECT_1,
VECTSP_1, RLVECT_2, INT_3, EC_PF_1, GROUP_1, VFUNCT_1, VECTSP_2,
VECTSP_4, VECTSP_5, VECTSP_6, VECTSP_7, ZMODUL01, VECTSP10;
constructors BINOP_2, FINSEQ_4, RELSET_1, RLVECT_2, ZMODUL01, VECTSP_4,
REALSET1, FUNCT_7, INT_3, NAT_D, GCD_1, VECTSP10, ALGSTR_1, VECTSP_6,
BINOP_1, VECTSP_7, VECTSP_5, PARTFUN1, DOMAIN_1, FUNCOP_1, XXREAL_0,
NAT_1, MEMBERED, VFUNCT_1;
registrations RELSET_1, FINSET_1, XREAL_0, STRUCT_0, INT_1, ZMODUL01,
XXREAL_0, ALGSTR_0, INT_3, VECTSP_1, XCMPLX_0, ORDINAL1, VECTSP_7,
MEMBERED;
requirements REAL, NUMERALS, BOOLE, SUBSET;
begin :: 1. Quotient module of Z-module and vector space
reserve x, y, y1, y2 for set;
reserve R for Ring;
reserve V for LeftMod of R;
reserve u, v, w for VECTOR of V;
reserve F, G, H, I for FinSequence of V;
reserve i, j, k, n for Element of NAT;
reserve f, f9, g for sequence of V;
definition
let R be Ring;
let V be LeftMod of R;
let a be Element of R;
func a * V -> non empty Subset of V equals
:: ZMODUL02:def 1
the set of all a * v where v is Element of V;
end;
definition
let R be Ring;
let V be LeftMod of R;
let a be Element of R;
func Zero_(a,V) -> Element of a*V equals
:: ZMODUL02:def 2
0.V;
end;
definition
let R be Ring;
let V be LeftMod of R;
let a be Element of R;
func Add_(a,V) -> Function of [:a*V,a*V :], a*V equals
:: ZMODUL02:def 3
(the addF of V) | [:a*V,a*V:];
end;
definition
let R be commutative Ring;
let V be VectSp of R;
let a be Element of R;
func Mult_(a,V) -> Function of [:the carrier of R,a*V :], a*V equals
:: ZMODUL02:def 4
(the lmult of V) | [:the carrier of R, a*V:];
end;
definition
let R be commutative Ring;
let V be LeftMod of R;
let a be Element of R;
func a (*) V -> Subspace of V equals
:: ZMODUL02:def 5
ModuleStr (# a * V, Add_(a,V), Zero_(a,V), Mult_(a,V) #);
end;
definition
::$CD 5
end;
theorem :: ZMODUL02:1
for p be Element of INT.Ring, V be Z_Module, W be Submodule of V,
x be VECTOR of VectQuot(V, W) st W = p (*) V
holds p * x = 0.VectQuot(V, W);
theorem :: ZMODUL02:2
for p, i be Element of INT.Ring, V be Z_Module, W be Submodule of V,
x be VECTOR of VectQuot(V, W)
st p <> 0 & W = p (*) V
holds i * x = (i mod p) * x;
theorem :: ZMODUL02:3
for p, q be Element of INT.Ring, V be Z_Module, W be Submodule of V,
v be VECTOR of V
st W = p (*) V & p > 1 & q > 1 & p,q are_coprime
holds q * v = 0.V implies v + W = 0.VectQuot(V, W);
registration
cluster prime for Element of INT.Ring;
end;
registration
cluster prime -> natural for integer Number;
end;
definition
let p be prime Element of INT.Ring;
let V be Z_Module;
func Mult_Mod_pV(V,p) -> Function of
[:the carrier of GF(p), the carrier of VectQuot(V,p(*)V):],
the carrier of VectQuot(V,p(*)V) means
:: ZMODUL02:def 11
for a being Element of GF(p), i being Element of INT.Ring,
x being Element of VectQuot(V,p(*)V) st a = i mod p
holds it.(a,x) = (i mod p) * x;
end;
definition
let p be prime Element of INT.Ring, V be Z_Module;
func Z_MQ_VectSp(V,p) -> non empty strict ModuleStr over GF(p) equals
:: ZMODUL02:def 12
ModuleStr (# the carrier of VectQuot(V,p(*)V),
the addF of VectQuot(V,p(*)V), the ZeroF of VectQuot(V,p(*)V),
Mult_Mod_pV(V,p) #);
end;
registration
let p be prime Element of INT.Ring, V be Z_Module;
cluster Z_MQ_VectSp(V,p) -> scalar-distributive vector-distributive
scalar-associative scalar-unital add-associative right_zeroed
right_complementable Abelian;
end;
definition
let p be prime Element of INT.Ring, V be Z_Module, v be VECTOR of V;
func ZMtoMQV(V,p,v) -> Vector of Z_MQ_VectSp(V,p) equals
:: ZMODUL02:def 13
v + p(*)V;
end;
definition
let R be Ring; let X be LeftMod of R;
func Mult_INT*(X) -> Function of
[:the carrier of R,the carrier of X:], the carrier of X equals
:: ZMODUL02:def 14
the lmult of X;
end;
definition
let R be Ring;
let X be LeftMod of R;
func modetrans(X) -> non empty strict ModuleStr over R equals
:: ZMODUL02:def 15
ModuleStr (#the carrier of X, the addF of X, the ZeroF of X, Mult_INT*(X) #);
end;
registration
let R be Ring; let X be LeftMod of R;
cluster modetrans(X) -> Abelian add-associative right_zeroed
right_complementable vector-distributive scalar-distributive
scalar-associative scalar-unital;
end;
definition
::$CD 13
end;
::$CT 4
begin :: 2. Linear combination of Z-module
reserve K,L,L1,L2,L3 for Linear_Combination of V;
theorem :: ZMODUL02:8
for R being Ring
for V be LeftMod of R, L be Linear_Combination of V,
v be Element of V holds L.v = 0.R iff not v in Carrier(L);
theorem :: ZMODUL02:9
for R being Ring
for V be LeftMod of R, v be Element of V holds (ZeroLC(V)).v = 0.R;
reserve a, b for Element of R;
reserve G, H1, H2, F, F1, F2, F3 for FinSequence of V;
reserve A, B for Subset of V,
v1, v2, v3, u1, u2, u3 for Vector of V,
f for Function of V, R,
i for Element of NAT;
reserve l, l1, l2 for Linear_Combination of A;
theorem :: ZMODUL02:10
A c= B implies l is Linear_Combination of B;
theorem :: ZMODUL02:11
ZeroLC(V) is Linear_Combination of A;
theorem :: ZMODUL02:12
for l being Linear_Combination of {}the carrier of V holds l = ZeroLC(V);
theorem :: ZMODUL02:13
i in dom F & v = F.i implies (f (#) F).i = f.v * v;
theorem :: ZMODUL02:14
f (#) <*>(the carrier of V) = <*>(the carrier of V);
theorem :: ZMODUL02:15
f (#) <* v *> = <* f.v * v *>;
theorem :: ZMODUL02:16
f (#) <* v1,v2 *> = <* f.v1 * v1, f.v2 * v2 *>;
theorem :: ZMODUL02:17
f (#) <* v1,v2,v3 *> = <* f.v1 * v1, f.v2 * v2, f.v3 * v3 *>;
theorem :: ZMODUL02:18
R is non degenerated implies
(A <> {} & A is linearly-closed iff for l holds Sum(l) in A);
theorem :: ZMODUL02:19
Sum(ZeroLC(V)) = 0.V;
theorem :: ZMODUL02:20
for l being Linear_Combination of {}(the carrier of V) holds Sum(l) = 0.V;
theorem :: ZMODUL02:21
for l being Linear_Combination of {v} holds Sum(l) = l.v * v;
theorem :: ZMODUL02:22
v1 <> v2 implies for l being Linear_Combination of {v1,v2} holds
Sum(l) = l.v1 * v1 + l.v2 * v2;
theorem :: ZMODUL02:23
Carrier(L) = {} implies Sum(L) = 0.V;
theorem :: ZMODUL02:24
Carrier(L) = {v} implies Sum(L) = L.v * v;
theorem :: ZMODUL02:25
Carrier(L) = {v1,v2} & v1 <> v2 implies Sum(L) = L.v1 * v1 + L.v2 * v2;
theorem :: ZMODUL02:26
Carrier(L1 + L2) c= Carrier(L1) \/ Carrier(L2);
theorem :: ZMODUL02:27
L1 is Linear_Combination of A & L2 is Linear_Combination of A
implies L1 + L2 is Linear_Combination of A;
theorem :: ZMODUL02:28
L1 + (L2 + L3) = L1 + L2 + L3;
registration let R,V,L;
reduce L + ZeroLC(V) to L;
end;
theorem :: ZMODUL02:29
for V being Z_Module,
a being Element of INT.Ring,
L being Linear_Combination of V holds
a <> 0.INT.Ring implies Carrier(a * L) = Carrier(L);
theorem :: ZMODUL02:30
0.R * L = ZeroLC(V);
theorem :: ZMODUL02:31
L is Linear_Combination of A implies a * L is Linear_Combination of A;
theorem :: ZMODUL02:32
(a + b) * L = a * L + b * L;
theorem :: ZMODUL02:33
a * (L1 + L2) = a * L1 + a * L2;
theorem :: ZMODUL02:34
a * (b * L) = (a * b) * L;
registration let R,V,L;
reduce (1.R)*L to L;
end;
theorem :: ZMODUL02:35
(- L).v = - L.v;
theorem :: ZMODUL02:36
L1 + L2 = ZeroLC(V) implies L2 = - L1;
theorem :: ZMODUL02:37
Carrier(- L) = Carrier(L);
theorem :: ZMODUL02:38
L is Linear_Combination of A
implies - L is Linear_Combination of A;
theorem :: ZMODUL02:39
(L1 - L2).v = L1.v - L2.v;
theorem :: ZMODUL02:40
Carrier(L1 - L2) c= Carrier(L1) \/ Carrier(L2);
theorem :: ZMODUL02:41
L1 is Linear_Combination of A & L2 is Linear_Combination of A implies
L1 - L2 is Linear_Combination of A;
theorem :: ZMODUL02:42
L - L = ZeroLC(V);
definition
let R,V;
func LinComb(V) -> set means
:: ZMODUL02:def 29
x in it iff x is Linear_Combination of V;
end;
registration
let R,V;
cluster LinComb(V) -> non empty;
end;
reserve e, e1, e2 for Element of LinComb(V);
definition
let R,V, e;
func @e -> Linear_Combination of V equals
:: ZMODUL02:def 30
e;
end;
definition
let R,V, L;
func @L -> Element of LinComb(V) equals
:: ZMODUL02:def 31
L;
end;
definition
let R,V;
func LCAdd(V) -> BinOp of LinComb(V) means
:: ZMODUL02:def 32
for e1, e2 holds it.(e1,e2) = @e1 + @e2;
end;
definition
let R,V;
func LCMult(V) -> Function of [:the carrier of R, LinComb(V):],
LinComb(V) means
:: ZMODUL02:def 33
for a, e holds it. [a,e] = a * @e;
end;
definition let R,V;
func LC_Z_Module V -> ModuleStr over R equals
:: ZMODUL02:def 34
ModuleStr (# LinComb(V), LCAdd(V), @ZeroLC(V), LCMult(V) #);
end;
registration let R,V;
cluster LC_Z_Module V -> strict non empty;
end;
registration let R,V;
cluster LC_Z_Module V -> Abelian add-associative right_zeroed
right_complementable vector-distributive scalar-distributive
scalar-associative scalar-unital;
end;
theorem :: ZMODUL02:43
the carrier of LC_Z_Module(V) = LinComb(V);
theorem :: ZMODUL02:44
0.LC_Z_Module(V) = ZeroLC(V);
theorem :: ZMODUL02:45
the addF of LC_Z_Module(V) = LCAdd(V);
theorem :: ZMODUL02:46
the lmult of LC_Z_Module(V) = LCMult(V);
theorem :: ZMODUL02:47
vector(LC_Z_Module(V),L1) + vector(LC_Z_Module(V),L2) = L1 + L2;
theorem :: ZMODUL02:48
a * vector(LC_Z_Module(V),L) = a * L;
theorem :: ZMODUL02:49
- vector(LC_Z_Module(V),L) = - L;
theorem :: ZMODUL02:50
vector(LC_Z_Module(V),L1) - vector(LC_Z_Module(V),L2) = L1 - L2;
definition
let R,V,A;
func LC_Z_Module(A) -> strict Submodule of LC_Z_Module(V) means
:: ZMODUL02:def 35
the carrier of it = the set of all l;
end;
begin :: 3. Linearly independent subset of Z-module
reserve W, W1, W2, W3 for Submodule of V;
reserve v, v1, v2, u for Vector of V;
reserve A, B, C for Subset of V;
reserve T for finite Subset of V;
reserve L, L1, L2 for Linear_Combination of V;
reserve l for Linear_Combination of A;
reserve F, G, H for FinSequence of V;
reserve f, g for Function of V, R;
theorem :: ZMODUL02:51
f (#) (F ^ G) = (f (#) F) ^ (f (#) G);
theorem :: ZMODUL02:52
Sum(L1 + L2) = Sum(L1) + Sum(L2);
theorem :: ZMODUL02:53
Sum(a * L) = a * Sum(L);
theorem :: ZMODUL02:54
Sum(- L) = - Sum(L);
theorem :: ZMODUL02:55
Sum(L1 - L2) = Sum(L1) - Sum(L2);
theorem :: ZMODUL02:56
R is commutative &
A c= B & B is linearly-independent implies A is linearly-independent;
theorem :: ZMODUL02:57
R is non degenerated &
A is linearly-independent implies not 0.V in A;
theorem :: ZMODUL02:58
{}(the carrier of V) is linearly-independent;
registration
let R be Ring;
let V be LeftMod of R;
cluster linearly-independent for Subset of V;
end;
theorem :: ZMODUL02:59
R is non degenerated & V is Mult-cancelable implies
({v} is linearly-independent iff v <> 0.V);
registration let R be non degenerated Ring;
let V be LeftMod of R;
cluster {0.V} -> linearly-dependent for Subset of V;
end;
theorem :: ZMODUL02:60
R is commutative non degenerated &
{v1,v2} is linearly-independent implies v1 <> 0.V;
theorem :: ZMODUL02:61
R is commutative non degenerated implies
{v,0.V} is linearly-dependent;
theorem :: ZMODUL02:62
R = INT.Ring &
::: R is commutative non degenerated &
V is Mult-cancelable implies
(v1 <> v2 & {v1,v2} is linearly-independent iff v2 <> 0.V &
for a, b being Element of R st b <> 0.R holds
b * v1 <> a * v2);
theorem :: ZMODUL02:63
R = INT.Ring &
V is Mult-cancelable implies
(v1 <> v2 & {v1,v2} is linearly-independent iff
for a,b st a * v1 + b * v2 = 0.V holds a = 0.R & b = 0.R);
theorem :: ZMODUL02:64
x in Lin(A) iff ex l st x = Sum(l);
theorem :: ZMODUL02:65
x in A implies x in Lin(A);
theorem :: ZMODUL02:66
for x being object holds x in (0).V iff x = 0.V;
theorem :: ZMODUL02:67
Lin({}(the carrier of V)) = (0).V;
theorem :: ZMODUL02:68
Lin(A) = (0).V implies A = {} or A = {0.V};
theorem :: ZMODUL02:69
for V being strict LeftMod of R,A being Subset of V holds
A = the carrier of V implies Lin(A) = V;
theorem :: ZMODUL02:70
A c= B implies Lin(A) is Submodule of Lin(B);
theorem :: ZMODUL02:71
for V being strict Z_Module,A,B being Subset of V holds
Lin(A) = V & A c= B implies Lin(B) = V;
theorem :: ZMODUL02:72
Lin(A \/ B) = Lin(A) + Lin(B);
theorem :: ZMODUL02:73
Lin(A /\ B) is Submodule of Lin(A) /\ Lin(B);
begin :: 4. Theorems related to submodule
theorem :: ZMODUL02:74
W1 is Submodule of W3 implies W1 /\ W2 is Submodule of W3;
theorem :: ZMODUL02:75
W1 is Submodule of W2 & W1 is Submodule of W3 implies W1 is Submodule of
W2 /\ W3;
theorem :: ZMODUL02:76
W1 is Submodule of W3 & W2 is Submodule of W3 implies W1 + W2 is
Submodule of W3;
theorem :: ZMODUL02:77
W1 is Submodule of W2 implies W1 is Submodule of W2 + W3;