### The Mizar article:

### Category of Left Modules

**by****Michal Muzalewski**

- Received December 12, 1991
Copyright (c) 1991 Association of Mizar Users

- MML identifier: MODCAT_1
- [ MML identifier index ]

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;

Back to top