## Stream: new members

### Topic: Semialgebra

#### Nicolò Cavalleri (Jul 12 2020 at 10:49):

Since in mathlib a module over a semiring is called a semimodule why there is not both concept of algebra and semialgebra? I mean maybe not to confuse it with a semialgebra of sets but if it is just a naming problem I guess it can be solved easily

#### Kevin Buzzard (Jul 12 2020 at 10:56):

because it's the computer scientists who like all this semring stuff, and they are not sufficiently into algebra to have bothered to build all this semi-theory as far as the mathematicians who want to do Galois theory and algebraic number theory etc and who don't really care about semirings and just need rings. I'm sure that PRs making all these new structures would be seriously considered.

#### Kevin Buzzard (Jul 12 2020 at 10:56):

There didn't used to be semimodules, there was just modules, and then someone spotted that there was an exciting generalisation and someone else bothered to do it.

#### Kevin Buzzard (Jul 12 2020 at 10:57):

The definition of a UFD makes sense for semirings, but Lean demands an integral domain because the person who wrote it didn't care.

#### Kevin Buzzard (Jul 12 2020 at 10:58):

In fact the definition of UFD makes sense for commutative cancellative monoids with 0, if you care. But the library grows organically.

#### Patrick Massot (Jul 12 2020 at 10:59):

Kevin, you should stop writing things like this. We are very grateful to have many lemmas about natural numbers. Semi-rings are not exotic, you use one since you were 2 years old.

#### Patrick Massot (Jul 12 2020 at 11:00):

And who knows whether you'll end wanting to talk about $\mathbb{N}[X]$ for instance?

#### Kevin Buzzard (Jul 12 2020 at 11:00):

@Yury G. Kudryashov has been an amazing proponent of making stuff work in the right generality, he tirelessly refactors -- and others too.

#### Kevin Buzzard (Jul 12 2020 at 11:01):

Yes Patrick, you are absolutely right. 99% of use cases have the "normal mathematical" assumptions, and then all of a sudden you run into a situation where the slight extra generality is really helpful, and then you curse the library for having it all set up in the way the maths books are set up.

#### Kevin Buzzard (Jul 12 2020 at 11:02):

The first time I saw this was when someone defined a group acting on a set, and then Mario said "but there are no inverses mentioned in the axioms -- make it a monoid acting on a set". If you catch it early you can get it "right" from the start, but the more you leave it, the harder it is to change.

#### Sebastien Gouezel (Jul 12 2020 at 11:46):

In the measure theory refactor, Yury notes that there is an ennreal-semimodule structure on the space of measures, and uses it to deduce several facts for free.

#### Nicolò Cavalleri (Jul 12 2020 at 17:39):

So does everybody agree that what is now an algebra should be called a semialgebra and introduce the name algebra for what mathematicians actually call an algebra, so that the names are coherent with rings, semirings modules and semimodules? I am asking all of this because I am introducing topological algebras and smooth algebras and need names for what is actually an algebra and not a semialgebra otherwise everything becomes a mess

#### Reid Barton (Jul 12 2020 at 17:41):

Aren't algebras and semialgebras the same thing?

#### Reid Barton (Jul 12 2020 at 17:41):

Maybe the problem is with semimodule

#### Reid Barton (Jul 12 2020 at 17:41):

i.e. semimodule should just be called module

#### Reid Barton (Jul 12 2020 at 17:45):

It's entirely possible that I am missing something bad that would happen if we just renamed semimodule -> module and removed module

#### Nicolò Cavalleri (Jul 12 2020 at 17:48):

I do not understand what you mean by saying they are the same thing! I though something like a commutative monoid was a semimodule on $\mathbb{N}$ that does not have a module structure. What am I missing?

#### Reid Barton (Jul 12 2020 at 17:49):

(The general categorical framework is that you have a symmetric monoidal category $(V, \otimes, 1)$, the relevant examples being commutative monoids/abelian groups; a (commutative) semiring/ring $R$ is a (commutative) monoid object in $V$; an $R$-module is a module object over $R$ in $V$; if $R$ is commutative and $V$ is a reasonable category then $R$-modules again form a symmetric monoidal category; an $R$-algebra is a monoid object in $R\mathrm{Mod}$. For semiring/ring the distinction is important because you need to know which $V$ you are talking about, but once you give a semiring/ring $R$ then $V$ is determined, so you don't need to repeat yourself in (semi)module and (semi)algebra.)

#### Reid Barton (Jul 12 2020 at 17:51):

Well, I guess it could still happen that a semimodule over a ring viewed as a semiring is different from a module over that ring, but in fact that doesn't happen here.

#### Reid Barton (Jul 12 2020 at 17:53):

The reason being that negation on the module is determined by the semimodule structure, it's multiplication by -1 : R.

#### Nicolò Cavalleri (Jul 12 2020 at 17:54):

Oh ok I see this but what if I want to define a topological algebra to be something for which addition, negation and multiplication are continuous (and multiplication by a scalar). If I only have the name semialgebra I cannot talk about negation and if I do what other name should I give to it if not a topological algebra?

#### Nicolò Cavalleri (Jul 12 2020 at 17:54):

Actually I get it for free with multiplication by -1 again I guess

#### Nicolò Cavalleri (Jul 12 2020 at 17:55):

Then never mind it's just that I did not ever use these things before

#### Reid Barton (Jul 12 2020 at 17:59):

I guess I was arguing two separate things before. It's "morally correct" to refer to a semimodule structure over a semiring as a module structure. And, when there could be ambiguity (a semimodule structure over a ring), the ambiguity doesn't matter.

#### Reid Barton (Jul 12 2020 at 17:59):

Of course things that don't matter in ordinary math sometimes matter in formalization, but looking at the definition of module it looks like it will in fact not matter in Lean either.

#### Nicolò Cavalleri (Jul 12 2020 at 18:11):

I am not really sure what the best thing to do is, if to remove module or keep useless names just because they are more familiar to normal mathematicians who might not need to deal with the greatest generalizations, and I am clearly not the right person to discuss these decisions, but I just think it would be cool to have more uniformity and have the same conventions for modules and algebras because otherwise things are pretty hard to name afterwards and they get quite confusing for someone like me who just began looking into mathlib

#### Scott Morrison (Jul 12 2020 at 23:19):

I think it would be good for someone to try deleting module and renaming semimodule to module! I hope it works.

Last updated: May 06 2021 at 22:13 UTC