Journal of Formalized Mathematics
Volume 3, 1991
University of Bialystok
Copyright (c) 1991 Association of Mizar Users

### Category of Left Modules

by
Michal Muzalewski

MML identifier: MODCAT_1
[ Mizar article, 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;

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
:: MODCAT_1:def 1
for x being Element of it holds x is strict LeftMod of R;
end;

reserve V for LeftMod_DOMAIN of R;

definition let R,V;
redefine mode Element of V -> LeftMod of R;
end;

definition let R,V;
cluster strict Element of V;
end;

definition let R;
mode LModMorphism_DOMAIN of R -> non empty set means
:: MODCAT_1:def 2
for x being Element of it holds x is strict LModMorphism of R;
end;

definition let R; let M be LModMorphism_DOMAIN of R;
redefine mode Element of M -> LModMorphism of R;
end;

definition let R; let M be LModMorphism_DOMAIN of R;
cluster strict Element of M;
end;

canceled 2;

theorem :: MODCAT_1:3
for f being strict LModMorphism of R
holds {f} is LModMorphism_DOMAIN of R;

definition let R,G,H;
mode LModMorphism_DOMAIN of G,H -> LModMorphism_DOMAIN of R means
:: MODCAT_1:def 3
for x being Element of it holds x is strict Morphism of G,H;
end;

theorem :: MODCAT_1:4
D is LModMorphism_DOMAIN of G,H
iff for x being Element of D holds x is strict Morphism of G,H;

theorem :: MODCAT_1:5
for f being strict Morphism of G,H holds {f} is LModMorphism_DOMAIN of G,H;

definition let R,G,H;
func Morphs(G,H) -> LModMorphism_DOMAIN of G,H means
:: MODCAT_1:def 4
x in it iff x is strict Morphism of G,H;
end;

definition let R,G,H; let M be LModMorphism_DOMAIN of G,H;
redefine mode Element of M -> Morphism of G,H;
end;

::
::  4a. Category of left modules - objects
::

definition let x,y,R;
pred GO x,y,R means
:: MODCAT_1:def 5
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 :: MODCAT_1:6
for x,y1,y2 being set st GO x,y1,R & GO x,y2,R holds y1 = y2;

theorem :: MODCAT_1:7
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;

definition let UN,R;
func LModObjects(UN,R) -> set means
:: MODCAT_1:def 6
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;
end;

theorem :: MODCAT_1:8
TrivialLMod(R) in LModObjects(UN,R);

definition let UN,R;
cluster LModObjects(UN,R) -> non empty;
end;

theorem :: MODCAT_1:9
for x being Element of LModObjects(UN,R)
holds x is strict LeftMod of R;

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

::
::  4b. Category of left modules - morphisms
::

definition let R,V;
func Morphs(V) -> LModMorphism_DOMAIN of R means
:: MODCAT_1:def 7
for x holds x in it iff ex G,H being strict Element of V
st x is strict Morphism of G,H;
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
:: MODCAT_1:def 8
dom(F);
func cod'(F) -> Element of V equals
:: MODCAT_1:def 9
cod(F);
end;

definition let R,V; let G be Element of V;
func ID(G) -> strict Element of Morphs(V) equals
:: MODCAT_1:def 10
ID(G);
end;

definition let R,V;
func dom(V) -> Function of Morphs(V),V means
:: MODCAT_1:def 11
for f being Element of Morphs(V) holds it.f = dom'(f);
func cod(V) -> Function of Morphs(V),V means
:: MODCAT_1:def 12
for f being Element of Morphs(V) holds it.f = cod'(f);
func ID(V) -> Function of V,Morphs(V) means
:: MODCAT_1:def 13
for G being Element of V holds it.G = ID(G);
end;

::
::  4d. Category of left modules - superposition
::

theorem :: MODCAT_1:10
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;

theorem :: MODCAT_1:11
for g,f being Element of Morphs(V) st dom'(g) = cod'(f)
holds g*f in Morphs(V);

theorem :: MODCAT_1:12
for g,f being Element of Morphs(V) st dom(g) = cod(f)
holds g*f in Morphs(V);

definition let R,V;
func comp(V) -> PartFunc of [:Morphs(V),Morphs(V):],Morphs(V) means
:: 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);
end;

theorem :: MODCAT_1:13
for g,f being Element of Morphs(V) holds
[g,f] in dom comp(V) iff dom(g) = cod(f);

::
::  4e. Definition of Category of left modules
::

definition let UN,R;
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)),ID(LModObjects(UN,R))#);
end;

theorem :: MODCAT_1:14
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;

theorem :: MODCAT_1:15
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);

theorem :: MODCAT_1:16
for b  being Object of LModCat(UN,R),
b' being Element of LModObjects(UN,R)
st b = b' holds id b = ID(b');

theorem :: MODCAT_1:17
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';

theorem :: MODCAT_1:18
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');

definition let UN,R;
cluster LModCat(UN,R) -> Category-like;
end;
```