:: Operations on Submodules in Right Module over Associative Ring
:: by Michal Muzalewski and Wojciech Skaba
::
:: Received October 22, 1990
:: Copyright (c) 1990-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 FUNCSDOM, VECTSP_2, RMOD_2, VECTSP_1, ARYTM_3, STRUCT_0,
SUBSET_1, TARSKI, SUPINF_2, RLSUB_1, XBOOLE_0, ARYTM_1, ZFMISC_1,
FUNCT_1, RELAT_1, RLSUB_2, FINSEQ_4, MCART_1, BINOP_1, LATTICES, EQREL_1,
PBOOLE, RMOD_3;
notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, BINOP_1, RELAT_1, FUNCT_1,
STRUCT_0, LATTICES, RLVECT_1, DOMAIN_1, VECTSP_1, VECTSP_2, RMOD_2;
constructors BINOP_1, DOMAIN_1, LATTICES, RMOD_2;
registrations SUBSET_1, STRUCT_0, LATTICES, VECTSP_2, RMOD_2, RELAT_1,
XTUPLE_0;
requirements SUBSET, BOOLE;
begin
reserve R for Ring,
V for RightMod of R,
W,W1,W2,W3 for Submodule of V,
u,u1, u2,v,v1,v2 for Vector of V,
x,y,y1,y2 for object;
definition
let R;
let V;
let W1,W2;
func W1 + W2 -> strict Submodule of V means
:: RMOD_3:def 1
the carrier of it = {v + u: v in W1 & u in W2};
end;
definition
let R;
let V;
let W1,W2;
func W1 /\ W2 -> strict Submodule of V means
:: RMOD_3:def 2
the carrier of it = (the carrier of W1) /\ (the carrier of W2);
end;
theorem :: RMOD_3:1
x in W1 + W2 iff ex v1,v2 st v1 in W1 & v2 in W2 & x = v1 + v2;
theorem :: RMOD_3:2
v in W1 or v in W2 implies v in W1 + W2;
theorem :: RMOD_3:3
x in W1 /\ W2 iff x in W1 & x in W2;
theorem :: RMOD_3:4
for W being strict Submodule of V holds W + W = W;
theorem :: RMOD_3:5
W1 + W2 = W2 + W1;
theorem :: RMOD_3:6
W1 + (W2 + W3) = (W1 + W2) + W3;
theorem :: RMOD_3:7
W1 is Submodule of W1 + W2 & W2 is Submodule of W1 + W2;
theorem :: RMOD_3:8
for W2 being strict Submodule of V holds W1 is Submodule of W2
iff W1 + W2 = W2;
theorem :: RMOD_3:9
for W being strict Submodule of V holds (0).V + W = W & W + (0). V = W;
theorem :: RMOD_3:10
for V being strict RightMod of R holds (0).V + (Omega).V = V &
(Omega).V + (0).V = V;
theorem :: RMOD_3:11
for V being RightMod of R, W being Submodule of V holds (Omega).
V + W = the RightModStr of V & W + (Omega). V = the RightModStr of V;
theorem :: RMOD_3:12
for V being strict RightMod of R holds (Omega).V + (Omega).V = V;
theorem :: RMOD_3:13
for W being strict Submodule of V holds W /\ W = W;
theorem :: RMOD_3:14
W1 /\ W2 = W2 /\ W1;
theorem :: RMOD_3:15
W1 /\ (W2 /\ W3) = (W1 /\ W2) /\ W3;
theorem :: RMOD_3:16
W1 /\ W2 is Submodule of W1 & W1 /\ W2 is Submodule of W2;
theorem :: RMOD_3:17
(for W1 being strict Submodule of V holds W1 is Submodule of W2
implies W1 /\ W2 = W1) & for W1 st W1 /\ W2 = W1 holds W1 is Submodule of W2;
theorem :: RMOD_3:18
W1 is Submodule of W2 implies W1 /\ W3 is Submodule of W2 /\ W3;
theorem :: RMOD_3:19
W1 is Submodule of W3 implies W1 /\ W2 is Submodule of W3;
theorem :: RMOD_3:20
W1 is Submodule of W2 & W1 is Submodule of W3 implies W1 is Submodule
of W2 /\ W3;
theorem :: RMOD_3:21
(0).V /\ W = (0).V & W /\ (0).V = (0).V;
theorem :: RMOD_3:22
for W being strict Submodule of V holds (Omega).V /\ W = W & W
/\ (Omega).V = W;
theorem :: RMOD_3:23
for V being strict RightMod of R holds (Omega).V /\ (Omega).V = V;
theorem :: RMOD_3:24
W1 /\ W2 is Submodule of W1 + W2;
theorem :: RMOD_3:25
for W2 being strict Submodule of V holds (W1 /\ W2) + W2 = W2;
theorem :: RMOD_3:26
for W1 being strict Submodule of V holds W1 /\ (W1 + W2) = W1;
theorem :: RMOD_3:27
(W1 /\ W2) + (W2 /\ W3) is Submodule of W2 /\ (W1 + W3);
theorem :: RMOD_3:28
W1 is Submodule of W2 implies W2 /\ (W1 + W3) = (W1 /\ W2) + (W2 /\ W3
);
theorem :: RMOD_3:29
W2 + (W1 /\ W3) is Submodule of (W1 + W2) /\ (W2 + W3);
theorem :: RMOD_3:30
W1 is Submodule of W2 implies W2 + (W1 /\ W3) = (W1 + W2) /\ (W2 + W3);
theorem :: RMOD_3:31
for W1 being strict Submodule of V holds W1 is Submodule of W3
implies W1 + (W2 /\ W3) = (W1 + W2) /\ W3;
theorem :: RMOD_3:32
for W1,W2 being strict Submodule of V holds W1 + W2 = W2 iff W1 /\ W2 = W1;
theorem :: RMOD_3:33
for W2,W3 being strict Submodule of V holds W1 is Submodule of W2
implies W1 + W3 is Submodule of W2 + W3;
theorem :: RMOD_3:34
W1 is Submodule of W2 implies W1 is Submodule of W2 + W3;
theorem :: RMOD_3:35
W1 is Submodule of W3 & W2 is Submodule of W3 implies W1 + W2 is
Submodule of W3;
theorem :: RMOD_3:36
(ex W st the carrier of W = (the carrier of W1) \/ (the carrier of W2)
) iff W1 is Submodule of W2 or W2 is Submodule of W1;
definition
let R;
let V;
func Submodules(V) -> set means
:: RMOD_3:def 3
for x being object
holds x in it iff ex W being strict Submodule of V st W = x;
end;
registration
let R;
let V;
cluster Submodules(V) -> non empty;
end;
theorem :: RMOD_3:37
for V being strict RightMod of R holds V in Submodules(V);
definition
let R;
let V;
let W1,W2;
pred V is_the_direct_sum_of W1,W2 means
:: RMOD_3:def 4
the RightModStr of V = W1 + W2 & W1 /\ W2 = (0).V;
end;
theorem :: RMOD_3:38
V is_the_direct_sum_of W1,W2 implies V is_the_direct_sum_of W2, W1;
theorem :: RMOD_3:39
for V being strict RightMod of R holds V is_the_direct_sum_of (0).V,
(Omega).V & V is_the_direct_sum_of (Omega).V,(0).V;
reserve C1 for Coset of W1;
reserve C2 for Coset of W2;
theorem :: RMOD_3:40
C1 meets C2 implies C1 /\ C2 is Coset of W1 /\ W2;
theorem :: RMOD_3:41
for V being RightMod of R, W1,W2 being Submodule of V holds V
is_the_direct_sum_of W1,W2 iff for C1 being Coset of W1, C2 being Coset of W2
ex v being Vector of V st C1 /\ C2 = {v};
theorem :: RMOD_3:42
for V being strict RightMod of R, W1,W2 being Submodule of V holds W1
+ W2 = V iff for v being Vector of V ex v1,v2 being Vector of V st v1 in W1 &
v2 in W2 & v = v1 + v2;
theorem :: RMOD_3:43
for V being RightMod of R, W1,W2 being Submodule of V, v,v1,v2,
u1,u2 being Vector of V holds V is_the_direct_sum_of W1,W2 & v = v1 + v2 & v =
u1 + u2 & v1 in W1 & u1 in W1 & v2 in W2 & u2 in W2 implies v1 = u1 & v2 = u2
;
theorem :: RMOD_3:44
V = W1 + W2 & (ex v st for v1,v2,u1,u2 st v = v1 + v2 & v = u1 + u2 &
v1 in W1 & u1 in W1 & v2 in W2 & u2 in W2 holds v1 = u1 & v2 = u2) implies V
is_the_direct_sum_of W1,W2;
definition
let R;
let V be RightMod of R;
let v be Vector of V;
let W1,W2 be Submodule of V;
assume
V is_the_direct_sum_of W1,W2;
func v |-- (W1,W2) -> Element of [:the carrier of V, the carrier of V:]
means
:: RMOD_3:def 5
v = it`1 + it`2 & it`1 in W1 & it`2 in W2;
end;
theorem :: RMOD_3:45
V is_the_direct_sum_of W1,W2 implies (v |-- (W1,W2))`1 = (v |-- (W2,W1 ))`2;
theorem :: RMOD_3:46
V is_the_direct_sum_of W1,W2 implies (v |-- (W1,W2))`2 = (v |-- (W2,W1 ))`1;
reserve A1,A2,B for Element of Submodules(V);
definition
let R;
let V;
func SubJoin(V) -> BinOp of Submodules(V) means
:: RMOD_3:def 6
for A1,A2,W1,W2 st A1 = W1 & A2 = W2 holds it.(A1,A2) = W1 + W2;
end;
definition
let R;
let V;
func SubMeet(V) -> BinOp of Submodules(V) means
:: RMOD_3:def 7
for A1,A2,W1,W2 st A1 = W1 & A2 = W2 holds it.(A1,A2) = W1 /\ W2;
end;
theorem :: RMOD_3:47
LattStr (# Submodules(V), SubJoin(V), SubMeet(V) #) is Lattice;
theorem :: RMOD_3:48
LattStr (# Submodules(V), SubJoin(V), SubMeet(V) #) is 0_Lattice;
theorem :: RMOD_3:49
for V being RightMod of R holds LattStr (# Submodules(V),
SubJoin(V), SubMeet(V) #) is 1_Lattice;
theorem :: RMOD_3:50
for V being RightMod of R holds LattStr (# Submodules(V), SubJoin(V),
SubMeet(V) #) is 01_Lattice;
theorem :: RMOD_3:51
LattStr (# Submodules(V), SubJoin(V), SubMeet(V) #) is M_Lattice;