subfields are not fields

Stream: mathlib4

[Kevin Buzzard]

I'm very surprised to notice that apparently docs#Subfield s are not fields because they might not be commutative. I know that in French people use "corps" and this word is often translated as "field" even though commutativity is not assumed, but in English a field is surely always commutative, and the fact that this isn't assumed is not even mentioned in the docstring. Are people happy with this convention? At the very least I'd like to mention this in the docstring but my preference would be to change this to SubdivisionRing or something (i.e. stick with the literature rather than going our own way).

[Damiano Testa]

I would be in favour of renaming to SubdivisionRing, since a Subfield not being a Field seems very strange.

[Kevin Buzzard]

It is mentioned in the module docstring at least, but not in the docstring of Subfield.

[Damiano Testa]

It would be great if Lean could give you a warning once, every time you introduce a new variable with stuff like this. E.g. you type (F : Subfield K) and Lean tells you "Remember, a subfield is not necessarily commutative." And then shuts up when you keep typing stuff.

[Kevin Buzzard]

Of course we're going to run into the VectorSpace issue here, which might now be solvable in Lean 3. For younger viewers: we had VectorSpace at some point to be a synonym for Module when the base ring was a field, but it caused problems in Lean 3 and we eventually gave up. Here we'll have subdivisionrings of a division ring and then all over Galois theory we'll either have subdivisionrings of fields or we'll have to duplicate API or we'll have to have the thing which the computer scientists hate, namely subfield just meaning the same thing as subdivisionring

[Damiano Testa]

Kevin Buzzard said:

It is mentioned in the module docstring at least, but not in the docstring of Subfield.

I am still more in favour of a rename, than writing a warning in the doc-string.

[Edward van de Meent]

Kevin Buzzard said:

Here we'll have subdivisionrings of a division ring and then all over Galois theory we'll either have subdivisionrings of fields or we'll have to duplicate API or we'll have to have the thing which the computer scientists hate, namely subfield just meaning the same thing as subdivisionring

is there a reason not to have Subfield assuming commutativity (while also having SubdivisionRing)?

[Yury G. Kudryashov]

Duplicating API?

[Edward van de Meent]

we can add a coersion, right?

[Edward van de Meent]

i think that should prevent most duplication

[Yury G. Kudryashov]

No, if we have 2 types, then we need to duplicate CompleteLattice instance, map/comap etc.

[Edward van de Meent]

ah right

[Edward van de Meent]

still, you can't really get around that, as they're separate concepts...

[Edward van de Meent]

how should one spell "commutative subdivisionring", if we don't add a proper type like Subfield?

[Yury G. Kudryashov]

They're just subdivisionrings of fields.

[Edward van de Meent]

can't a subdivisionring of a divisionring be commutative?

[Yury G. Kudryashov]

It can, but they don't form a CompleteLattice.

[Edward van de Meent]

i don't think "forming a CompleteLattice" is the criterion we should use to decide if a definition is useful...

[Yury G. Kudryashov]

We can talk about (S : SubDivisionRing K) [@Std.Commutative S fun a b => a * b]

[Kevin Buzzard]

Yury G. Kudryashov said:

They're just subdivisionrings of fields.

In the actual issue which prompted this question, I have students who want to talk about subfields (assumed commutative) of a division ring (genuinely not commutative). This is a really common concept in the theory of finite-dimensional central simple algebras; they can be understood by understanding maximal commutative subalgebras (which are subfields) and then bootstrapping up from there.

[Yury G. Kudryashov]

What about (S : SubDivisionRing K) [@Std.Commutative ..]?

[Kevin Buzzard]

I guess that would work! Note that subfields of a division ring are far from being a lattice, e.g. there are plenty of subfields of $M_2(\mathbb{R})$ which are isomorphic to $\mathbb{C}$, so there's no sup, no top etc.

[Yury G. Kudryashov]

Of course, another option is to create a structure that extends SubDivisionRing and assumes commutativity, with a SemilatticeInf instance.

[Yury G. Kudryashov]

The comm field can have a default value := by intros; apply mul_comm, and we can have an equivalence between SubDivisionRing and Subfield (+CompleteLattice instance) in case of a field.

[Eric Wieser]

This presumably also is relevant for commutative subrings of a noncommutative ring etc

[Eric Wieser]

Don't we have docs#Subgroup.IsCommutative for pretty much an analogous case?