:: Category of Left Modules
:: by Micha{\l} Muzalewski
::
:: Received December 12, 1991
:: Copyright (c) 1991-2017 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies 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 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;
constructors GRCAT_1, MOD_2, RELSET_1, FUNCT_5;
registrations XBOOLE_0, RELSET_1, STRUCT_0, CAT_1, VECTSP_2, GRCAT_1, MOD_2;
requirements SUBSET, BOOLE, NUMERALS;
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;
registration
let R,V;
cluster strict for 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;
registration
let R;
let M be LModMorphism_DOMAIN of R;
cluster strict for Element of M;
end;
theorem :: MODCAT_1:1
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:2
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:3
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
for x being object holds 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 be object; let R;
pred GO x,y,R means
:: MODCAT_1:def 5
ex x1,x2 being object st x = [x1,x2] &
ex G being strict LeftMod of R
st y = G & x1 = the addLoopStr of G & x2 = the lmult of G;
end;
theorem :: MODCAT_1:4
for x,y1,y2 being object st GO x,y1,R & GO x,y2,R holds y1 = y2;
theorem :: MODCAT_1:5
for UN
ex x being object st x in the set of all
[G,f] where G is Element of GroupObjects(UN)
, f is Element of Funcs([:the carrier of R,{{}}:],{{}})
& GO x, TrivialLMod(R),R;
definition
let UN,R;
func LModObjects(UN,R) -> set means
:: MODCAT_1:def 6
for y being object holds y in it iff
ex x st x in the set of all [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)
& GO x,y,R;
end;
theorem :: MODCAT_1:6
TrivialLMod(R) in LModObjects(UN,R);
registration
let UN,R;
cluster LModObjects(UN,R) -> non empty;
end;
theorem :: MODCAT_1:7
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 being object 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);
::$CD
end;
::
:: 4d. Category of left modules - superposition
::
theorem :: MODCAT_1:8
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:9
for g,f being Element of Morphs(V) st dom'(g) = cod'(f) holds g*
f in Morphs(V);
theorem :: MODCAT_1:10
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:11
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))
#);
end;
registration
let UN,R;
cluster LModCat(UN,R) -> non void non empty;
end;
theorem :: MODCAT_1:12
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;
registration let UN,R;
cluster -> strict for Element of Morphs LModObjects(UN,R);
end;
::$CT 2
theorem :: MODCAT_1:15
for f being Morphism of LModCat(UN,R) for f9 being Element of
Morphs(LModObjects(UN,R)) st f = f9 holds dom f = dom f9 & cod f = cod f9;
theorem :: MODCAT_1:16
for f,g being (Morphism of LModCat(UN,R)), f9,g9 being Element
of Morphs(LModObjects(UN,R)) st f = f9 & g = g9 holds (dom g = cod f iff dom g9
= cod f9) & (dom g = cod f iff [g9,f9] in dom comp(LModObjects(UN,R))) & (dom g
= cod f implies g(*)f = g9*f9) & (dom f = dom g iff dom f9 = dom g9) &
(cod f =
cod g iff cod f9 = cod g9);
registration
let UN,R;
cluster LModCat(UN,R) -> Category-like
transitive associative reflexive;
end;