I have no strong opinion whether to use ( X MndHom Y ) or ( X -Mnd-> Y ),
etc. Maybe the "Hom" in the current version makes it clearer that we are
talking about homomorphisms (it is a little bit more understandable).
Concerning the length we do not save anything. I think the current
convention is (or could be) consistent, if always <category>Hom is used as
symbol (unfortunately, RngHom was already used in a mathbox, so I had to
use RngHomo for nonunital ring homomorphisms - maybe I will rename the
current RngHom to RngHomOld and then my RngHomo to RngHom...). Besides
RngHomo, I also defined a magma homomorphism MgmHom.
df-map is a different topic, it should not be mixed with homomorphisms. And
there are reasons for the order of the arguments (see comment for df-map) -
although I still have to think twice often when using this definition...
Concerning Proposals 2 and 3, I agree with FL that the semantics of arrows
like >-> is difficult to remember (they are too similar). And since the
current symbols are used by Takeuti & Zaring (see Norm's comments), I would
favour to keep the current symbols.
Regards,
Alexander
On Thursday, April 16, 2020 at 1:45:38 PM UTC+2, Benoit wrote:
>
> 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/5788f3d9-5468-4e76-a2bb-84f69253e880%40googlegroups.com.
