Zulip Chat Archive

Stream: maths

Topic: Basic lemmas/instances about subfields


view this post on Zulip 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?)

view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Johan Commelin (Aug 20 2020 at 17:18):

@Patrick Lutz Aha, that's good

view this post on Zulip 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

view this post on Zulip Johan Commelin (Aug 20 2020 at 17:25):

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

view this post on Zulip 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?

view this post on Zulip 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 KK in a non-algebraic extension LL?

view this post on Zulip Adam Topaz (Aug 20 2020 at 17:37):

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

view this post on Zulip Johan Commelin (Aug 20 2020 at 17:42):

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

view this post on Zulip 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.

view this post on Zulip 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 KK in LL is subalgebra of LL which is the integral closure of KK, and in the second example, you again would just need complete subalgebras. But it would be nice, for example, to do the following: if LKL|K is an arbitrary extension and SLS \subset L, we should be able to take, for example, the relative algebraic closure of k(S)k(S) in LL, as an intermediate subfield between LL and KK. Such things pop up all the time in algebraic geometry.

view this post on Zulip 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.

view this post on Zulip 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...

view this post on Zulip 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.

view this post on Zulip Adam Topaz (Aug 20 2020 at 18:22):

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

view this post on Zulip 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