FL asked me to post this.
-------- Forwarded Message --------
Subject: Arrows
Date: Fri, 17 Apr 2020 13:56:36 +0200 (CEST)
From:FL
Hi Norm,
I Hope you are fine.
Can you post that I like Benoît's arrows annotated with a subscript (Grp
etc.) but
that the semantics of arrows like >-> is difficult to remember. On the
HTML pages the subscripts are not correctly centered.
-FL
On Thursday, April 16, 2020 at 7:45:38 AM UTC-4, 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/6334559f-cf38-4cfe-a9ce-f4f9af77f4bb%40googlegroups.com.
