:: Domains of Submodules, Join and Meet of Finite Sequences of Submodules
:: and Quotient Modules
:: by Micha{\l} Muzalewski
::
:: Received March 29, 1993
:: Copyright (c) 1993-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 SUBSET_1, XBOOLE_0, BINOP_1, FUNCT_1, MULTOP_1, FUNCSDOM,
VECTSP_1, VECTSP_2, RLVECT_2, RLSUB_1, FINSEQ_1, RMOD_3, ARYTM_1,
ARYTM_3, ZFMISC_1, RLVECT_3, SUPINF_2, GROUP_1, TARSKI, CARD_3, MOD_3,
STRUCT_0, RLSUB_2, INCSP_1, PARTFUN1, PRELAMB, SETWISEO, LATTICES,
QC_LANG1, FINSEQ_4, ALGSTR_0, RLVECT_1, RELAT_1, LMOD_7;
notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, DOMAIN_1, STRUCT_0, ALGSTR_0,
FUNCT_2, BINOP_1, FINSEQ_1, SETWISEO, SETWOP_2, LATTICES, MULTOP_1,
RLVECT_1, GROUP_1, VECTSP_1, VECTSP_2, VECTSP_4, VECTSP_5, VECTSP_6,
VECTSP_7, LMOD_6;
constructors BINOP_1, DOMAIN_1, SETWISEO, MULTOP_1, FINSOP_1, LATTICES,
VECTSP_6, VECTSP_7, LMOD_6, RELSET_1;
registrations XBOOLE_0, SUBSET_1, STRUCT_0, LATTICES, VECTSP_1, VECTSP_4,
VECTSP_5, LATTICE2, ALGSTR_0;
requirements BOOLE, SUBSET;
begin :: Schemes
scheme :: LMOD_7:sch 1
ElementEq {A()->set,P[object]} :
for X1,X2 being Element of A() st
(for x being object holds x in X1 iff P[x]) &
(for x being object holds x in X2 iff P[x]) holds X1 = X2;
scheme :: LMOD_7:sch 2
UnOpEq {A() -> non empty set, F(Element of A()) -> object}:
for f1,f2 being UnOp of A() st
(for a being Element of A() holds f1.(a) = F(a))
& (for a being Element of A() holds f2.(a) = F(a)) holds f1 = f2;
scheme :: LMOD_7:sch 3
TriOpEq {A() -> non empty set,
F(Element of A(),Element of A(),Element of A()) -> object}:
for f1,f2 being TriOp of A() st
(for a,b,c being Element of A() holds f1.(a,b,c) = F(a,b,c))
& (for a,b,c being Element of A() holds f2.(a,b,c) = F(a,b,c)) holds f1 = f2;
scheme :: LMOD_7:sch 4
QuaOpEq {A() -> non empty set,
F(Element of A(),Element of A(),Element of A(),Element of A()) -> object}:
for f1,f2 being QuaOp of A() st
(for a,b,c,d being Element of A() holds f1.(a,b,c,d) = F(a,b,c,d))
& (for a,b,c,d being Element of A() holds f2.(a,b,c,d) = F(a,b,c,d))
holds f1 = f2;
scheme :: LMOD_7:sch 5
Fraenkel1Ex {A, D() -> non empty set,
F(object) -> Element of D(), P[object]} : ex S being Subset of D()
st S = {F(x) where x is Element of A() : P[x]};
scheme :: LMOD_7:sch 6
Fr0 {A() -> non empty set, x() -> Element of A(), P[object]} : P[x()]
provided
x() in {a where a is Element of A() : P[a]};
scheme :: LMOD_7:sch 7
Fr1
{X() -> set, A() -> non empty set, a() -> Element of A(), P[object]}:
a() in X() iff P[a()]
provided
X() = {a where a is Element of A() : P[a]};
scheme :: LMOD_7:sch 8
Fr2
{X() -> set, A() -> non empty set, a() -> Element of A(), P[object]}:
P[a()]
provided
a() in X() and
X() = {a where a is Element of A() : P[a]};
scheme :: LMOD_7:sch 9
Fr3 {x() -> set, X() -> set, A() -> non empty set, P[object]} :
x() in X() iff ex a being Element of A() st x()=a & P[a]
provided
X() = {a where a is Element of A() : P[a]};
scheme :: LMOD_7:sch 10
Fr4 {D1,D2() -> non empty set, B() -> set,
a() -> Element of D1(), F(object) -> set, P,Q[object,object]} :
a() in F(B()) iff for b being Element of D2() st b in B() holds P[a(),b]
provided
F(B()) = {a where a is Element of D1() : Q[a,B()]} and
Q[a(),B()] iff for b being Element of D2() st b in B() holds P[a(),b];
begin :: Main Part
reserve x for set,
K for Ring,
r for Scalar of K,
V for LeftMod of K,
a,b,a1,a2 for Vector of V,
A,A1,A2 for Subset of V,
l for Linear_Combination of A,
W for Subspace of V,
Li for FinSequence of Submodules(V);
:: 1. Auxiliary theorems about free-modules
theorem :: LMOD_7:1
K is non trivial & A is linearly-independent implies not 0.V in A;
theorem :: LMOD_7:2
not a in A implies l.a = 0.K;
theorem :: LMOD_7:3
K is trivial implies (for l holds Carrier(l) = {}) & Lin A is trivial;
theorem :: LMOD_7:4
V is non trivial implies for A st A is base holds A <> {};
theorem :: LMOD_7:5
A1 \/ A2 is linearly-independent & A1 misses A2
implies Lin A1 /\ Lin A2 = (0).V;
theorem :: LMOD_7:6
A is base & A = A1 \/ A2 & A1 misses A2 implies
V is_the_direct_sum_of Lin A1,Lin A2;
begin :: 2. Domains of submodules
definition
let K,V;
mode SUBMODULE_DOMAIN of V -> non empty set means
:: LMOD_7:def 1
x in it implies x is strict Subspace of V;
end;
definition
let K,V;
redefine func Submodules(V) -> SUBMODULE_DOMAIN of V;
end;
definition
let K,V;
let D be SUBMODULE_DOMAIN of V;
redefine mode Element of D -> strict Subspace of V;
end;
registration
let K,V;
let D be SUBMODULE_DOMAIN of V;
cluster strict for Element of D;
end;
definition
let K,V;
assume
V is non trivial;
mode LINE of V -> strict Subspace of V means
:: LMOD_7:def 2
ex a st a<>0.V & it = <:a:>;
end;
definition
let K,V;
mode LINE_DOMAIN of V -> non empty set means
:: LMOD_7:def 3
x in it implies x is LINE of V;
end;
definition
let K,V;
func lines(V) -> LINE_DOMAIN of V means
:: LMOD_7:def 4
for x being object holds x in it iff x is LINE of V;
end;
definition
let K,V;
let D be LINE_DOMAIN of V;
redefine mode Element of D -> LINE of V;
end;
definition
let K,V;
assume that
V is non trivial and
V is free;
mode HIPERPLANE of V -> strict Subspace of V means
:: LMOD_7:def 5
ex a st a<>0.V & V is_the_direct_sum_of <:a:>,it;
end;
definition
let K,V;
mode HIPERPLANE_DOMAIN of V -> non empty set means
:: LMOD_7:def 6
x in it implies x is HIPERPLANE of V;
end;
definition
let K,V;
func hiperplanes(V) -> HIPERPLANE_DOMAIN of V means
:: LMOD_7:def 7
for x being object holds x in it iff x is HIPERPLANE of V;
end;
definition
let K,V;
let D be HIPERPLANE_DOMAIN of V;
redefine mode Element of D -> HIPERPLANE of V;
end;
begin :: 3. Join and meet of finite sequences of submodules
definition
let K,V,Li;
func Sum Li -> Element of Submodules(V) equals
:: LMOD_7:def 8
SubJoin(V) $$ Li;
func /\ Li -> Element of Submodules(V) equals
:: LMOD_7:def 9
SubMeet(V) $$ Li;
end;
theorem :: LMOD_7:7
SubJoin(V) is commutative associative & SubJoin(V) is having_a_unity
& (0).V = the_unity_wrt SubJoin(V);
theorem :: LMOD_7:8
SubMeet(V) is commutative associative & SubMeet(V)
is having_a_unity & (Omega).V = the_unity_wrt SubMeet(V);
begin :: 4. Sum of subsets of module
definition
let K,V,A1,A2;
func A1 + A2 -> Subset of V means
:: LMOD_7:def 10
x in it iff ex a1,a2 st a1 in A1 & a2 in A2 & x = a1+a2;
end;
begin :: 5. Vector of subset
definition
let K,V,A;
assume
A <> {};
mode Vector of A -> Vector of V means
:: LMOD_7:def 11
it is Element of A;
end;
theorem :: LMOD_7:9
A1 <> {} & A1 c= A2 implies for x st x is Vector of A1 holds x is Vector of
A2;
:: 6. Quotient modules
theorem :: LMOD_7:10
a2 in a1 + W iff a1 - a2 in W;
theorem :: LMOD_7:11
a1 + W = a2 + W iff a1 - a2 in W;
definition
let K,V,W;
func V..W -> set means
:: LMOD_7:def 12
x in it iff ex a st x = a + W;
end;
registration
let K,V,W;
cluster V..W -> non empty;
end;
definition
let K,V,W,a;
func a..W -> Element of V..W equals
:: LMOD_7:def 13
a + W;
end;
theorem :: LMOD_7:12
for x being Element of V..W ex a st x = a..W;
theorem :: LMOD_7:13
a1..W = a2..W iff a1 - a2 in W;
reserve S1,S2 for Element of V..W;
definition
let K,V,W,S1;
func -S1 -> Element of V..W means
:: LMOD_7:def 14
S1 = a..W implies it = (-a)..W;
let S2;
func S1 + S2 -> Element of V..W means
:: LMOD_7:def 15
S1 = a1..W & S2 = a2..W implies it = (a1+a2)..W;
end;
definition
let K,V,W;
func COMPL W -> UnOp of V..W means
:: LMOD_7:def 16
it.S1 = -S1;
func ADD W -> BinOp of V..W means
:: LMOD_7:def 17
it.(S1,S2) = S1 + S2;
end;
definition
let K,V,W;
func V.W -> strict addLoopStr equals
:: LMOD_7:def 18
addLoopStr(#V..W,ADD W,(0.V)..W#);
end;
registration
let K,V,W;
cluster V.W -> non empty;
end;
theorem :: LMOD_7:14
a..W is Element of V.W;
definition
let K,V,W,a;
func a.W -> Element of V.W equals
:: LMOD_7:def 19
a..W;
end;
theorem :: LMOD_7:15
for x being Element of V.W ex a st x = a.W;
theorem :: LMOD_7:16
a1.W = a2.W iff a1 - a2 in W;
theorem :: LMOD_7:17
a.W + b.W = (a+b).W & 0.(V.W) = (0.V).W;
registration
let K,V,W;
cluster V.W -> Abelian add-associative right_zeroed right_complementable;
end;
reserve S for Element of V.W;
definition
let K,V,W,r,S;
func r*S -> Element of V.W means
:: LMOD_7:def 20
S = a.W implies it = (r*a).W;
end;
definition
let K,V,W;
func LMULT W -> Function of [:the carrier of K,the carrier of V.W:],
the carrier of V.W means
:: LMOD_7:def 21
it.(r,S) = r*S;
end;
begin
definition
let K,V,W;
func V/W -> strict ModuleStr over K equals
:: LMOD_7:def 22
ModuleStr(#the carrier of V.W,the addF of V.W,0.V.W,LMULT W#);
end;
registration
let K,V,W;
cluster V/W -> non empty;
end;
theorem :: LMOD_7:18
a.W is Vector of V/W;
theorem :: LMOD_7:19
for x being Vector of V/W holds x is Element of V.W;
definition
let K,V,W,a;
func a/W -> Vector of V/W equals
:: LMOD_7:def 23
a.W;
end;
theorem :: LMOD_7:20
for x being Vector of V/W ex a st x = a/W;
theorem :: LMOD_7:21
a1/W = a2/W iff a1 - a2 in W;
theorem :: LMOD_7:22
a/W + b/W = (a+b)/W & r*(a/W) = (r*a)/W;
theorem :: LMOD_7:23
V/W is strict LeftMod of K;
registration
let K,V,W;
cluster V/W -> vector-distributive scalar-distributive
scalar-associative scalar-unital;
end;