On Friday, January 31, 2020 at 8:19:00 PM UTC-5, Jim Kingdon wrote: > > > > On January 31, 2020 3:39:46 PM PST, Norman Megill wrote: > > >I would like to hear other opinions on whether "magma" and "semigroup" > >should become part of the main set.mm body. > > I don't have a strong opinion one way or the other. I suspect Norm is > right that these are a whole lot more obscure than groups and rings and > fields and the other usual suspects. On the other hand, I guess things are > arranged so that a proof about groups doesn't really need to know about > magmas and semigroups?
Yes, it is simple to arrange it so that groups don't have to know about magmas and semigroups: we can just leave the group definition and proofs alone, since they don't depend on them now. > That might point us to a "harmless even if not strictly necessary" stance. > If we leave groups alone, then importing magma and semigroup will be "harmless" in principle. However, logically they would belong before groups are introduced. This means that it is likely that proof of the group associative law will start to borrow from the same theorem about semigroups in order to shorten the proof (as we always do with layered structures). This in principle is also harmless. What I fear happening is that we've introduced unnecessary additional complexity for anyone just wanting to learn about groups (such as an engineer). What was a straightforward definition turns into a tower of associated structures they've never heard of (monoid, semigroup, magma) and don't care about, but are forced to learn. Will they give up and go elsewhere (e.g. an undergraduate book on group theory that simply starts with groups at the beginning)? Even monoids are apparently a graduate-level topic based on Lang's books. We could put semigroups and monoids after df-grp to prevent "contamination", but that is also weird and somewhat contrary to the set.mm philosophy. In their pure form, magmas and semigroups have no serious applications. Most semigroup applications (in e.g. FL's search) concern semigroups with additional properties, not pure semigroups. When we start to have those kinds of applications, we can revisit this and see if it makes sense to share the common pure semigroup base they're built on. But we don't have such applications now. Norm -- 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/06289310-2f14-4e6f-96a6-aadec4716afe%40googlegroups.com.
