environ
vocabularies HIDDEN, XBOOLE_0, CLASSES2, FUNCSDOM, VECTSP_2, SUBSET_1, STRUCT_0, MOD_2, MIDSP_1, CAT_1, GRCAT_1, FUNCT_2, ENS_1, RELAT_1, GRAPH_1, FUNCT_1, ALGSTR_0, VECTSP_1, ZFMISC_1, MCART_1, TARSKI, ARYTM_3, PARTFUN1, MODCAT_1, MSSUBFAM, UNIALG_1, MONOID_0, RELAT_2, BINOP_1, CARD_1;
notations HIDDEN, TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, RELAT_1, SETFAM_1, RELSET_1, ORDINAL1, PARTFUN1, FUNCT_2, FUNCT_3, BINOP_1, FUNCT_5, STRUCT_0, ALGSTR_0, VECTSP_1, VECTSP_2, GRAPH_1, CAT_1, CLASSES2, GRCAT_1, MOD_2;
definitions CAT_1;
theorems CAT_1, GRCAT_1, FUNCT_2, MOD_2, TARSKI, ZFMISC_1, XBOOLE_0, BINOP_1, SUBSET_1, XTUPLE_0;
schemes FUNCT_2, BINOP_1, TARSKI;
registrations XBOOLE_0, RELSET_1, STRUCT_0, CAT_1, VECTSP_2, GRCAT_1, MOD_2;
constructors HIDDEN, GRCAT_1, MOD_2, RELSET_1, FUNCT_5;
requirements HIDDEN, SUBSET, BOOLE, NUMERALS;
equalities ALGSTR_0, MOD_2, GRAPH_1, CAT_1, ORDINAL1;
expansions CAT_1;
theorem Th4:
for
R being
Ring for
x,
y1,
y2 being
object st
GO x,
y1,
R &
GO x,
y2,
R holds
y1 = y2
definition
let UN be
Universe;
let R be
Ring;
existence
ex b1 being set st
for y being object 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, the carrier of G:], the carrier of G) : verum } & GO x,y,R ) )
uniqueness
for b1, b2 being set st ( for y being object 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, the carrier of G:], the carrier of G) : verum } & GO x,y,R ) ) ) & ( for y being object 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, the carrier of G:], the carrier of G) : verum } & GO x,y,R ) ) ) holds
b1 = b2
end;
definition
let R be
Ring;
let V be
LeftMod_DOMAIN of
R;
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;
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))) #);
coherence
CatStr(# (LModObjects (UN,R)),(Morphs (LModObjects (UN,R))),(dom (LModObjects (UN,R))),(cod (LModObjects (UN,R))),(comp (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))) #);
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
:: 2. Domains of left modules
::