Hi all,
I am asking for your opinions on the following proposals.
Proposal 1: There are already definitions in set.mm for morphisms in
various categories. In each case, the class of morphisms from A to B is
denoted by ( A token B ). For instance:
token label category
^m df-map Set <---- /!\ arguments reversed
MndHom df-mhm Mnd
GrpHom df-ghm Grp
RingHom df-rnghom Ring <---- I would relabel to df-ringhom
LMHom df-df-lmhm Mod <---- category of left modules
Cn df-cn Top
NGHom df-nghm NrmGrp
NMHom df-nmhm NrmMod
[other examples in depracted sections and mathboxes, also *OLD definitions
and other definitions that my basic search may have missed -- I did a
Ctrl-F on "hom" in mmdefinitions.html]
In order to make things more consistent and, in my opinion, more readable
and understandable, I propose to use instead the tokens:
-Set-> [maybe later, since the argument reversal would make it more work to
change]
-Mnd->
-Grp->
...
and use the unicode equivalent of the LaTex
\overset{\text{Set}}{\longrightarrow}. See the previous post
https://groups.google.com/d/topic/metamath/fghKk1HsCe4/discussion for the
unicode equivalent. See http://us2.metamath.org/mpeuni/df-bj-fset.html and
http://us2.metamath.org/mpeuni/df-bj-cur.html for examples of how it looks.
Proposal 2: There are also a few definitions for monomorphisms,
epimorphisms and isomorphisms (e.g. GrpIso, RingIso, LMIso, Homeo). I would
use the tokens:
>-Grp->
-Grp->>
>-Grp->>
respectively, using the unicode equivalent of the LaTeX \twoheadrightarrow,
\rightarrowtail, \twoheadrightarrowtail. These arrows are used with these
meanings in many texts. (Isomorphisms are often denoted by
\overset{\sim}{\longrightarrow} but I think using the combination of the
symbols for monomorphism and epimorphisms makes it clearer and avoids too
many decorations.)
Proposal 3: Since in the category of sets, the monomorphisms (resp.
epimorphisms, isomorphisms) are exactly the injective (resp. surjective,
bijective) functions, one would have the the classes ( A >-Set-> B ) etc. I
would also propose to make the replacements:
F : A -1-1-> --------> F : A >--> B
F : A -onto-> --------> F : A -->> B
F : A -1-1-onto-> --------> F : A >-->> B
with associated unicodes.
Note 1: As for the general notion, the class of morphisms from A to B in
the category C is denoted by ( A ( Hom ` C ) B ) which I think is
satisfactory. A standard notation in books is $\Hom_C (A, B)$.
Note 2: The set.mm-definition of module morphism is a bit strange. The most
common practice is to consider the category A-Mod of A-modules for some
fixed ring A. If one considers the category Mod of modules over arbitrary
rings, then the standard notion of morphism allows for different scalars
(i.e. a morphism is a couple (f,g) : (A,M) --> (B,N) where f : A -Ring-> B
and g(ax) = f(a)g(x)). Maybe the current definition was chosen because it
makes some uses easier ? Anyway, this is another matter.
Benoît
--
You received this message because you are subscribed to the Google Groups
"Metamath" group.
To unsubscribe from this group and stop receiving emails from it, send an email
to [email protected].
To view this discussion on the web visit
https://groups.google.com/d/msgid/metamath/261a6123-b3bd-40e5-a343-ec0265e77124%40googlegroups.com.
