Copyright (c) 1991 Association of Mizar Users
environ
vocabulary CLASSES2, FUNCSDOM, VECTSP_2, MOD_2, CAT_1, MIDSP_1, GRCAT_1,
ENS_1, INCSP_1, ORDINAL4, FUNCT_2, RELAT_1, PRE_TOPC, VECTSP_1, BOOLE,
FUNCT_3, FUNCT_1, TARSKI, ARYTM_3, PARTFUN1, MODCAT_1, RLVECT_1,
ALGSTR_1;
notation TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, STRUCT_0, RELAT_1, FUNCT_1,
FUNCT_2, PARTFUN1, RLVECT_1, VECTSP_1, FUNCSDOM, VECTSP_2, CAT_1,
FRAENKEL, CLASSES2, PRE_TOPC, ALGSTR_1, GRCAT_1, MOD_2, FUNCT_3, MIDSP_1;
constructors GRCAT_1, MOD_2, MIDSP_1, VECTSP_2, ALGSTR_1, MEMBERED, XBOOLE_0;
clusters VECTSP_2, CAT_1, GRCAT_1, MOD_2, RELSET_1, STRUCT_0, SUBSET_1,
MEMBERED, ZFMISC_1, XBOOLE_0;
requirements SUBSET, BOOLE;
theorems CAT_1, GRCAT_1, FUNCT_2, MOD_2, PARTFUN1, TARSKI, ZFMISC_1, RELSET_1,
XBOOLE_0, ALGSTR_1;
schemes FUNCT_2, GRCAT_1, TARSKI;
begin
reserve x,y for set;
reserve D for non empty set;
reserve UN for Universe;
reserve R for Ring;
reserve G,H for LeftMod of R;
::
:: 2. Domains of left modules
::
definition let R;
mode LeftMod_DOMAIN of R -> non empty set means
:Def1: for x being Element of it holds x is strict LeftMod of R;
existence
proof
set D = {TrivialLMod(R)};
take D;
thus thesis by TARSKI:def 1;
end;
end;
reserve V for LeftMod_DOMAIN of R;
definition let R,V;
redefine mode Element of V -> LeftMod of R;
coherence by Def1;
end;
definition let R,V;
cluster strict Element of V;
existence
proof
consider e being Element of V;
take e;
thus thesis by Def1;
end;
end;
definition let R;
mode LModMorphism_DOMAIN of R -> non empty set means
:Def2: for x being Element of it holds x is strict LModMorphism of R;
existence
proof
consider G;
take {ID G};
let x be Element of {ID G};
thus thesis by TARSKI:def 1;
end;
end;
definition let R; let M be LModMorphism_DOMAIN of R;
redefine mode Element of M -> LModMorphism of R;
coherence by Def2;
end;
definition let R; let M be LModMorphism_DOMAIN of R;
cluster strict Element of M;
existence
proof consider e being Element of M;
take e;
thus thesis by Def2;
end;
end;
canceled 2;
theorem
Th3: for f being strict LModMorphism of R
holds {f} is LModMorphism_DOMAIN of R
proof
let f be strict LModMorphism of R;
for x be Element of {f} holds
x is strict LModMorphism of R by TARSKI:def 1;
hence thesis by Def2;
end;
definition let R,G,H;
mode LModMorphism_DOMAIN of G,H -> LModMorphism_DOMAIN of R means
:Def3: for x being Element of it holds x is strict Morphism of G,H;
existence
proof
reconsider D = {ZERO(G,H)} as LModMorphism_DOMAIN of R by Th3;
take D;
thus thesis by TARSKI:def 1;
end;
end;
theorem
Th4: D is LModMorphism_DOMAIN of G,H
iff for x being Element of D holds x is strict Morphism of G,H
proof
thus D is LModMorphism_DOMAIN of G,H
implies for x being Element of D holds x is strict Morphism of G,H
by Def3;
thus (for x being Element of D holds x is strict Morphism of G,H)
implies D is LModMorphism_DOMAIN of G,H
proof
assume A1: for x being Element of D holds x is strict Morphism of G,H;
then for x being Element of D holds x is strict LModMorphism of R;
then reconsider D' = D as LModMorphism_DOMAIN of R by Def2;
for x being Element of D' holds x is strict Morphism of G,H by A1;
hence thesis by Def3;
end;
end;
theorem
for f being strict Morphism of G,H holds {f} is LModMorphism_DOMAIN of G,H
proof
let f be strict Morphism of G,H;
for x being Element of {f} holds x is strict Morphism of G,H
by TARSKI:def 1;
hence thesis by Th4;
end;
definition let R,G,H;
func Morphs(G,H) -> LModMorphism_DOMAIN of G,H means
:Def4: x in it iff x is strict Morphism of G,H;
existence
proof
set D = { LModMorphismStr(# G,H,f#) where f is Element of Maps(G,H)
: f is linear };
ZeroMap(G,H) is Element of
Funcs(the carrier of G, the carrier of H) by FUNCT_2:11;
then reconsider f0 = ZeroMap(G,H) as Element of Maps(G,H) by GRCAT_1:def
26;
f0 is linear by MOD_2:8;
then LModMorphismStr(# G,H,f0#) in D;
then reconsider D as non empty set;
A1: x in D implies x is strict Morphism of G,H
proof
assume x in D;
then ex f being Element of Maps(G,H) st
x = LModMorphismStr (#G,H,f#) & f is linear;
hence thesis by MOD_2:12;
end;
then A2: for x being Element of D holds x is strict Morphism of G,H;
A3: x is strict Morphism of G,H implies x in D
proof
assume x is strict Morphism of G,H;
then reconsider x as strict Morphism of G,H;
dom(x) = G & cod(x) = H by MOD_2:def 11;
then A4: the Dom of x = G & the Cod of x = H by MOD_2:def 6,def 7;
A5: (the Fun of x) is linear by MOD_2:10;
reconsider f = the Fun of x as map of G,H by A4;
f is Element of Funcs(the carrier of G,
the carrier of H) by FUNCT_2:11;
then reconsider g = f as Element of Maps(G,H) by GRCAT_1:def 26;
x = LModMorphismStr(# G,H,g #) by A4;
hence thesis by A5;
end;
reconsider D as LModMorphism_DOMAIN of G,H by A2,Th4;
take D;
thus thesis by A1,A3;
end;
uniqueness
proof
let D1,D2 be LModMorphism_DOMAIN of G,H such that
A6: x in D1 iff x is strict Morphism of G,H and
A7: x in D2 iff x is strict Morphism of G,H;
x in D1 iff x in D2
proof
hereby assume x in D1;
then x is strict Morphism of G,H by A6;
hence x in D2 by A7;
end;
assume x in D2;
then x is strict Morphism of G,H by A7;
hence thesis by A6;
end;
hence thesis by TARSKI:2;
end;
end;
definition let R,G,H; let M be LModMorphism_DOMAIN of G,H;
redefine mode Element of M -> Morphism of G,H;
coherence by Def3;
end;
::
:: 4a. Category of left modules - objects
::
definition let x,y,R;
pred GO x,y,R means
:Def5: ex x1,x2 being set st x = [x1,x2] &
ex G being strict LeftMod of R st y = G
& x1 = the LoopStr of G
& x2 = the lmult of G;
end;
theorem
Th6: for x,y1,y2 being set st GO x,y1,R & GO x,y2,R holds y1 = y2
proof
let x,y1,y2 be set such that
A1: GO x,y1,R and
A2: GO x,y2,R;
consider a1,a2 being set such that
A3: x = [a1,a2] and
A4: ex G being strict LeftMod of R st y1 = G
& a1 = the LoopStr of G
& a2 = the lmult of G by A1,Def5;
consider b1,b2 being set such that
A5: x = [b1,b2] and
A6: ex G being strict LeftMod of R st y2 = G
& b1 = the LoopStr of G
& b2 = the lmult of G by A2,Def5;
consider G1 being strict LeftMod of R such that
A7: y1 = G1
& a1 = the LoopStr of G1
& a2 = the lmult of G1 by A4;
consider G2 being strict LeftMod of R such that
A8: y2 = G2
& b1 = the LoopStr of G2
& b2 = the lmult of G2 by A6;
the LoopStr of G1 = the LoopStr of G2
& the lmult of G1 = the lmult of G2 by A3,A5,A7,A8,ZFMISC_1:33;
hence thesis by A7,A8;
end;
theorem
Th7: for UN ex x st x in {[G,f] where G is Element of GroupObjects(UN),
f is Element of Funcs([:the carrier of R,{{}}:],{{}}) : not contradiction}
& GO x,TrivialLMod(R),R
proof
let UN;
set T = TrivialLMod(R);
A1: op0 = {} by TARSKI:def 1 .= Extract {} by TARSKI:def 1;
A2:T = VectSpStr (#{{}},op2,op0,pr2(the carrier of R, {{}})#)
by MOD_2:def 2;
then reconsider x1 = the LoopStr of T as Element of GroupObjects(UN)
by A1,ALGSTR_1:def 4,GRCAT_1:42;
reconsider f1 = (the lmult of T)
as Function of [:the carrier of R,{{}}:],{{}} by A2;
reconsider x2 = f1 as Element of Funcs([:the carrier of R,{{}}:],{{}}) by
FUNCT_2:11;
take x = [x1,x2];
thus x in {[G,f] where G is Element of GroupObjects(UN),
f is Element of Funcs([:the carrier of R,{{}}:],{{}
}) : not contradiction};
thus GO x,TrivialLMod(R),R by Def5;
end;
definition let UN,R;
func LModObjects(UN,R) -> set means
:Def6: for y holds y in it iff ex x st
x in {[G,f] where G is Element of GroupObjects(UN),
f is Element of Funcs([:the carrier of R,{{}}:],{{}}) : not contradiction}
& GO x,y,R;
existence
proof
set N = {[G,f] where G is Element of GroupObjects(UN),
f is Element of Funcs([:the carrier of R,{{}}:],{{}}) : not contradiction};
defpred P[set,set] means GO $1,$2,R;
A1: for x,y1,y2 being set st P[x,y1] & P[x,y2] holds y1 = y2 by Th6;
consider Y being set such that
A2: for y holds y in Y iff ex x st x in N & P[x,y] from Fraenkel(A1);
take Y;
thus thesis by A2;
end;
uniqueness
proof
set N = {[G,f] where G is Element of GroupObjects(UN),
f is Element of Funcs([:the carrier of R,{{}}:],{{}}) :
not contradiction};
let Y1,Y2 be set such that
A3: for y holds y in Y1 iff ex x st x in N & GO x,y,R and
A4: for y holds y in Y2 iff ex x st x in N & GO x,y,R;
now
let y;
y in Y1 iff ex x st x in N & GO x,y,R by A3;
hence y in Y1 iff y in Y2 by A4;end;
hence thesis by TARSKI:2;
end;
end;
theorem Th8:
TrivialLMod(R) in LModObjects(UN,R)
proof
ex x st x in {[G,f] where G is Element of GroupObjects(UN),
f is Element of Funcs([:the carrier of R,{{}}:],{{}}) : not contradiction}
& GO x,TrivialLMod(R),R by Th7;
hence thesis by Def6;
end;
definition let UN,R;
cluster LModObjects(UN,R) -> non empty;
coherence by Th8;
end;
theorem
Th9: for x being Element of LModObjects(UN,R)
holds x is strict LeftMod of R
proof
let x be Element of LModObjects(UN,R);
set N = {[G,f] where G is Element of GroupObjects(UN),
f is Element of Funcs([:the carrier of R,{{}}:],{{}}) : not contradiction};
consider u being set such that
A1: u in N & GO u,x,R by Def6;
ex a1,a2 being set st
u = [a1,a2] &
ex G being strict LeftMod of R st x = G
& a1 = the LoopStr of G
& a2 = the lmult of G by A1,Def5;
hence thesis;
end;
definition let UN,R;
redefine func LModObjects(UN,R) -> LeftMod_DOMAIN of R;
coherence
proof
for x being Element of LModObjects(UN,R) holds x is strict LeftMod of R
by Th9;
hence thesis by Def1;
end;
end;
::
:: 4b. Category of left modules - morphisms
::
definition let R,V;
func Morphs(V) -> LModMorphism_DOMAIN of R means
:Def7: for x holds x in it iff ex G,H being strict Element of V
st x is strict Morphism of G,H;
existence
proof
consider G0,H0 being strict Element of V;
set M = Morphs(G0,H0),
S = { Morphs(G,H)
where G is strict Element of V, H is strict Element of V
: not contradiction };
A1: (ZERO(G0,H0)) is Element of M by Def4;
M in S;
then reconsider T = union S as non empty set by A1,TARSKI:def 4;
A2: for x holds x in T iff ex G,H being strict Element of V
st x is strict Morphism of G,H
proof
let x;
thus x in T implies ex G,H being strict Element of V
st x is strict Morphism of G,H
proof
assume x in T;
then consider Y being set such that
A3: x in Y and
A4: Y in S by TARSKI:def 4;
consider G,H being strict Element of V such that
A5: Y = Morphs(G,H) by A4;
take G,H;
thus thesis by A3,A5,Def4;
end;
thus (ex G,H being strict Element of V
st x is strict Morphism of G,H)
implies x in T
proof
given G,H being strict Element of V such that
A6: x is strict Morphism of G,H;
set M = Morphs(G,H);
A7: x in M by A6,Def4;
M in S;
hence thesis by A7,TARSKI:def 4;
end;
end;
now let x be Element of T;
ex G,H being strict Element of V st
x is strict Morphism of G,H by A2;
hence x is strict LModMorphism of R;end;
then reconsider T' = T as LModMorphism_DOMAIN of R
by Def2;
take T';
thus thesis by A2;
end;
uniqueness
proof
let D1,D2 be LModMorphism_DOMAIN of R such that
A8: for x holds x in D1 iff ex G,H being strict Element of V
st x is strict Morphism of G,H and
A9: for x holds x in D2 iff ex G,H being strict Element of V
st x is strict Morphism of G,H;
now let x;
x in D1 iff
ex G,H being strict Element of V st x is strict Morphism of G,H by A8;
hence x in D1 iff x in D2 by A9;end;
hence thesis by TARSKI:2;
end;
end;
::
:: 4c. Category of left modules - dom,cod,id
::
definition let R,V; let F be Element of Morphs(V);
func dom'(F) -> Element of V equals
:Def8: dom(F);
coherence
proof
consider G,H being strict Element of V such that
A1: F is strict Morphism of G,H by Def7;
reconsider F' = F as Morphism of G,H by A1;
dom(F') = G by MOD_2:def 11;
hence thesis;
end;
func cod'(F) -> Element of V equals
:Def9: cod(F);
coherence
proof
consider G,H being strict Element of V such that
A2: F is strict Morphism of G,H by Def7;
reconsider F' = F as Morphism of G,H by A2;
cod(F') = H by MOD_2:def 11;
hence thesis;
end;
end;
definition let R,V; let G be Element of V;
func ID(G) -> strict Element of Morphs(V) equals
:Def10: ID(G);
coherence
proof
reconsider G as strict Element of V by Def1;
ID(G) is strict Element of Morphs(V) by Def7;
hence thesis;
end;
end;
definition let R,V;
func dom(V) -> Function of Morphs(V),V means
:Def11: for f being Element of Morphs(V) holds it.f = dom'(f);
existence
proof
deffunc G(Element of Morphs(V))=dom'($1);
consider F being Function of Morphs(V),V such that
A1: for f being Element of Morphs(V) holds F.f = G(f) from LambdaD;
take F;
thus thesis by A1;
end;
uniqueness
proof
let F1,F2 be Function of Morphs(V),V such that
A2: for f being Element of Morphs(V) holds F1.f = dom' f and
A3: for f being Element of Morphs(V) holds F2.f = dom' f;
now let f be Element of Morphs(V);
F1.f = dom'(f) by A2;
hence F1.f = F2.f by A3;end;
hence thesis by FUNCT_2:113;
end;
func cod(V) -> Function of Morphs(V),V means
:Def12: for f being Element of Morphs(V) holds it.f = cod'(f);
existence
proof
deffunc G(Element of Morphs(V))=cod'($1);
consider F being Function of Morphs(V),V such that
A4: for f being Element of Morphs(V) holds F.f = G(f) from LambdaD;
take F;
thus thesis by A4;
end;
uniqueness
proof
let F1,F2 be Function of Morphs(V),V such that
A5: for f being Element of Morphs(V) holds F1.f = cod' f and
A6: for f being Element of Morphs(V) holds F2.f = cod' f;
now let f be Element of Morphs(V);
F1.f = cod'(f) by A5;
hence F1.f = F2.f by A6;end;
hence thesis by FUNCT_2:113;
end;
func ID(V) -> Function of V,Morphs(V) means
:Def13: for G being Element of V holds it.G = ID(G);
existence
proof
deffunc Gf(Element of V) = ID($1);
consider F being Function of V,Morphs(V) such that
A7: for G being Element of V holds F.G = Gf(G) from LambdaD;
take F;
thus thesis by A7;
end;
uniqueness
proof
let F1,F2 be Function of V,Morphs(V) such that
A8: for G being Element of V holds F1.G = ID(G) and
A9: for G being Element of V holds F2.G = ID(G);
now let G be Element of V;
F1.G = ID(G) by A8;
hence F1.G = F2.G by A9;end;
hence thesis by FUNCT_2:113;
end;
end;
::
:: 4d. Category of left modules - superposition
::
theorem
Th10: for g,f being Element of Morphs(V) st dom'(g) = cod'(f)
ex G1,G2,G3 being strict Element of V st g is Morphism of G2,G3
& f is Morphism of G1,G2
proof
set X = Morphs(V);
defpred P[Element of X,Element of X] means dom'($1) = cod'($2);
let g,f be Element of X such that
A1: P[g,f];
consider G2,G3 being strict Element of V such that
A2: g is strict Morphism of G2,G3 by Def7;
dom(g) = dom'(g) by Def8;
then A3: G2 = dom'(g) by A2,MOD_2:def 11;
consider G1,G2' being strict Element of V such that
A4: f is strict Morphism of G1,G2' by Def7;
cod(f) = cod'(f) by Def9;
then G2' = cod'(f) by A4,MOD_2:def 11;
hence thesis by A1,A2,A3,A4;
end;
theorem
Th11: for g,f being Element of Morphs(V) st dom'(g) = cod'(f)
holds g*f in Morphs(V)
proof
set X = Morphs(V);
defpred P[Element of X,Element of X] means dom'($1) = cod'($2);
let g,f be Element of X; assume P[g,f];
then consider G1,G2,G3 being strict Element of V such that
A1: g is Morphism of G2,G3 & f is Morphism of G1,G2 by Th10;
reconsider g' = g as Morphism of G2,G3 by A1;
reconsider f' = f as Morphism of G1,G2 by A1;
g'*f' = g'*'f' by MOD_2:def 14;
hence thesis by Def7;
end;
theorem
Th12: for g,f being Element of Morphs(V) st dom(g) = cod(f)
holds g*f in Morphs(V)
proof
let g,f be Element of Morphs(V); assume
dom(g) = cod(f);
then dom'(g) = cod(f) by Def8 .= cod'(f) by Def9;
hence thesis by Th11;
end;
definition let R,V;
func comp(V) -> PartFunc of [:Morphs(V),Morphs(V):],Morphs(V) means
:Def14:
(for g,f being Element of Morphs(V) holds
[g,f] in dom it iff dom'(g) = cod'(f))
& (for g,f being Element of Morphs(V) st [g,f] in dom it holds
it.[g,f] = g*f);
existence
proof
set X = Morphs(V);
defpred P[Element of X,Element of X] means dom'($1) = cod'($2);
deffunc F(Element of X,Element of X) = $1*$2;
A1: for g,f being Element of X st P[g,f] holds F(g,f) in X by Th11;
consider c being PartFunc of [:X,X:],X such that
A2: for g,f being Element of X holds [g,f] in dom c iff P[g,f] and
A3: for g,f being Element of X st [g,f] in dom c
holds c.[g,f] = F(g,f) from PartLambda2D(A1);
take c;
thus thesis by A2,A3;
end;
uniqueness
proof
set X = Morphs(V);
defpred P[Element of X,Element of X] means dom'($1) = cod'($2);
let c1,c2 be PartFunc of [:X,X:],X such that
A4: for g,f being Element of X holds [g,f] in dom c1 iff P[g,f] and
A5: for g,f being Element of X st [g,f] in dom c1
holds c1.[g,f] = g*f and
A6: for g,f being Element of X holds [g,f] in dom c2 iff P[g,f] and
A7: for g,f being Element of X st [g,f] in dom c2
holds c2.[g,f] = g*f;
A8: dom c1 c= [:X,X:] & dom c2 c= [:X,X:] by RELSET_1:12;
A9: dom c1 = dom c2
proof
now let x; assume
A10: x in dom c1;
then consider g,f being Element of X such that
A11: x = [g,f] by A8,GRCAT_1:2;
P[g,f] by A4,A10,A11;
hence x in dom c2 by A6,A11;end;
then A12: dom c1 c= dom c2 by TARSKI:def 3;
now let x; assume
A13: x in dom c2;
then consider g,f being Element of X such that
A14: x = [g,f] by A8,GRCAT_1:2;
P[g,f] by A6,A13,A14;
hence x in dom c1 by A4,A14;end;
then dom c2 c= dom c1 by TARSKI:def 3;
hence thesis by A12,XBOOLE_0:def 10;
end;
set V0 = dom c1;
for x,y st [x,y] in V0 holds c1.[x,y]=c2.[x,y]
proof
let x,y;assume
A15: [x,y] in V0;
then reconsider x,y as Element of X by A8,ZFMISC_1:106;
c1.[x,y] = x*y by A5,A15;
hence thesis by A7,A9,A15;
end;
hence thesis by A9,PARTFUN1:35;
end;
end;
theorem
Th13: for g,f being Element of Morphs(V) holds
[g,f] in dom comp(V) iff dom(g) = cod(f)
proof
let g,f be Element of Morphs(V);
dom(g) = dom'(g) & cod(f) = cod'(f) by Def8,Def9;
hence thesis by Def14;
end;
::
:: 4e. Definition of Category of left modules
::
definition let UN,R;
func LModCat(UN,R) -> strict CatStr equals
:Def15: CatStr(#LModObjects(UN,R),Morphs(LModObjects(UN,R)),
dom(LModObjects(UN,R)),cod(LModObjects(UN,R)),
comp(LModObjects(UN,R)),ID(LModObjects(UN,R))#);
coherence;
end;
theorem
Th14: for f,g being Morphism of LModCat(UN,R) holds
[g,f] in dom(the Comp of LModCat(UN,R)) iff dom g = cod f
proof
set C = LModCat(UN,R), V = LModObjects(UN,R);
A1: C = CatStr(#V,Morphs(V),dom(V),cod(V),comp(V),ID(V)#) by Def15;
let f,g be Morphism of C;
reconsider f' = f as Element of Morphs(V) by A1;
reconsider g' = g as Element of Morphs(V) by A1;
A2: dom g = dom(V).g' by A1,CAT_1:def 2
.= dom'(g') by Def11
.= dom (g') by Def8;
A3: cod f = cod(V).f' by A1,CAT_1:def 3
.= cod'(f') by Def12
.= cod (f') by Def9;
A4: now assume [g,f] in dom(the Comp of C);
then dom' g' = cod' f' by A1,Def14
.= cod f' by Def9;
hence dom g = cod f by A2,A3,Def8;end;
now assume dom g = cod f;
then dom' g' = cod f' by A2,A3,Def8
.= cod' f' by Def9;
hence [g,f] in dom(the Comp of C) by A1,Def14;end;
hence thesis by A4;
end;
theorem
Th15: for f being (Morphism of LModCat(UN,R)),
f' being Element of Morphs(LModObjects(UN,R)),
b being Object of LModCat(UN,R),
b' being Element of LModObjects(UN,R)
holds f is strict Element of Morphs(LModObjects(UN,R))
& f' is Morphism of LModCat(UN,R)
& b is strict Element of LModObjects(UN,R)
& b' is Object of LModCat(UN,R)
proof
set C = LModCat(UN,R), V = LModObjects(UN,R); set X = Morphs(V);
A1: C = CatStr(#V,X,dom(V),cod(V),comp(V),ID(V)#) by Def15;
let f be (Morphism of C),
f' be Element of X,
b be Object of C,
b' be Element of V;
ex G,H being strict Element of V
st f is strict Morphism of G,H by A1,Def7;
hence f is strict Element of X by A1;
thus f' is Morphism of C by A1;
consider x such that
A2: x in {[G,ff] where G is Element of GroupObjects(UN),
ff is Element of Funcs([:the carrier of R,{{}}:],{{}
}) : not contradiction}
& GO x,b,R by A1,Def6;
ex x1,x2 being set st x = [x1,x2] &
ex G being strict LeftMod of R st b = G
& x1 = the LoopStr of G
& x2 = the lmult of G by A2,Def5;
hence b is strict Element of V by A1;
thus b' is Object of C by A1;
end;
theorem
Th16: for b being Object of LModCat(UN,R),
b' being Element of LModObjects(UN,R)
st b = b' holds id b = ID(b')
proof
set C = LModCat(UN,R), V = LModObjects(UN,R);
A1: C = CatStr(#V,(Morphs(V)),dom(V),cod(V),comp(V),ID(V)#) by Def15;
let b be Object of C, b' be Element of V; assume
b = b';
hence id b = (ID(V)).b' by A1,CAT_1:def 5
.= ID(b') by Def13;
end;
theorem
Th17: for f being Morphism of LModCat(UN,R)
for f' being Element of Morphs(LModObjects(UN,R))
st f = f'
holds dom f = dom f'
& cod f = cod f'
proof
set C = LModCat(UN,R), V = LModObjects(UN,R); set X = Morphs(V);
A1: C = CatStr(#V,X,dom(V),cod(V),comp(V),ID(V)#) by Def15;
let f be (Morphism of C), f' be Element of X; assume
A2: f = f';
hence dom f = dom(V).f' by A1,CAT_1:def 2
.= dom'(f') by Def11
.= dom (f') by Def8;
thus cod f = cod(V).f' by A1,A2,CAT_1:def 3
.= cod' f' by Def12
.= cod f' by Def9;
end;
theorem
Th18: for f,g being (Morphism of LModCat(UN,R)),
f',g' being Element of Morphs(LModObjects(UN,R))
st f = f' & g = g'
holds (dom g = cod f iff dom g' = cod f')
& (dom g = cod f iff [g',f'] in dom comp(LModObjects(UN,R)))
& (dom g = cod f implies g*f = g'*f')
& (dom f = dom g iff dom f' = dom g')
& (cod f = cod g iff cod f' = cod g')
proof
set C = LModCat(UN,R), V = LModObjects(UN,R); set X = Morphs(V);
A1: C = CatStr(#V,X,dom(V),cod(V),comp(V),ID(V)#) by Def15;
let f,g be Morphism of C;
let f',g' be Element of X; assume
A2: f = f' & g = g';
then A3: dom g = dom g' by Th17;
A4: cod f = cod f' by A2,Th17;
A5: dom f = dom f' by A2,Th17;
A6: cod g = cod g' by A2,Th17;
thus dom g = cod f iff dom g' = cod f' by A2,A4,Th17;
thus A7: dom g = cod f iff [g',f'] in dom comp(V)
by A3,A4,Th13;
thus dom g = cod f implies g*f = g'*f'
proof
assume A8: dom g = cod f;
then [g,f] in dom (the Comp of C) by Th14;
hence g*f = (comp(V)).[g',f'] by A1,A2,CAT_1:def 4
.= g'*f' by A7,A8,Def14;
end;
thus dom f = dom g iff dom f' = dom g' by A2,A5,Th17;
thus cod f = cod g iff cod f' = cod g' by A2,A6,Th17;
end;
Lm1: for f,g being Morphism of LModCat(UN,R) st dom g = cod f holds
dom(g*f) = dom f
& cod (g*f) = cod g
proof set X = Morphs((LModObjects(UN,R)));
let f,g be Morphism of (LModCat(UN,R)) such that
A1: dom g = cod f;
reconsider f' = f as strict Element of X by Th15;
reconsider g' = g as strict Element of X by Th15;
A2: dom g' = cod f' by A1,Th18;
then A3: dom(g'*f') = dom f'
& cod (g'*f') = cod g' by MOD_2:23;
reconsider gf = g'*f' as Element of X by A2,Th12;
gf = g*f by A1,Th18;
hence thesis by A3,Th18;
end;
Lm2: for f,g,h being Morphism of LModCat(UN,R)
st dom h = cod g & dom g = cod f holds h*(g*f) = (h*g)*f
proof set X = Morphs((LModObjects(UN,R)));
let f,g,h be Morphism of (LModCat(UN,R)) such that
A1: dom h = cod g & dom g = cod f;
reconsider f'=f, g'=g, h'=h as strict Element of X by Th15;
A2: dom h' = cod g' & dom g' = cod f' by A1,Th18;
A3: g'*f' = g*f & h'*g' = h*g by A1,Th18;
reconsider gf = g'*f', hg = h'*g' as strict Element of X by A2,Th12;
A4: dom(h) = cod(g*f) by A1,Lm1;
A5: dom(h*g) = cod(f) by A1,Lm1;
h*(g*f) = h'*gf by A3,A4,Th18
.= hg*f' by A2,MOD_2:25
.= (h*g)*f by A3,A5,Th18;
hence thesis;
end;
Lm3: for b being Object of LModCat(UN,R) holds
dom id b = b
& cod id b = b
& (for f being Morphism of LModCat(UN,R) st cod f = b holds (id b)*f = f)
& (for g being Morphism of LModCat(UN,R) st dom g = b holds g*(id b) = g)
proof
set C = LModCat(UN,R), V = LModObjects(UN,R); set X = Morphs(V);
let b be Object of C;
reconsider b' = b as Element of V by Th15;
reconsider b'' = b' as LeftMod of R;
A1: id b = ID(b') by Th16;
hence A2: dom id b = dom ID(b') by Th17
.= dom ID(b'') by Def10
.= b by MOD_2:26;
thus A3: cod id b = cod ID(b') by A1,Th17
.= cod ID(b'') by Def10
.= b by MOD_2:26;
thus for f being Morphism of C st cod f = b holds (id b)*f = f
proof
let f be Morphism of C such that
A4: cod f = b;
reconsider f1 = f as Element of X by Th15;
ex G,H being strict Element of V
st f1 is strict Morphism of G,H by Def7;
then reconsider f' = f1 as strict LModMorphism of R;
A5: cod f' = b'' by A4,Th17;
thus (id b)*f = ID(b')*f' by A1,A2,A4,Th18
.= ID(b'')*f' by Def10
.= f by A5,MOD_2:26;
end;
thus for g being Morphism of C st dom g = b holds g*(id b) = g
proof
let f be Morphism of C such that
A6: dom f = b;
reconsider f1 = f as Element of X by Th15;
ex G,H being strict Element of V
st f1 is strict Morphism of G,H by Def7;
then reconsider f' = f1 as strict LModMorphism of R;
A7: dom f' = b'' by A6,Th17;
thus f*(id b) = f'*ID(b') by A1,A3,A6,Th18
.= f'*ID(b'') by Def10
.= f by A7,MOD_2:26;
end;
end;
definition let UN,R;
cluster LModCat(UN,R) -> Category-like;
coherence
proof
( for f,g being Morphism of LModCat(UN,R)
holds [g,f] in dom(the Comp of LModCat(UN,R)) iff dom g = cod f )
& ( for f,g being Morphism of LModCat(UN,R) st dom g = cod f
holds dom(g*f) = dom f & cod (g*f) = cod g )
& ( for f,g,h being Morphism of LModCat(UN,R)
st dom h = cod g & dom g = cod f holds h*(g*f) = (h*g)*f )
& ( for b being Object of LModCat(UN,R)
holds dom id b = b & cod id b = b &
(for f being Morphism of LModCat(UN,R)
st cod f = b holds (id b)*f = f) &
(for g being Morphism of LModCat(UN,R)
st dom g = b holds g*(id b) = g) ) by Lm1,Lm2,Lm3,Th14;
hence thesis by CAT_1:29;
end;
end;