begin
:: deftheorem Def1 defines LeftMod_DOMAIN MODCAT_1:def 1 :
for R being Ring
for b2 being non empty set holds
( b2 is LeftMod_DOMAIN of R iff for x being Element of b2 holds x is strict LeftMod of R );
:: deftheorem Def2 defines LModMorphism_DOMAIN MODCAT_1:def 2 :
for R being Ring
for b2 being non empty set holds
( b2 is LModMorphism_DOMAIN of R iff for x being Element of b2 holds x is strict LModMorphism of R );
theorem
canceled;
theorem
canceled;
theorem Th3:
:: deftheorem Def3 defines LModMorphism_DOMAIN MODCAT_1:def 3 :
for R being Ring
for G, H being LeftMod of R
for b4 being LModMorphism_DOMAIN of R holds
( b4 is LModMorphism_DOMAIN of G,H iff for x being Element of b4 holds x is strict Morphism of G,H );
theorem Th4:
theorem
definition
let R be
Ring;
let G,
H be
LeftMod of
R;
func Morphs G,
H -> LModMorphism_DOMAIN of
G,
H means :
Def4:
for
x being
set holds
(
x in it iff
x is
strict Morphism of
G,
H );
existence
ex b1 being LModMorphism_DOMAIN of G,H st
for x being set holds
( x in b1 iff x is strict Morphism of G,H )
uniqueness
for b1, b2 being LModMorphism_DOMAIN of G,H st ( for x being set holds
( x in b1 iff x is strict Morphism of G,H ) ) & ( for x being set holds
( x in b2 iff x is strict Morphism of G,H ) ) holds
b1 = b2
end;
:: deftheorem Def4 defines Morphs MODCAT_1:def 4 :
for R being Ring
for G, H being LeftMod of R
for b4 being LModMorphism_DOMAIN of G,H holds
( b4 = Morphs G,H iff for x being set holds
( x in b4 iff x is strict Morphism of G,H ) );
:: deftheorem Def5 defines GO MODCAT_1:def 5 :
for x, y being set
for R being Ring holds
( GO x,y,R iff ex x1, x2 being set 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 Th6:
for
R being
Ring for
x,
y1,
y2 being
set st
GO x,
y1,
R &
GO x,
y2,
R holds
y1 = y2
theorem Th7:
definition
let UN be
Universe;
let R be
Ring;
func LModObjects UN,
R -> set means :
Def6:
for
y being
set 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,1:],1 : verum } &
GO x,
y,
R ) );
existence
ex b1 being set st
for y being set holds
( y in b1 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,1:],1 : verum } & GO x,y,R ) )
uniqueness
for b1, b2 being set st ( for y being set holds
( y in b1 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,1:],1 : verum } & GO x,y,R ) ) ) & ( for y being set holds
( y in b2 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,1:],1 : verum } & GO x,y,R ) ) ) holds
b1 = b2
end;
:: deftheorem Def6 defines LModObjects MODCAT_1:def 6 :
for UN being Universe
for R being Ring
for b3 being set holds
( b3 = LModObjects UN,R iff for y being set holds
( y in b3 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,1:],1 : verum } & GO x,y,R ) ) );
theorem Th8:
theorem Th9:
:: deftheorem Def7 defines Morphs MODCAT_1:def 7 :
for R being Ring
for V being LeftMod_DOMAIN of R
for b3 being LModMorphism_DOMAIN of R holds
( b3 = Morphs V iff for x being set holds
( x in b3 iff ex G, H being strict Element of V st x is strict Morphism of G,H ) );
:: 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;
:: 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;
:: 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;
definition
let R be
Ring;
let V be
LeftMod_DOMAIN of
R;
func dom V -> Function of
(Morphs V),
V means :
Def11:
for
f being
Element of
Morphs V holds
it . f = dom' f;
existence
ex b1 being Function of (Morphs V),V st
for f being Element of Morphs V holds b1 . f = dom' f
uniqueness
for b1, b2 being Function of (Morphs V),V st ( for f being Element of Morphs V holds b1 . f = dom' f ) & ( for f being Element of Morphs V holds b2 . f = dom' f ) holds
b1 = b2
func cod V -> Function of
(Morphs V),
V means :
Def12:
for
f being
Element of
Morphs V holds
it . f = cod' f;
existence
ex b1 being Function of (Morphs V),V st
for f being Element of Morphs V holds b1 . f = cod' f
uniqueness
for b1, b2 being Function of (Morphs V),V st ( for f being Element of Morphs V holds b1 . f = cod' f ) & ( for f being Element of Morphs V holds b2 . f = cod' f ) holds
b1 = b2
func ID V -> Function of
V,
(Morphs V) means :
Def13:
for
G being
Element of
V holds
it . G = ID G;
existence
ex b1 being Function of V,(Morphs V) st
for G being Element of V holds b1 . G = ID G
uniqueness
for b1, b2 being Function of V,(Morphs V) st ( for G being Element of V holds b1 . G = ID G ) & ( for G being Element of V holds b2 . G = ID G ) holds
b1 = b2
end;
:: deftheorem Def11 defines dom MODCAT_1:def 11 :
for R being Ring
for V being LeftMod_DOMAIN of R
for b3 being Function of (Morphs V),V holds
( b3 = dom V iff for f being Element of Morphs V holds b3 . f = dom' f );
:: deftheorem Def12 defines cod MODCAT_1:def 12 :
for R being Ring
for V being LeftMod_DOMAIN of R
for b3 being Function of (Morphs V),V holds
( b3 = cod V iff for f being Element of Morphs V holds b3 . f = cod' f );
:: deftheorem Def13 defines ID MODCAT_1:def 13 :
for R being Ring
for V being LeftMod_DOMAIN of R
for b3 being Function of V,(Morphs V) holds
( b3 = ID V iff for G being Element of V holds b3 . G = ID G );
theorem Th10:
theorem Th11:
theorem Th12:
definition
let R be
Ring;
let V be
LeftMod_DOMAIN of
R;
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
ex b1 being PartFunc of [:(Morphs V),(Morphs V):],(Morphs V) st
( ( for g, f being Element of Morphs V holds
( [g,f] in dom b1 iff dom' g = cod' f ) ) & ( for g, f being Element of Morphs V st [g,f] in dom b1 holds
b1 . g,f = g * f ) )
uniqueness
for b1, b2 being PartFunc of [:(Morphs V),(Morphs V):],(Morphs V) st ( for g, f being Element of Morphs V holds
( [g,f] in dom b1 iff dom' g = cod' f ) ) & ( for g, f being Element of Morphs V st [g,f] in dom b1 holds
b1 . g,f = g * f ) & ( for g, f being Element of Morphs V holds
( [g,f] in dom b2 iff dom' g = cod' f ) ) & ( for g, f being Element of Morphs V st [g,f] in dom b2 holds
b2 . g,f = g * f ) holds
b1 = b2
end;
:: deftheorem Def14 defines comp MODCAT_1:def 14 :
for R being Ring
for V being LeftMod_DOMAIN of R
for b3 being PartFunc of [:(Morphs V),(Morphs V):],(Morphs V) holds
( b3 = comp V iff ( ( for g, f being Element of Morphs V holds
( [g,f] in dom b3 iff dom' g = cod' f ) ) & ( for g, f being Element of Morphs V st [g,f] in dom b3 holds
b3 . g,f = g * f ) ) );
theorem Th13:
definition
let UN be
Universe;
let R be
Ring;
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)),
(ID (LModObjects UN,R)) #);
coherence
CatStr(# (LModObjects UN,R),(Morphs (LModObjects UN,R)),(dom (LModObjects UN,R)),(cod (LModObjects UN,R)),(comp (LModObjects UN,R)),(ID (LModObjects UN,R)) #) is strict CatStr
;
end;
:: 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)),(ID (LModObjects UN,R)) #);
theorem Th14:
theorem Th15:
theorem Th16:
theorem Th17:
theorem Th18:
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 )
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
Lm3:
for UN being Universe
for R being Ring
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 ) )