:: Category of Left Modules
:: by Micha{\l} Muzalewski
::
:: Received December 12, 1991
:: Copyright (c) 1991-2026 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 XBOOLE_0, CLASSES2, FUNCSDOM, VECTSP_2, SUBSET_1, STRUCT_0,
MOD_2, MIDSP_1, CAT_1, GRCAT_1, FUNCT_2, ENS_1, RELAT_1, GRAPH_1,
FUNCT_1, ALGSTR_0, VECTSP_1, ZFMISC_1, MCART_1, TARSKI, ARYTM_3,
PARTFUN1, MODCAT_1, MSSUBFAM, UNIALG_1, MONOID_0, RELAT_2, BINOP_1,
CARD_1;
notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, RELAT_1, SETFAM_1, RELSET_1,
ORDINAL1, PARTFUN1, FUNCT_2, FUNCT_3, BINOP_1, FUNCT_5, STRUCT_0,
ALGSTR_0, VECTSP_1, VECTSP_2, GRAPH_1, CAT_1, CLASSES2, GRCAT_1, MOD_2;
constructors GRCAT_1, MOD_2, RELSET_1, FUNCT_5;
registrations XBOOLE_0, RELSET_1, STRUCT_0, CAT_1, VECTSP_2, GRCAT_1, MOD_2;
requirements SUBSET, BOOLE;
definitions CAT_1;
equalities ALGSTR_0, MOD_2, GRAPH_1, CAT_1, ORDINAL1;
expansions CAT_1;
theorems CAT_1, GRCAT_1, FUNCT_2, MOD_2, TARSKI, ZFMISC_1, XBOOLE_0, BINOP_1,
SUBSET_1, XTUPLE_0;
schemes FUNCT_2, BINOP_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; :: redefines Element (SUBSET_1, definition)
coherence by Def1;
end;
registration
let R,V;
cluster strict for Element of V;
existence
proof
set e = the 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
set G = the LeftMod of R;
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; :: redefines Element (SUBSET_1, definition)
coherence by Def2;
end;
registration
let R;
let M be LModMorphism_DOMAIN of R;
cluster strict for Element of M;
existence
proof
set e = the Element of M;
take e;
thus thesis by Def2;
end;
end;
theorem Th1:
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 Th1;
take D;
thus thesis by TARSKI:def 1;
end;
end;
theorem Th2:
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 D9 = D as LModMorphism_DOMAIN of R by Def2;
for x being Element of D9 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 Th2;
end;
definition
let R,G,H;
func Morphs(G,H) -> LModMorphism_DOMAIN of G,H means
:Def4:
for x being object holds x in it iff x is strict Morphism of G,H;
existence
proof
ZeroMap(G,H) is Element of Funcs(the carrier of G, the carrier of H)
by FUNCT_2:8;
then reconsider f0 = ZeroMap(G,H) as Element of Maps(G,H) by GRCAT_1:def 21
;
set D = { LModMorphismStr(# G,H,f#) where f is Element of Maps(G,H) : f is
additive homogeneous };
LModMorphismStr(# G,H,f0#) in D;
then reconsider D as non empty set;
A1: for x being object holds x is strict Morphism of G,H implies x in D
proof let x be object;
assume x is strict Morphism of G,H;
then reconsider x as strict Morphism of G,H;
dom(x) = G by MOD_2:def 8;
then
A2: the DomL of x = G;
A3: cod(x) = H by MOD_2:def 8;
then the CodL of x = H;
then reconsider f = the Fun of x as Function of G,H by A2;
f is Element of Funcs(the carrier of G, the carrier of H) by FUNCT_2:8;
then reconsider g = f as Element of Maps(G,H) by GRCAT_1:def 21;
(the Fun of x) is additive homogeneous &
x = LModMorphismStr(# G,H,g #) by A3,A2,MOD_2:4;
hence thesis;
end;
A4: for x being object holds x in D implies x is strict Morphism of G,H
proof let x be object;
assume x in D;
then
ex f being Element of Maps(G,H) st x = LModMorphismStr (#G,H,f#) & f
is additive homogeneous;
hence thesis by MOD_2:6;
end;
then for x being Element of D holds x is strict Morphism of G,H;
then reconsider D as LModMorphism_DOMAIN of G,H by Th2;
take D;
thus thesis by A4,A1;
end;
uniqueness
proof
let D1,D2 be LModMorphism_DOMAIN of G,H such that
A5: for x being object holds x in D1 iff x is strict Morphism of G,H and
A6: for x being object holds x in D2 iff x is strict Morphism of G,H;
for x being object holds x in D1 iff x in D2
proof let x be object;
hereby
assume x in D1;
then x is strict Morphism of G,H by A5;
hence x in D2 by A6;
end;
assume x in D2;
then x is strict Morphism of G,H by A6;
hence thesis by A5;
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; :: redefines Element (SUBSET_1, definition)
coherence by Def3;
end;
::
:: 4a. Category of left modules - objects
::
definition
let x,y be object; let R;
pred GO x,y,R means
ex x1,x2 being object st x = [x1,x2] &
ex G being strict LeftMod of R
st y = G & x1 = the addLoopStr of G & x2 = the lmult of G;
end;
theorem Th4:
for x,y1,y2 being object st GO x,y1,R & GO x,y2,R holds y1 = y2
proof
let x,y1,y2 be object such that
A1: GO x,y1,R and
A2: GO x,y2,R;
consider a1,a2 being object such that
A3: x = [a1,a2] and
A4: ex G being strict LeftMod of R st y1 = G & a1 = the addLoopStr of G
& a2 = the lmult of G by A1;
consider G1 being strict LeftMod of R such that
A5: y1 = G1 and
A6: a1 = the addLoopStr of G1 and
A7: a2 = the lmult of G1 by A4;
consider b1,b2 being object such that
A8: x = [b1,b2] and
A9: ex G being strict LeftMod of R st y2 = G & b1 = the addLoopStr of G
& b2 = the lmult of G by A2;
consider G2 being strict LeftMod of R such that
A10: y2 = G2 and
A11: b1 = the addLoopStr of G2 and
A12: b2 = the lmult of G2 by A9;
the addLoopStr of G1 = the addLoopStr of G2 by A3,A8,A6,A11,XTUPLE_0:1;
hence thesis by A3,A8,A5,A7,A10,A12,XTUPLE_0:1;
end;
theorem
for UN
ex x being object st x in the set of all
[G,f] where G is Element of GroupObjects(UN)
, f is Element of Funcs([:the carrier of R,{{}}:],{{}})
& GO x, TrivialLMod(R),R
proof
let UN;
set T = TrivialLMod(R);
reconsider x1 = the addLoopStr of T as Element of GroupObjects(UN)
by GRCAT_1:29;
reconsider f1 = the lmult of T as Function of [:the carrier of R,{{}}:],{{}};
reconsider x2 = f1 as Element of Funcs([:the carrier of R,{{}}:],{{}})
by FUNCT_2:8;
take x = [x1,x2];
thus x in the set of all
[G,f] where G is Element of GroupObjects(UN), f is Element of
Funcs([:the carrier of R,{{}}:],{{}}) ;
thus thesis;
end;
definition
let UN,R;
func LModObjects(UN,R) -> set means
:Def6:
for y being object holds y in it iff
ex x st x in the set of all [G,f] where G is Element of GroupObjects(UN),
f is Element of Funcs([:the carrier of R,the carrier of G:],
the carrier of G)
& GO x,y,R;
existence
proof
defpred P[object,object] means GO $1,$2,R;
set N = the set of all
[G,f] where G is Element of GroupObjects(UN), f is Element of
Funcs([:the carrier of R,the carrier of G:],
the carrier of G) ;
A1: for x,y1,y2 being object st P[x,y1] & P[x,y2] holds y1 = y2 by Th4;
consider Y being set such that
A2: for y being object holds y in Y iff
ex x being object st x in N & P[x,y] from TARSKI:sch 1(A1);
take Y;
let y be object;
thus y in Y implies ex x st x
in the set of all [G,f] where G is Element of GroupObjects(UN),
f is Element of Funcs([:the carrier of R,the carrier of G:],
the carrier of G)
& GO x,y,R
proof assume y in Y;
then ex x being object st x in N & P[x,y] by A2;
hence thesis;
end;
thus thesis by A2;
end;
uniqueness
proof
set N = the set of all
[G,f] where G is Element of GroupObjects(UN), f is Element of
Funcs([:the carrier of R,the carrier of G:],
the carrier of G) ;
let Y1,Y2 be set such that
A3: for y being object holds y in Y1 iff ex x st x in N & GO x,y,R and
A4: for y being object holds y in Y2 iff ex x st x in N & GO x,y,R;
now
let y be object;
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 Th6:
TrivialLMod(R) in LModObjects(UN,R)
proof
set G0 = Trivial-addLoopStr, f0 = pr2(the carrier of R,{0});
reconsider G0 as Element of GroupObjects(UN) by GRCAT_1:29;
reconsider f0 as Element of Funcs([:the carrier of R,the carrier of G0:],
the carrier of G0) by FUNCT_2:8;
set x = [G0,f0];
A1: x in the set of all
[G,f] where G is Element of GroupObjects(UN), f is Element
of Funcs([:the carrier of R,the carrier of G:],
the carrier of G) ;
GO x,TrivialLMod(R),R;
hence thesis by A1,Def6;
end;
registration
let UN,R;
cluster LModObjects(UN,R) -> non empty;
coherence by Th6;
end;
theorem Th7:
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 = the set of all
[G,f] where G is Element of GroupObjects(UN), f is Element of Funcs
([:the carrier of R,the carrier of G:],
the carrier of G) ;
consider u being set such that
u in N and
A1: GO u,x,R by Def6;
ex a1,a2 being object st u = [a1,a2] & ex G being strict LeftMod of R st x
= G & a1 = the addLoopStr of G & a2 = the lmult of G by A1;
hence thesis;
end;
definition
let UN,R;
redefine func LModObjects(UN,R) -> LeftMod_DOMAIN of R; :: redefines LModObjects (MODCAT_1, definition)
coherence
proof
for x being Element of LModObjects(UN,R) holds x is strict LeftMod of
R by Th7;
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 being object holds x in it
iff ex G,H being strict Element of V st x is strict Morphism of G,H;
existence
proof
set G0 = the strict Element of V;
set M = Morphs(G0,G0), S = the set of all
Morphs(G,H) where G is strict Element of V, H
is strict Element of V ;
(ZERO(G0,G0)) is Element of M & M in S by Def4;
then reconsider T = union S as non empty set by TARSKI:def 4;
A1: for x being object
holds x in T iff ex G,H being strict Element of V st x is strict
Morphism of G,H
proof
let x be object;
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
A2: x in Y and
A3: Y in S by TARSKI:def 4;
consider G,H being strict Element of V such that
A4: Y = Morphs(G,H) by A3;
take G,H;
thus thesis by A2,A4,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
A5: x is strict Morphism of G,H;
set M = Morphs(G,H);
A6: M in S;
x in M by A5,Def4;
hence thesis by A6,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 A1;
hence x is strict LModMorphism of R;
end;
then reconsider T9 = T as LModMorphism_DOMAIN of R by Def2;
take T9;
thus thesis by A1;
end;
uniqueness
proof
let D1,D2 be LModMorphism_DOMAIN of R such that
A7: for x being object
holds x in D1 iff ex G,H being strict Element of V st x is
strict Morphism of G,H and
A8: for x being object
holds x in D2 iff ex G,H being strict Element of V st x is
strict Morphism of G,H;
now
let x be object;
x in D1 iff ex G,H being strict Element of V st x is strict
Morphism of G,H by A7;
hence x in D1 iff x in D2 by A8;
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
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 F9 = F as Morphism of G,H by A1;
dom(F9) = G by MOD_2:def 8;
hence thesis;
end;
func cod'(F) -> Element of V equals
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 F9 = F as Morphism of G,H by A2;
cod(F9) = H by MOD_2:def 8;
hence thesis;
end;
end;
definition
let R,V;
let G be Element of V;
func ID(G) -> strict Element of Morphs(V) equals
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 FUNCT_2:sch
4;
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:63;
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 FUNCT_2:sch
4;
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:63;
end;
::$CD
end;
::
:: 4d. Category of left modules - superposition
::
theorem Th8:
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;
consider G1,G29 being strict Element of V such that
A3: f is strict Morphism of G1,G29 by Def7;
A4: G29 = cod'(f) by A3,MOD_2:def 8;
G2 = dom'(g) by A2,MOD_2:def 8;
hence thesis by A1,A2,A3,A4;
end;
theorem Th9:
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 and
A2: f is Morphism of G1,G2 by Th8;
reconsider f9 = f as Morphism of G1,G2 by A2;
reconsider g9 = g as Morphism of G2,G3 by A1;
g9*f9 = g9*'f9;
hence thesis by Def7;
end;
theorem Th10:
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);
hence thesis by Th9;
end;
definition
let R,V;
func comp(V) -> PartFunc of [:Morphs(V),Morphs(V):],Morphs(V) means
:Def13:
(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 Th9;
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])& for
g,f being Element of X st [g,f] in dom c holds c.(g,f) = F(g,f) from BINOP_1:
sch 8(A1);
take c;
thus thesis by A2;
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
A3: for g,f being Element of X holds [g,f] in dom c1 iff P[g,f] and
A4: for g,f being Element of X st [g,f] in dom c1 holds c1.(g,f) = g*f and
A5: for g,f being Element of X holds [g,f] in dom c2 iff P[g,f] and
A6: for g,f being Element of X st [g,f] in dom c2 holds c2.(g,f) = g*f;
set V0 = dom c1;
now
let x be object;
assume
A7: x in dom c1;
then consider g,f being Element of X such that
A8: x = [g,f] by SUBSET_1:43;
P[g,f] by A3,A7,A8;
hence x in dom c2 by A5,A8;
end;
then
A9: dom c1 c= dom c2 by TARSKI:def 3;
A10: for x,y being object st [x,y] in V0 holds c1.(x,y)=c2.(x,y)
proof
let x,y be object;
assume
A11: [x,y] in V0;
then reconsider x,y as Element of X by ZFMISC_1:87;
c1.(x,y) = x*y by A4,A11;
hence thesis by A6,A9,A11;
end;
now
let x be object;
assume
A12: x in dom c2;
then consider g,f being Element of X such that
A13: x = [g,f] by SUBSET_1:43;
P[g,f] by A5,A12,A13;
hence x in dom c1 by A3,A13;
end;
then dom c2 c= dom c1 by TARSKI:def 3;
then dom c1 = dom c2 by A9,XBOOLE_0:def 10;
hence thesis by A10,BINOP_1:20;
end;
end;
theorem Th11:
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);
hence thesis by Def13;
end;
::
:: 4e. Definition of Category of left modules
::
definition
let UN,R;
func LModCat(UN,R) -> strict CatStr equals
CatStr(#LModObjects(UN,R),Morphs(
LModObjects(UN,R)), dom(LModObjects(UN,R)),cod(LModObjects(UN,R)), comp(
LModObjects(UN,R))
#);
coherence;
end;
registration
let UN,R;
cluster LModCat(UN,R) -> non void non empty;
coherence;
end;
theorem Th12:
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);
let f,g be Morphism of C;
reconsider f9 = f as Element of Morphs(V);
reconsider g9 = g as Element of Morphs(V);
A1: cod f = cod'(f9) by Def12
.= cod (f9);
A2: dom g = dom'(g9) by Def11
.= dom (g9);
A3: now
assume dom g = cod f;
then dom' g9 = cod' f9 by A2,A1;
hence [g,f] in dom(the Comp of C) by Def13;
end;
now
assume [g,f] in dom(the Comp of C);
then dom' g9 = cod' f9 by Def13
.= cod f9;
hence dom g = cod f by A2,A1;
end;
hence thesis by A3;
end;
registration let UN,R;
cluster -> strict for Element of Morphs LModObjects(UN,R);
coherence
proof
set V = LModObjects(UN,R);
let f be Element of Morphs V;
ex G,H being strict Element of V st f is strict Morphism of G,H by Def7;
hence f is strict;
end;
end;
::$CT 2
theorem Th13:
for f being Morphism of LModCat(UN,R) for f9 being Element of
Morphs(LModObjects(UN,R)) st f = f9 holds dom f = dom f9 & cod f = cod f9
proof
set C = LModCat(UN,R), V = LModObjects(UN,R);
set X = Morphs(V);
let f be (Morphism of C), f9 be Element of X;
assume
A1: f = f9;
hence dom f = dom'(f9) by Def11
.= dom (f9);
thus cod f = cod' f9 by A1,Def12
.= cod f9;
end;
theorem Th14:
for f,g being (Morphism of LModCat(UN,R)), f9,g9 being Element
of Morphs(LModObjects(UN,R)) st f = f9 & g = g9 holds (dom g = cod f iff dom g9
= cod f9) & (dom g = cod f iff [g9,f9] in dom comp(LModObjects(UN,R))) & (dom g
= cod f implies g(*)f = g9*f9) & (dom f = dom g iff dom f9 = dom g9) &
(cod f =
cod g iff cod f9 = cod g9)
proof
set C = LModCat(UN,R), V = LModObjects(UN,R);
set X = Morphs(V);
let f,g be Morphism of C;
let f9,g9 be Element of X;
assume that
A1: f = f9 and
A2: g = g9;
A3: cod f = cod f9 by A1,Th13;
hence dom g = cod f iff dom g9 = cod f9 by A2,Th13;
dom g = dom g9 by A2,Th13;
hence
A4: dom g = cod f iff [g9,f9] in dom comp(V) by A3,Th11;
thus dom g = cod f implies g(*)f = g9*f9
proof
assume
A5: dom g = cod f;
then [g,f] in dom (the Comp of C) by Th12;
hence g(*)f = (comp(V)).(g9,f9) by A1,A2,CAT_1:def 1
.= g9*f9 by A4,A5,Def13;
end;
dom f = dom f9 by A1,Th13;
hence dom f = dom g iff dom f9 = dom g9 by A2,Th13;
cod g = cod g9 by A2,Th13;
hence thesis by A1,Th13;
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 g9 = g as strict Element of X;
reconsider f9 = f as strict Element of X;
A2: dom g9 = cod f9 by A1,Th14;
then
A3: dom(g9*f9) = dom f9 & cod (g9*f9) = cod g9 by MOD_2:15;
reconsider gf = g9*f9 as Element of X by A2,Th10;
gf = g(*)f by A1,Th14;
hence thesis by A3,Th14;
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 f9=f, g9=g, h9=h as strict Element of X;
A2: h9*g9 = h(*)g & dom(h(*)g) = cod(f) by A1,Lm1,Th14;
A3: dom h9 = cod g9 & dom g9 = cod f9 by A1,Th14;
then reconsider gf = g9*f9, hg = h9*g9 as strict Element of X by Th10;
g9*f9 = g(*)f & dom(h) = cod(g(*)f) by A1,Lm1,Th14;
then h(*)(g(*)f) = h9*gf by Th14
.= hg*f9 by A3,MOD_2:17
.= (h(*)g)(*)f by A2,Th14;
hence thesis;
end;
registration
let UN,R;
cluster LModCat(UN,R) -> Category-like
transitive associative reflexive;
coherence
proof set C = LModCat(UN,R);
thus C is Category-like
by Th14;
thus C is transitive
by Lm1;
thus C is associative
by Lm2;
thus C is reflexive
proof let a be Element of C;
reconsider G = a as Element of LModObjects(UN,R);
consider x such that
x in the set of all [H,f]
where H is Element of GroupObjects(UN),
f is Element of Funcs([:the carrier of R,the carrier of H:],
the carrier of H)
and
A1: GO x,G,R by Def6;
set ii = ID G;
consider x1,x2 being object such that
x = [x1,x2] and
A2: ex H being strict LeftMod of R
st G = H & x1 = the addLoopStr of H & x2 = the lmult of H
by A1;
reconsider G as strict Element of LModObjects(UN,R) by A2;
reconsider ii as Morphism of C;
reconsider ia = ii as LModMorphismStr over R;
A3: dom ii = dom ia by Th13
.= a;
cod ii = cod ia by Th13
.= a;
then ii in Hom(a,a) by A3;
hence Hom(a,a)<>{};
end;
end;
end;