definition of `IsSeparable` seems wrong for general rings

Stream: maths

[Jz Pan]

Currently IsSeparable F K is defined to be every element x of K is integral over F and has separable minimal polynomial. While this is the commonly used definition for separable field extensions, it's not true for rings if we use this definition https://en.wikipedia.org/wiki/Separable_algebra, which is defined as the multiplication map $K\otimes_F K\to K$ has a section. For example, under this definition $\mathbb{Q}$ is a separable $\mathbb{Z}$ algebra, but which is not integral over $\mathbb{Z}$.

In the documentation of IsSeparable there is a line of text:

We define this for general (commutative) rings and only assume F and K are fields if this is needed for a proof.

Maybe we should add another line of text state that this definition is not quite correct for general rings?

[Jz Pan]

PS: I think the current IsSeparable is more close to étale algebra https://en.wikipedia.org/wiki/%C3%89tale_morphism which for field case is also equivalent to finite separable extension.

[Kevin Buzzard]

My instinct is that what's going on here is that people are just observing "oh look the definition for separability of fields (which we need for Galois theory) typechecks if we drop the field hypothesis" rather than asking the more complex question of whether it's the right definition in that generality. On the other hand the link you give is really I think more of a thing in noncommutative ring theory. Do we have commutativity assumptions in docs#IsSeparable ?

[Kevin Buzzard]

So the bottom ring is commutative, which is not ideal for the Separable algebra Wikipedia page. I think it would be very cool to have definition of an etale morphism of rings and then refactor separability to just mean etale :-)

[Adam Topaz]

Our notion of algebra always assumes some commutativity

[Jz Pan]

Apart from commutativity problem (which I usually ignored), an important question is that: should $\mathbb{Q}$ be a separable $\mathbb{Z}$-algebra?

[Adam Topaz]

Yes?

[Adam Topaz]

But I live in the étale world, so maybe I’m biased

[Kevin Buzzard]

I think that if this question is at all ambiguous then we should just restrict to field extensions rather than making up notation and possibly making things worse. I would like mathlib to become some kind of authority about the actual meaning of words (for example nat has zero, compact doesn't imply Hausdorff) and surely 99% of the uses of the term in the literature will be in the case of fields.

[Antoine Chambert-Loir]

I partially agree: a definition should request the minimal amount of assumption it needs to make sense to the compiler, because that allows other people to use it in a more general framework if they need it.
On the other hand, the mathlib code should precise that the “classical definition” (with a reference to standard math litterature) generally makes more specific assumption and write them down, so that people are not confused.

[Anne Baanen]

I'm the one to blame for generalizing IsSeparable to all rings. It was a workaround for some timeouts back in the Lean 3 days, so I have no objection to restrict this back to fields if that's technically possible. However, it would be even better to use the general definition of separable algebra, and then prove this is equivalent in the case of fields.