Semialgebra

Stream: new members

[Nicolò Cavalleri]

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]

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]

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]

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]

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

[Patrick Massot]

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]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

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]

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]

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]

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]

Aren't algebras and semialgebras the same thing?

[Reid Barton]

Maybe the problem is with semimodule

[Reid Barton]

i.e. semimodule should just be called module

[Reid Barton]

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

[Nicolò Cavalleri]

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]

(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]

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]

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

[Nicolò Cavalleri]

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]

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

[Nicolò Cavalleri]

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

[Reid Barton]

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]

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]

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]

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