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.
On Sun, Apr 19, 2020 at 2:00 AM 'Alexander van der Vekens' via Metamath < [email protected]> wrote: > 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 > <https://groups.google.com/d/msgid/metamath/5788f3d9-5468-4e76-a2bb-84f69253e880%40googlegroups.com?utm_medium=email&utm_source=footer> > . > -- 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/CAFXXJSvkTBPH6SAbx5CQ69GOTiZzZ5jS41mJYT8GPo1KuE65JQ%40mail.gmail.com.
