:: by Micha{\l} Muzalewski

::

:: Received December 12, 1991

:: Copyright (c) 1991-2018 Association of Mizar Users

definition

let R be Ring;

ex b_{1} being non empty set st

for x being Element of b_{1} holds x is strict LeftMod of R

end;
mode LeftMod_DOMAIN of R -> non empty set means :Def1: :: MODCAT_1:def 1

for x being Element of it holds x is strict LeftMod of R;

existence for x being Element of it holds x is strict LeftMod of R;

ex b

for x being Element of b

proof end;

:: deftheorem Def1 defines LeftMod_DOMAIN MODCAT_1:def 1 :

for R being Ring

for b_{2} being non empty set holds

( b_{2} is LeftMod_DOMAIN of R iff for x being Element of b_{2} holds x is strict LeftMod of R );

for R being Ring

for b

( b

definition

let R be Ring;

let V be LeftMod_DOMAIN of R;

:: original: Element

redefine mode Element of V -> LeftMod of R;

coherence

for b_{1} being Element of V holds b_{1} is LeftMod of R
by Def1;

end;
let V be LeftMod_DOMAIN of R;

:: original: Element

redefine mode Element of V -> LeftMod of R;

coherence

for b

registration

let R be Ring;

let V be LeftMod_DOMAIN of R;

ex b_{1} being Element of V st b_{1} is strict

end;
let V be LeftMod_DOMAIN of R;

cluster non empty right_complementable V99() V100() V101() strict V145(R) V146(R) V147(R) V148(R) for of ;

existence ex b

proof end;

definition

let R be Ring;

ex b_{1} being non empty set st

for x being Element of b_{1} holds x is strict LModMorphism of R

end;
mode LModMorphism_DOMAIN of R -> non empty set means :Def2: :: MODCAT_1:def 2

for x being Element of it holds x is strict LModMorphism of R;

existence for x being Element of it holds x is strict LModMorphism of R;

ex b

for x being Element of b

proof end;

:: deftheorem Def2 defines LModMorphism_DOMAIN MODCAT_1:def 2 :

for R being Ring

for b_{2} being non empty set holds

( b_{2} is LModMorphism_DOMAIN of R iff for x being Element of b_{2} holds x is strict LModMorphism of R );

for R being Ring

for b

( b

definition

let R be Ring;

let M be LModMorphism_DOMAIN of R;

:: original: Element

redefine mode Element of M -> LModMorphism of R;

coherence

for b_{1} being Element of M holds b_{1} is LModMorphism of R
by Def2;

end;
let M be LModMorphism_DOMAIN of R;

:: original: Element

redefine mode Element of M -> LModMorphism of R;

coherence

for b

registration

let R be Ring;

let M be LModMorphism_DOMAIN of R;

existence

ex b_{1} being Element of M st b_{1} is strict

end;
let M be LModMorphism_DOMAIN of R;

existence

ex b

proof end;

definition

let R be Ring;

let G, H be LeftMod of R;

ex b_{1} being LModMorphism_DOMAIN of R st

for x being Element of b_{1} holds x is strict Morphism of G,H

end;
let G, H be LeftMod of R;

mode LModMorphism_DOMAIN of G,H -> LModMorphism_DOMAIN of R means :Def3: :: MODCAT_1:def 3

for x being Element of it holds x is strict Morphism of G,H;

existence for x being Element of it holds x is strict Morphism of G,H;

ex b

for x being Element of b

proof end;

:: deftheorem Def3 defines LModMorphism_DOMAIN MODCAT_1:def 3 :

for R being Ring

for G, H being LeftMod of R

for b_{4} being LModMorphism_DOMAIN of R holds

( b_{4} is LModMorphism_DOMAIN of G,H iff for x being Element of b_{4} holds x is strict Morphism of G,H );

for R being Ring

for G, H being LeftMod of R

for b

( b

theorem Th2: :: MODCAT_1:2

for D being non empty set

for R being Ring

for G, H being LeftMod of R holds

( D is LModMorphism_DOMAIN of G,H iff for x being Element of D holds x is strict Morphism of G,H )

for R being Ring

for G, H being LeftMod of R holds

( D is LModMorphism_DOMAIN of G,H iff for x being Element of D holds x is strict Morphism of G,H )

proof end;

theorem :: MODCAT_1:3

for R being Ring

for G, H being LeftMod of R

for f being strict Morphism of G,H holds {f} is LModMorphism_DOMAIN of G,H

for G, H being LeftMod of R

for f being strict Morphism of G,H holds {f} is LModMorphism_DOMAIN of G,H

proof end;

definition

let R be Ring;

let G, H be LeftMod of R;

ex b_{1} being LModMorphism_DOMAIN of G,H st

for x being object holds

( x in b_{1} iff x is strict Morphism of G,H )

for b_{1}, b_{2} being LModMorphism_DOMAIN of G,H st ( for x being object holds

( x in b_{1} iff x is strict Morphism of G,H ) ) & ( for x being object holds

( x in b_{2} iff x is strict Morphism of G,H ) ) holds

b_{1} = b_{2}

end;
let G, H be LeftMod of R;

func Morphs (G,H) -> LModMorphism_DOMAIN of G,H means :Def4: :: MODCAT_1:def 4

for x being object holds

( x in it iff x is strict Morphism of G,H );

existence for x being object holds

( x in it iff x is strict Morphism of G,H );

ex b

for x being object holds

( x in b

proof end;

uniqueness for b

( x in b

( x in b

b

proof end;

:: deftheorem Def4 defines Morphs MODCAT_1:def 4 :

for R being Ring

for G, H being LeftMod of R

for b_{4} being LModMorphism_DOMAIN of G,H holds

( b_{4} = Morphs (G,H) iff for x being object holds

( x in b_{4} iff x is strict Morphism of G,H ) );

for R being Ring

for G, H being LeftMod of R

for b

( b

( x in b

definition

let R be Ring;

let G, H be LeftMod of R;

let M be LModMorphism_DOMAIN of G,H;

:: original: Element

redefine mode Element of M -> Morphism of G,H;

coherence

for b_{1} being Element of M holds b_{1} is Morphism of G,H
by Def3;

end;
let G, H be LeftMod of R;

let M be LModMorphism_DOMAIN of G,H;

:: original: Element

redefine mode Element of M -> Morphism of G,H;

coherence

for b

::

:: 4a. Category of left modules - objects

::

:: 4a. Category of left modules - objects

::

:: deftheorem defines GO MODCAT_1:def 5 :

for x, y being object

for R being Ring holds

( GO x,y,R iff ex x1, x2 being object st

( x = [x1,x2] & ex G being strict LeftMod of R st

( y = G & x1 = addLoopStr(# the carrier of G, the addF of G, the ZeroF of G #) & x2 = the lmult of G ) ) );

for x, y being object

for R being Ring holds

( GO x,y,R iff ex x1, x2 being object st

( x = [x1,x2] & ex G being strict LeftMod of R st

( y = G & x1 = addLoopStr(# the carrier of G, the addF of G, the ZeroF of G #) & x2 = the lmult of G ) ) );

theorem :: MODCAT_1:5

for R being Ring

for UN being Universe ex x being object st

( x in { [G,f] where G is Element of GroupObjects UN, f is Element of Funcs ([: the carrier of R,{{}}:],{{}}) : verum } & GO x, TrivialLMod R,R )

for UN being Universe ex x being object st

( x in { [G,f] where G is Element of GroupObjects UN, f is Element of Funcs ([: the carrier of R,{{}}:],{{}}) : verum } & GO x, TrivialLMod R,R )

proof end;

definition

let UN be Universe;

let R be Ring;

ex b_{1} being set st

for y being object holds

( y in b_{1} iff ex x being set st

( x in { [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) : verum } & GO x,y,R ) )

for b_{1}, b_{2} being set st ( for y being object holds

( y in b_{1} iff ex x being set st

( x in { [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) : verum } & GO x,y,R ) ) ) & ( for y being object holds

( y in b_{2} iff ex x being set st

( x in { [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) : verum } & GO x,y,R ) ) ) holds

b_{1} = b_{2}

end;
let R be Ring;

func LModObjects (UN,R) -> set means :Def6: :: MODCAT_1:def 6

for y being object holds

( y in it iff ex x being set st

( x in { [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) : verum } & GO x,y,R ) );

existence for y being object holds

( y in it iff ex x being set st

( x in { [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) : verum } & GO x,y,R ) );

ex b

for y being object holds

( y in b

( x in { [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) : verum } & GO x,y,R ) )

proof end;

uniqueness for b

( y in b

( x in { [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) : verum } & GO x,y,R ) ) ) & ( for y being object holds

( y in b

( x in { [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) : verum } & GO x,y,R ) ) ) holds

b

proof end;

:: deftheorem Def6 defines LModObjects MODCAT_1:def 6 :

for UN being Universe

for R being Ring

for b_{3} being set holds

( b_{3} = LModObjects (UN,R) iff for y being object holds

( y in b_{3} iff ex x being set st

( x in { [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) : verum } & GO x,y,R ) ) );

for UN being Universe

for R being Ring

for b

( b

( y in b

( x in { [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) : verum } & GO x,y,R ) ) );

registration
end;

theorem Th7: :: MODCAT_1:7

for UN being Universe

for R being Ring

for x being Element of LModObjects (UN,R) holds x is strict LeftMod of R

for R being Ring

for x being Element of LModObjects (UN,R) holds x is strict LeftMod of R

proof end;

definition

let UN be Universe;

let R be Ring;

:: original: LModObjects

redefine func LModObjects (UN,R) -> LeftMod_DOMAIN of R;

coherence

LModObjects (UN,R) is LeftMod_DOMAIN of R

end;
let R be Ring;

:: original: LModObjects

redefine func LModObjects (UN,R) -> LeftMod_DOMAIN of R;

coherence

LModObjects (UN,R) is LeftMod_DOMAIN of R

proof end;

::

:: 4b. Category of left modules - morphisms

::

:: 4b. Category of left modules - morphisms

::

definition

let R be Ring;

let V be LeftMod_DOMAIN of R;

ex b_{1} being LModMorphism_DOMAIN of R st

for x being object holds

( x in b_{1} iff ex G, H being strict Element of V st x is strict Morphism of G,H )

for b_{1}, b_{2} being LModMorphism_DOMAIN of R st ( for x being object holds

( x in b_{1} iff ex G, H being strict Element of V st x is strict Morphism of G,H ) ) & ( for x being object holds

( x in b_{2} iff ex G, H being strict Element of V st x is strict Morphism of G,H ) ) holds

b_{1} = b_{2}

end;
let V be LeftMod_DOMAIN of R;

func Morphs V -> LModMorphism_DOMAIN of R means :Def7: :: MODCAT_1:def 7

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 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 );

ex b

for x being object holds

( x in b

proof end;

uniqueness for b

( x in b

( x in b

b

proof end;

:: deftheorem Def7 defines Morphs MODCAT_1:def 7 :

for R being Ring

for V being LeftMod_DOMAIN of R

for b_{3} being LModMorphism_DOMAIN of R holds

( b_{3} = Morphs V iff for x being object holds

( x in b_{3} iff ex G, H being strict Element of V st x is strict Morphism of G,H ) );

for R being Ring

for V being LeftMod_DOMAIN of R

for b

( b

( x in b

::

:: 4c. Category of left modules - dom,cod,id

::

:: 4c. Category of left modules - dom,cod,id

::

definition

let R be Ring;

let V be LeftMod_DOMAIN of R;

let F be Element of Morphs V;

coherence

dom F is Element of V

cod F is Element of V

end;
let V be LeftMod_DOMAIN of R;

let F be Element of Morphs V;

coherence

dom F is Element of V

proof end;

coherence cod F is Element of V

proof end;

:: deftheorem defines dom' MODCAT_1:def 8 :

for R being Ring

for V being LeftMod_DOMAIN of R

for F being Element of Morphs V holds dom' F = dom F;

for R being Ring

for V being LeftMod_DOMAIN of R

for F being Element of Morphs V holds dom' F = dom F;

:: deftheorem defines cod' MODCAT_1:def 9 :

for R being Ring

for V being LeftMod_DOMAIN of R

for F being Element of Morphs V holds cod' F = cod F;

for R being Ring

for V being LeftMod_DOMAIN of R

for F being Element of Morphs V holds cod' F = cod F;

definition

let R be Ring;

let V be LeftMod_DOMAIN of R;

let G be Element of V;

coherence

ID G is strict Element of Morphs V

end;
let V be LeftMod_DOMAIN of R;

let G be Element of V;

coherence

ID G is strict Element of Morphs V

proof end;

:: deftheorem defines ID MODCAT_1:def 10 :

for R being Ring

for V being LeftMod_DOMAIN of R

for G being Element of V holds ID G = ID G;

for R being Ring

for V being LeftMod_DOMAIN of R

for G being Element of V holds ID G = ID G;

definition

let R be Ring;

let V be LeftMod_DOMAIN of R;

ex b_{1} being Function of (Morphs V),V st

for f being Element of Morphs V holds b_{1} . f = dom' f

for b_{1}, b_{2} being Function of (Morphs V),V st ( for f being Element of Morphs V holds b_{1} . f = dom' f ) & ( for f being Element of Morphs V holds b_{2} . f = dom' f ) holds

b_{1} = b_{2}

ex b_{1} being Function of (Morphs V),V st

for f being Element of Morphs V holds b_{1} . f = cod' f

for b_{1}, b_{2} being Function of (Morphs V),V st ( for f being Element of Morphs V holds b_{1} . f = cod' f ) & ( for f being Element of Morphs V holds b_{2} . f = cod' f ) holds

b_{1} = b_{2}

end;
let V be LeftMod_DOMAIN of R;

func dom V -> Function of (Morphs V),V means :Def11: :: MODCAT_1:def 11

for f being Element of Morphs V holds it . f = dom' f;

existence for f being Element of Morphs V holds it . f = dom' f;

ex b

for f being Element of Morphs V holds b

proof end;

uniqueness for b

b

proof end;

func cod V -> Function of (Morphs V),V means :Def12: :: MODCAT_1:def 12

for f being Element of Morphs V holds it . f = cod' f;

existence for f being Element of Morphs V holds it . f = cod' f;

ex b

for f being Element of Morphs V holds b

proof end;

uniqueness for b

b

proof end;

:: deftheorem Def11 defines dom MODCAT_1:def 11 :

for R being Ring

for V being LeftMod_DOMAIN of R

for b_{3} being Function of (Morphs V),V holds

( b_{3} = dom V iff for f being Element of Morphs V holds b_{3} . f = dom' f );

for R being Ring

for V being LeftMod_DOMAIN of R

for b

( b

:: deftheorem Def12 defines cod MODCAT_1:def 12 :

for R being Ring

for V being LeftMod_DOMAIN of R

for b_{3} being Function of (Morphs V),V holds

( b_{3} = cod V iff for f being Element of Morphs V holds b_{3} . f = cod' f );

for R being Ring

for V being LeftMod_DOMAIN of R

for b

( b

::

:: 4d. Category of left modules - superposition

::

:: 4d. Category of left modules - superposition

::

theorem Th8: :: MODCAT_1:8

for R being Ring

for V being LeftMod_DOMAIN of R

for g, f being Element of Morphs V st dom' g = cod' f holds

ex G1, G2, G3 being strict Element of V st

( g is Morphism of G2,G3 & f is Morphism of G1,G2 )

for V being LeftMod_DOMAIN of R

for g, f being Element of Morphs V st dom' g = cod' f holds

ex G1, G2, G3 being strict Element of V st

( g is Morphism of G2,G3 & f is Morphism of G1,G2 )

proof end;

theorem Th9: :: MODCAT_1:9

for R being Ring

for V being LeftMod_DOMAIN of R

for g, f being Element of Morphs V st dom' g = cod' f holds

g * f in Morphs V

for V being LeftMod_DOMAIN of R

for g, f being Element of Morphs V st dom' g = cod' f holds

g * f in Morphs V

proof end;

theorem Th10: :: MODCAT_1:10

for R being Ring

for V being LeftMod_DOMAIN of R

for g, f being Element of Morphs V st dom g = cod f holds

g * f in Morphs V

for V being LeftMod_DOMAIN of R

for g, f being Element of Morphs V st dom g = cod f holds

g * f in Morphs V

proof end;

definition

let R be Ring;

let V be LeftMod_DOMAIN of R;

ex b_{1} being PartFunc of [:(Morphs V),(Morphs V):],(Morphs V) st

( ( for g, f being Element of Morphs V holds

( [g,f] in dom b_{1} iff dom' g = cod' f ) ) & ( for g, f being Element of Morphs V st [g,f] in dom b_{1} holds

b_{1} . (g,f) = g * f ) )

for b_{1}, b_{2} being PartFunc of [:(Morphs V),(Morphs V):],(Morphs V) st ( for g, f being Element of Morphs V holds

( [g,f] in dom b_{1} iff dom' g = cod' f ) ) & ( for g, f being Element of Morphs V st [g,f] in dom b_{1} holds

b_{1} . (g,f) = g * f ) & ( for g, f being Element of Morphs V holds

( [g,f] in dom b_{2} iff dom' g = cod' f ) ) & ( for g, f being Element of Morphs V st [g,f] in dom b_{2} holds

b_{2} . (g,f) = g * f ) holds

b_{1} = b_{2}

end;
let V be LeftMod_DOMAIN of R;

func comp V -> PartFunc of [:(Morphs V),(Morphs V):],(Morphs V) means :Def13: :: MODCAT_1:def 14

( ( 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 ( ( 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 ) );

ex b

( ( for g, f being Element of Morphs V holds

( [g,f] in dom b

b

proof end;

uniqueness for b

( [g,f] in dom b

b

( [g,f] in dom b

b

b

proof end;

:: deftheorem Def13 defines comp MODCAT_1:def 14 :

for R being Ring

for V being LeftMod_DOMAIN of R

for b_{3} being PartFunc of [:(Morphs V),(Morphs V):],(Morphs V) holds

( b_{3} = comp V iff ( ( for g, f being Element of Morphs V holds

( [g,f] in dom b_{3} iff dom' g = cod' f ) ) & ( for g, f being Element of Morphs V st [g,f] in dom b_{3} holds

b_{3} . (g,f) = g * f ) ) );

for R being Ring

for V being LeftMod_DOMAIN of R

for b

( b

( [g,f] in dom b

b

theorem Th11: :: MODCAT_1:11

for R being Ring

for V being LeftMod_DOMAIN of R

for g, f being Element of Morphs V holds

( [g,f] in dom (comp V) iff dom g = cod f )

for V being LeftMod_DOMAIN of R

for g, f being Element of Morphs V holds

( [g,f] in dom (comp V) iff dom g = cod f )

proof end;

::

:: 4e. Definition of Category of left modules

::

:: 4e. Definition of Category of left modules

::

definition

let UN be Universe;

let R be Ring;

CatStr(# (LModObjects (UN,R)),(Morphs (LModObjects (UN,R))),(dom (LModObjects (UN,R))),(cod (LModObjects (UN,R))),(comp (LModObjects (UN,R))) #) is strict CatStr ;

end;
let R be Ring;

func LModCat (UN,R) -> strict CatStr equals :: MODCAT_1:def 15

CatStr(# (LModObjects (UN,R)),(Morphs (LModObjects (UN,R))),(dom (LModObjects (UN,R))),(cod (LModObjects (UN,R))),(comp (LModObjects (UN,R))) #);

coherence CatStr(# (LModObjects (UN,R)),(Morphs (LModObjects (UN,R))),(dom (LModObjects (UN,R))),(cod (LModObjects (UN,R))),(comp (LModObjects (UN,R))) #);

CatStr(# (LModObjects (UN,R)),(Morphs (LModObjects (UN,R))),(dom (LModObjects (UN,R))),(cod (LModObjects (UN,R))),(comp (LModObjects (UN,R))) #) is strict CatStr ;

:: deftheorem defines LModCat MODCAT_1:def 15 :

for UN being Universe

for R being Ring holds LModCat (UN,R) = CatStr(# (LModObjects (UN,R)),(Morphs (LModObjects (UN,R))),(dom (LModObjects (UN,R))),(cod (LModObjects (UN,R))),(comp (LModObjects (UN,R))) #);

for UN being Universe

for R being Ring holds LModCat (UN,R) = CatStr(# (LModObjects (UN,R)),(Morphs (LModObjects (UN,R))),(dom (LModObjects (UN,R))),(cod (LModObjects (UN,R))),(comp (LModObjects (UN,R))) #);

registration

let UN be Universe;

let R be Ring;

coherence

( not LModCat (UN,R) is void & not LModCat (UN,R) is empty ) ;

end;
let R be Ring;

coherence

( not LModCat (UN,R) is void & not LModCat (UN,R) is empty ) ;

theorem Th12: :: MODCAT_1:12

for UN being Universe

for R being Ring

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 R being Ring

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 end;

registration

let UN be Universe;

let R be Ring;

coherence

for b_{1} being Element of Morphs (LModObjects (UN,R)) holds b_{1} is strict

end;
let R be Ring;

coherence

for b

proof end;

::$CT 2

theorem Th13: :: MODCAT_1:15

for UN being Universe

for R being Ring

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 )

for R being Ring

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 end;

theorem Th14: :: MODCAT_1:16

for UN being Universe

for R being Ring

for f, g being Morphism of (LModCat (UN,R))

for f9, g9 being Element of Morphs (LModObjects (UN,R)) st f = f9 & g = g9 holds

( ( dom g = cod f implies dom g9 = cod f9 ) & ( dom g9 = cod f9 implies dom g = cod f ) & ( dom g = cod f implies [g9,f9] in dom (comp (LModObjects (UN,R))) ) & ( [g9,f9] in dom (comp (LModObjects (UN,R))) implies dom g = cod f ) & ( dom g = cod f implies g (*) f = g9 * f9 ) & ( dom f = dom g implies dom f9 = dom g9 ) & ( dom f9 = dom g9 implies dom f = dom g ) & ( cod f = cod g implies cod f9 = cod g9 ) & ( cod f9 = cod g9 implies cod f = cod g ) )

for R being Ring

for f, g being Morphism of (LModCat (UN,R))

for f9, g9 being Element of Morphs (LModObjects (UN,R)) st f = f9 & g = g9 holds

( ( dom g = cod f implies dom g9 = cod f9 ) & ( dom g9 = cod f9 implies dom g = cod f ) & ( dom g = cod f implies [g9,f9] in dom (comp (LModObjects (UN,R))) ) & ( [g9,f9] in dom (comp (LModObjects (UN,R))) implies dom g = cod f ) & ( dom g = cod f implies g (*) f = g9 * f9 ) & ( dom f = dom g implies dom f9 = dom g9 ) & ( dom f9 = dom g9 implies dom f = dom g ) & ( cod f = cod g implies cod f9 = cod g9 ) & ( cod f9 = cod g9 implies cod f = cod g ) )

proof end;

Lm1: for UN being Universe

for R being Ring

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 end;

Lm2: for UN being Universe

for R being Ring

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 end;

registration

let UN be Universe;

let R be Ring;

coherence

( LModCat (UN,R) is Category-like & LModCat (UN,R) is transitive & LModCat (UN,R) is associative & LModCat (UN,R) is reflexive )

end;
let R be Ring;

coherence

( LModCat (UN,R) is Category-like & LModCat (UN,R) is transitive & LModCat (UN,R) is associative & LModCat (UN,R) is reflexive )

proof end;

:: 2. Domains of left modules

::