set C = LModCat (UN,R);
thus
LModCat (UN,R) is Category-like
( LModCat (UN,R) is transitive & LModCat (UN,R) is associative & LModCat (UN,R) is reflexive )proof
let f be
Morphism of
(LModCat (UN,R));
CAT_1:def 6 for b1 being Element of the carrier' of (LModCat (UN,R)) holds
( ( not [b1,f] in dom the Comp of (LModCat (UN,R)) or dom b1 = cod f ) & ( not dom b1 = cod f or [b1,f] in dom the Comp of (LModCat (UN,R)) ) )
thus
for
b1 being
Element of the
carrier' of
(LModCat (UN,R)) holds
( ( not
[b1,f] in dom the
Comp of
(LModCat (UN,R)) or
dom b1 = cod f ) & ( not
dom b1 = cod f or
[b1,f] in dom the
Comp of
(LModCat (UN,R)) ) )
by Th16;
verum
end;
thus
LModCat (UN,R) is transitive
( LModCat (UN,R) is associative & LModCat (UN,R) is reflexive )
thus
LModCat (UN,R) is associative
LModCat (UN,R) is reflexive
thus
LModCat (UN,R) is reflexive
verumproof
let a be
Element of
(LModCat (UN,R));
CAT_1:def 9 not Hom (a,a) = {}
reconsider G =
a as
Element of
LModObjects (
UN,
R) ;
consider x being
set such that
x in { [H,f] where H is Element of GroupObjects UN, f is Element of Funcs ([: the carrier of R,1:],1) : verum }
and W2:
GO x,
G,
R
by Def6;
set ii =
ID G;
consider x1,
x2 being
set such that
x = [x1,x2]
and W4:
ex
H being
strict LeftMod of
R st
(
G = H &
x1 = addLoopStr(# the
carrier of
H, the
addF of
H, the
ZeroF of
H #) &
x2 = the
lmult of
H )
by W2, Def5;
reconsider G =
G as
strict Element of
LModObjects (
UN,
R)
by W4;
reconsider ii =
ID G as
Morphism of
(LModCat (UN,R)) ;
reconsider ia =
ii as
LModMorphismStr over
R ;
A:
dom ii =
dom ia
by Th15
.=
a
by MOD_2:18
;
cod ii =
cod ia
by Th15
.=
a
by MOD_2:18
;
then
ii in Hom (
a,
a)
by A;
hence
Hom (
a,
a)
<> {}
;
verum
end;