## Stream: maths

### Topic: Basic lemmas/instances about subfields

#### Thomas Browning (Aug 20 2020 at 03:09):

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 (Aug 20 2020 at 03:17):

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 (Aug 20 2020 at 03:19):

@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 (Aug 20 2020 at 07:08):

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

#### Patrick Lutz (Aug 20 2020 at 17:10):

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 (Aug 20 2020 at 17:18):

@Patrick Lutz Aha, that's good

#### Johan Commelin (Aug 20 2020 at 17:19):

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

#### Johan Commelin (Aug 20 2020 at 17:25):

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

#### Adam Topaz (Aug 20 2020 at 17:35):

Johan Commelin said:

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

What? Why?

#### Adam Topaz (Aug 20 2020 at 17:36):

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 (Aug 20 2020 at 17:37):

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

#### Johan Commelin (Aug 20 2020 at 17:42):

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

#### Johan Commelin (Aug 20 2020 at 17:43):

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 (Aug 20 2020 at 17:55):

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 (Aug 20 2020 at 17:57):

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

#### Patrick Massot (Aug 20 2020 at 18:16):

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 (Aug 20 2020 at 18:18):

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 (Aug 20 2020 at 18:22):

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

#### Thomas Browning (Aug 21 2020 at 16:09):

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

Last updated: May 06 2021 at 18:20 UTC