begin
:: deftheorem Def1 defines LeftMod_DOMAIN MODCAT_1:def 1 :
:: deftheorem Def2 defines LModMorphism_DOMAIN MODCAT_1:def 2 :
theorem
canceled;
theorem
canceled;
theorem Th3:
:: deftheorem Def3 defines LModMorphism_DOMAIN MODCAT_1:def 3 :
theorem Th4:
theorem
definition
let R be
Ring;
let G,
H be
LeftMod of ;
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 :
:: deftheorem Def5 defines GO MODCAT_1:def 5 :
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 :
theorem Th8:
theorem Th9:
:: deftheorem Def7 defines Morphs MODCAT_1:def 7 :
:: deftheorem defines dom' MODCAT_1:def 8 :
:: deftheorem defines cod' MODCAT_1:def 9 :
:: deftheorem defines ID MODCAT_1:def 10 :
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 :
:: deftheorem Def12 defines cod MODCAT_1:def 12 :
:: deftheorem Def13 defines ID MODCAT_1:def 13 :
theorem Th10:
theorem Th11:
theorem Th12:
definition
let R be
Ring;
let V be
LeftMod_DOMAIN of
R;
func comp V -> PartFunc of ,
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 , 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 , 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 :
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 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 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 holds
( dom (id b) = b & cod (id b) = b & ( for f being Morphism of st cod f = b holds
(id b) * f = f ) & ( for g being Morphism of st dom g = b holds
g * (id b) = g ) )