Basic lemmas/instances about subfields

Stream: maths

[Thomas Browning]

We have a few lemmas/instances at https://github.com/pglutz/galois_theory/blob/master/src/subfield_stuff.lean which relate field extensions (in terms of [algebra F E]) with the image as a subfield (set.range (algebra_map F E)). These are used in our proof of the primitive element theorem. Do these have a home somewhere in mathlib? (i.e., should we PR them to mathlib and if so, where?)

[Johan Commelin]

My gut feeling is that you want to define a type intermediate_field F E that extends subalgebra and subfield (once that one is bundled). @Kenny Lau do you have ideas for the design here?

[Johan Commelin]

@Thomas Browning This stuff should certainly end up in mathlib in some form. Probably in algebra.(sub)field or field_theory.subfield.
But to determine which form it should be in, I think it's better to see that these definitions can be used in an elegant and efficient way to prove some things. There might be a mathematically equivalent but Lean-different way of setting things up that works better. And you only know this once you've started using it.

[Kenny Lau]

That isn't necessary, as every subring of F that contains E is a field as long as F/E is algebraic

[Patrick Lutz]

Johan Commelin said:

Thomas Browning This stuff should certainly end up in mathlib in some form. Probably in algebra.(sub)field or field_theory.subfield.
But to determine which form it should be in, I think it's better to see that these definitions can be used in an elegant and efficient way to prove some things. There might be a mathematically equivalent but Lean-different way of setting things up that works better. And you only know this once you've started using it.

We used them in our proof of the primitive element theorem.

[Johan Commelin]

@Patrick Lutz Aha, that's good

[Johan Commelin]

@Kenny Lau That's a good point. And we're only interested in F/E algebraic anyways

[Johan Commelin]

@Patrick Lutz Do you think it makes sense to prove stuff about subalgebra F E instead?

[Adam Topaz]

Johan Commelin said:

Kenny Lau That's a good point. And we're only interested in F/E algebraic anyways

What? Why?

[Adam Topaz]

I understand that this work is mainly building up towards Galois theory, but what if, for example, I want to take the relative algebraic closure of a field $K$ in a non-algebraic extension $L$?

[Adam Topaz]

Or what if I want to do Galois theory for complete subextensions of $\mathbb{C}_p$ over $\mathbb{Q}_p$?

[Johan Commelin]

Certainly in the latter case you need a completely new bundled type, right?

[Johan Commelin]

But, you have a fair point, that outside of the immediate interest of Galois theory, there are probably good examples of subfields where we really want to know it's a bundled subfield.

[Adam Topaz]

Actually, both of these examples are not really relevant. In the first example, the relative algebraic closure of $K$ in $L$ is subalgebra of $L$ which is the integral closure of $K$, and in the second example, you again would just need complete subalgebras. But it would be nice, for example, to do the following: if $L|K$ is an arbitrary extension and $S \subset L$, we should be able to take, for example, the relative algebraic closure of $k(S)$ in $L$, as an intermediate subfield between $L$ and $K$. Such things pop up all the time in algebraic geometry.

[Adam Topaz]

And eventually if you want to do, say, differential Galois theory, then you would need to move away from just algebraic extensions.

[Patrick Massot]

Are you arguing to figure out whether transcendental extensions exist? I don't whether this is worse than the debate about existence of non-commutative rings...

[Adam Topaz]

I'm mainly saying that I agree with @Johan Commelin 's first suggestion of defining intermediate_field as extending subalgebra, and doing Galois theory with such a bundled type.

[Adam Topaz]

I think this approach would also be helpful for eventually defining transcendence bases of fields.

[Thomas Browning]

so should we go ahead and refactor our code in terms of intermediate_field?