Denoting morphisms in set.mm
94 views
Skip to first unread message
Benoit
Apr 16, 2020, 7:45:38 AM4/16/20
to Metamath
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
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
Norman Megill
Apr 18, 2020, 9:03:26 AM4/18/20
to Metamath
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
-------- 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
Norman Megill
Apr 18, 2020, 10:14:46 AM4/18/20
to Metamath
Regarding:
F : A -1-1-> --------> F : A >--> B
F : A -onto-> --------> F : A -->> B
F : A -1-1-onto-> --------> F : A >-->> B
Do you have a textbook reference for the new symbols you propose?
The current symbols we use are from Takeuti & Zaring. The are rendered exactly as in the book on the GIF pages. There are no Unicode symbols for them, so we provided a rough approximation (putting the symbol parts in a line instead of stacked vertically).
Norm
The current symbols we use are from Takeuti & Zaring. The are rendered exactly as in the book on the GIF pages. There are no Unicode symbols for them, so we provided a rough approximation (putting the symbol parts in a line instead of stacked vertically).
Norm
David Starner
Apr 18, 2020, 10:56:23 AM4/18/20
to meta...@googlegroups.com
they're being used, and I've helped get a couple characters added in
the past.
--
The standard is written in English . If you have trouble understanding
a particular section, read it again and again and again . . . Sit up
straight. Eat your vegetables. Do not mumble. -- _Pascal_, ISO 7185
(1991)
Alexander van der Vekens
Apr 19, 2020, 4:39:36 AM4/19/20
to meta...@googlegroups.com
... there are two topics in StackExchange containing such symbols:
Unfortunately, there is no reference to a textbook...
Alexander
Alexander van der Vekens
Apr 19, 2020, 5:00:29 AM4/19/20
to Metamath
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
Mario Carneiro
Apr 19, 2020, 5:10:46 AM4/19/20
to metamath
Regarding df-map, I would be in favor of reversing the argument order and changing the symbol to an arrow of some sort. I find that much easier to think about and I mix up the order literally every time. The number of times I want to think of this as an exponential is a small fraction of the number of times I want to think of this as a set version of the A --> B in F : A --> B. It makes things like F : A --> ( C ^m B ) unnecessarily difficult to understand, and every other function space constructor like Cn and all the Homs have the opposite argument order.
--
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 metamath+u...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/5788f3d9-5468-4e76-a2bb-84f69253e880%40googlegroups.com.
Benoit
Apr 20, 2020, 5:56:18 PM4/20/20
to Metamath
Thanks to everyone for your remarks. I'll add a few links to the two provided by Alexander (repeated as the first two below):
and for the unicodes: https://www.unicode.org/charts/PDF/U2190.pdf
Some remarks:
* The links above mention regular mono/epimorphisms. In the category of sets, all mono/epimorphisms are regular and are exactly the injective/surjective functions, so there is no ambiguity.
* It is true that \hookrightarrow is more frequent than \rightarrowtail to denote injections, but the latter is sometimes restricted to denote only inclusion maps, hence my choice for the latter, since non-ambiguity is most important.
* As for understandability, the symbol ( A >--> B ) suggests that the extra constraint (compared to A --> B ) is on the side of the domain (injectivity) while ( A -->> B ) suggests that the extra constraint is on the side of the target (surjectivity), and ( A >-->> B ) adds both constraints (bijectivity).
* Mario's example of F : A --> ( C ^m B ) versus F : A --> ( B -Set-> C ) or F e. ( A -Set-> ( B -Set-> C ) ) when F is a set, is a good one. It is also illustrated in http://us2.metamath.org/mpeuni/df-bj-unc.html : the domain of uncurry_{x,y,z} is the set ( x -Set-> ( y -Set-> z ) ).
> df-map is a different topic, it should not be mixed with homomorphisms.
This will be difficult, given that functions are morphisms of sets.
My main concerns are non-ambiguity and consistency of notation, which generally help understandability. In any case, I won't make any changes soon nor without Norm's green light.
Benoît
Reply all
Reply to author
Forward
0 new messages