:: Submodules
:: by Micha{\l} Muzalewski
::
:: Received June 19, 1992
:: Copyright (c) 1992-2019 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_1, VECTSP_2, SUBSET_1, RLVECT_2, RLSUB_1,
RMOD_3, RLSUB_2, STRUCT_0, RELAT_1, FUNCT_1, SUPINF_2, ZFMISC_1,
ALGSTR_0, REALSET1, GROUP_1, QC_LANG1, TARSKI, XBOOLE_0, RLVECT_3,
CARD_3, PARTFUN1, ARYTM_3, ARYTM_1;
notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, RELAT_1, BINOP_1, REALSET1,
DOMAIN_1, STRUCT_0, ALGSTR_0, GROUP_1, VECTSP_1, VECTSP_2, VECTSP_4,
VECTSP_5, VECTSP_6, VECTSP_7;
constructors BINOP_1, REALSET2, VECTSP_5, VECTSP_6, VECTSP_7, RELSET_1;
registrations RELSET_1, STRUCT_0, VECTSP_1, VECTSP_4, VECTSP_7;
requirements SUBSET, BOOLE;
definitions TARSKI, XBOOLE_0;
equalities XBOOLE_0, REALSET1, STRUCT_0;
expansions STRUCT_0;
theorems FUNCT_2, MOD_3, TARSKI, VECTSP_1, VECTSP_4, VECTSP_5, VECTSP_6,
XBOOLE_1, RELAT_1;
begin
reserve x for set,
K for Ring,
r for Scalar of K,
V, M, M1, M2, N for LeftMod of K,
a for Vector of V,
m, m1, m2 for Vector of M,
n, n1, n2 for Vector of N,
A for Subset of V,
l for Linear_Combination of A,
W, W1, W2, W3 for Subspace of V;
notation
let K, V;
synonym Submodules(V) for Subspaces(V);
end;
theorem
M1 = the ModuleStr of M2 implies (x in M1 iff x in M2);
theorem
for v being Vector of the ModuleStr of V st a=v holds r*a = r*v
proof
let v be Vector of (the ModuleStr of V) such that
A1: a=v;
thus r*a = (the lmult of V).(r,a) by VECTSP_1:def 12
.= r*v by A1,VECTSP_1:def 12;
end;
theorem Th3:
the ModuleStr of V is strict Subspace of V
proof
(Omega).V = the ModuleStr of V by VECTSP_4:def 4;
hence thesis;
end;
theorem Th4:
V is Subspace of (Omega).V
proof
set W=(Omega).V;
A1: W = the ModuleStr of V by VECTSP_4:def 4;
then
A2: 0.V = 0.W;
dom(the lmult of W) = [:the carrier of K, the carrier of W:] by FUNCT_2:def 1
;
then
A3: the lmult of V = (the lmult of W) | [:the carrier of K, the carrier of V
:] by A1,RELAT_1:68;
dom(the addF of W) = [:the carrier of W,the carrier of W:] by FUNCT_2:def 1;
then the addF of V = (the addF of W)||the carrier of V by A1,RELAT_1:68;
hence thesis by A1,A2,A3,VECTSP_4:def 2;
end;
begin
definition
let K;
redefine attr K is trivial means
0.K = 1_K;
compatibility
proof
thus K is trivial implies 0.K = 1_K;
assume
A1: 0.K = 1_K;
now
let x be Scalar of K;
thus x = x*(1_K)
.= 0.K by A1;
end;
hence thesis;
end;
end;
theorem Th5:
K is trivial implies (for r holds r = 0.K) & for a holds a = 0.V
proof
assume K is trivial;
then
A1: 0.K = 1_K;
A2: now
let a;
thus a = 1_K*a by VECTSP_1:def 17
.= 0.V by A1,VECTSP_1:14;
end;
now
let r;
thus r = r*1_K
.= 0.K by A1;
end;
hence thesis by A2;
end;
theorem
K is trivial implies V is trivial
by Th5;
theorem
V is trivial iff the ModuleStr of V = (0).V
proof
set X = the carrier of (0).V;
reconsider W = the ModuleStr of V as strict Subspace of V by Th3;
reconsider Z=(0).V as Subspace of W by VECTSP_4:39;
A1: now
assume W <> Z;
then consider a such that
A2: not a in Z by VECTSP_4:32;
not a in X by A2;
then not a in {0.V} by VECTSP_4:def 3;
then a <> 0.V by TARSKI:def 1;
hence V is non trivial;
end;
now
assume V is non trivial;
then consider a such that
A3: a <> 0.V;
not a in {0.V} by A3,TARSKI:def 1;
then not a in X by VECTSP_4:def 3;
hence W <> (0).V;
end;
hence thesis by A1;
end;
begin :: 1. Submodules and subsets
definition
let K,V;
let W be strict Subspace of V;
func @W -> Element of Submodules(V) equals
W;
coherence by VECTSP_5:def 3;
end;
theorem Th8:
for A being Subset of W holds A is Subset of V
proof
let A be Subset of W;
the carrier of W c= the carrier of V by VECTSP_4:def 2;
hence thesis by XBOOLE_1:1;
end;
definition
let K,V,W;
let A be Subset of W;
func @A -> Subset of V equals
A;
coherence by Th8;
end;
registration
let K,V,W;
let A be non empty Subset of W;
cluster @A -> non empty;
coherence;
end;
theorem
x in [#]V iff x in V;
theorem
x in @[#]W iff x in W;
theorem Th11:
A c= [#]Lin(A)
proof
let x be object;
assume x in A;
then x in Lin(A) by MOD_3:5;
hence thesis;
end;
theorem Th12:
A<>{} & A is linearly-closed implies Sum(l) in A
proof
assume
A1: A<>{} & A is linearly-closed;
now
per cases;
suppose
0.K<>1_K;
hence thesis by A1,VECTSP_6:14;
end;
suppose
0.K=1_K;
then K is trivial;
then Sum(l) = 0.V by Th5;
hence thesis by A1,VECTSP_4:1;
end;
end;
hence thesis;
end;
theorem
0.V in A & A is linearly-closed implies A = [#]Lin(A)
proof
assume
A1: 0.V in A & A is linearly-closed;
thus A c= [#]Lin(A) by Th11;
let x be object;
assume x in [#]Lin(A);
then x in Lin(A);
then ex l st x = Sum(l) by MOD_3:4;
hence thesis by A1,Th12;
end;
begin :: 2. Cyclic submodule
definition
let K,V,a;
func <:a:> -> strict Subspace of V equals
Lin({a});
correctness;
end;
begin :: 3. Inclusion of left R-modules
definition
let K,M,N;
pred M c= N means
M is Subspace of N;
reflexivity by VECTSP_4:24;
end;
theorem Th14:
for x being object holds
M c= N implies (x in M implies x in N) & (x is Vector of M
implies x is Vector of N)
by VECTSP_4:9,VECTSP_4:10;
theorem
M c= N implies 0.M = 0.N & (m1 = n1 & m2 = n2 implies m1 + m2 = n1 +
n2) & (m = n implies r * m = r * n) & (m = n implies - n = - m) & (m1 = n1 & m2
= n2 implies m1 - m2 = n1 - n2) & 0.N in M & 0.M in N & (n1 in M & n2 in M
implies n1 + n2 in M) & (n in M implies r * n in M) & (n in M implies - n in M)
& (n1 in M & n2 in M implies n1 - n2 in M)
by VECTSP_4:11,VECTSP_4:13,VECTSP_4:14,VECTSP_4:15,VECTSP_4:16,VECTSP_4:17,
VECTSP_4:19,VECTSP_4:20,VECTSP_4:21,VECTSP_4:22,VECTSP_4:23;
theorem
M1 c= N & M2 c= N implies 0.M1 = 0.M2 & 0.M1 in M2 & (the carrier of
M1 c= the carrier of M2 implies M1 c= M2) & ((for n st n in M1 holds n in M2)
implies M1 c= M2) & (the carrier of M1 = the carrier of M2 & M1 is strict & M2
is strict implies M1 = M2) & (0).M1 c= M2
by VECTSP_4:12,VECTSP_4:18,VECTSP_4:27,VECTSP_4:28,VECTSP_4:29,VECTSP_4:40;
theorem
for V,M being strict LeftMod of K holds V c= M & M c= V implies V = M
by VECTSP_4:25;
theorem
V c= M & M c= N implies V c= N
by VECTSP_4:26;
theorem
M c= N implies (0).M c= N
by VECTSP_4:38;
theorem
M c= N implies (0).N c= M
by VECTSP_4:39;
theorem
M c= N implies M c= (Omega).N
proof
assume M c= N;
then
A1: M is Subspace of N;
N is Subspace of (Omega).N by Th4;
then M is Subspace of (Omega).N by A1,VECTSP_4:26;
hence thesis;
end;
theorem
W1 c= W1 + W2 & W2 c= W1 + W2
by VECTSP_5:7;
theorem
W1 /\ W2 c= W1 & W1 /\ W2 c= W2
by VECTSP_5:15;
theorem
W1 c= W2 implies W1 /\ W3 c= W2 /\ W3
by VECTSP_5:17;
theorem
W1 c= W3 implies W1 /\ W2 c= W3
by VECTSP_5:18;
theorem
W1 c= W2 & W1 c= W3 implies W1 c= W2 /\ W3
by VECTSP_5:19;
theorem
W1 /\ W2 c= W1 + W2
by VECTSP_5:23;
theorem
(W1 /\ W2) + (W2 /\ W3) c= W2 /\ (W1 + W3)
by VECTSP_5:26;
theorem
W1 c= W2 implies W2 /\ (W1 + W3) = (W1 /\ W2) + (W2 /\ W3)
by VECTSP_5:27;
theorem
W2 + (W1 /\ W3) c= (W1 + W2) /\ (W2 + W3)
by VECTSP_5:28;
theorem
W1 c= W2 implies W2 + (W1 /\ W3) = (W1 + W2) /\ (W2 + W3)
by VECTSP_5:29;
theorem
W1 c= W2 implies W1 c= W2 + W3
by VECTSP_5:33;
theorem
W1 c= W3 & W2 c= W3 implies W1 + W2 c= W3
by VECTSP_5:34;
theorem
for A,B being Subset of V st A c= B holds Lin(A) c= Lin(B)
by MOD_3:10;
theorem
for A,B being Subset of V holds Lin(A /\ B) c= Lin(A) /\ Lin(B)
by MOD_3:13;
theorem Th36:
M1 c= M2 implies [#]M1 c= [#]M2
proof
assume
A1: M1 c= M2;
let x be object;
assume x in [#]M1;
then x in M1;
then x in M2 by A1,Th14;
hence thesis;
end;
theorem Th37:
W1 c= W2 iff for a st a in W1 holds a in W2
by VECTSP_4:8,VECTSP_4:28;
theorem Th38:
W1 c= W2 iff [#]W1 c= [#]W2
proof
thus W1 c= W2 implies [#]W1 c= [#]W2 by Th36;
assume [#]W1 c= [#]W2;
then for a st a in W1 holds a in W2;
hence thesis by Th37;
end;
theorem
W1 c= W2 iff @[#]W1 c= @[#]W2 by Th38;
theorem
(0).W c= V & (0).V c= W & (0).W1 c= W2 by VECTSP_4:38,39,40;