# Zulip Chat Archive

## Stream: maths

### Topic: Isomorphism of Field Extensions

#### Thomas Browning (Nov 02 2020 at 21:32):

We've been working on Galois theory, and it would be nice to have a notion of isomorphic field extensions. If `E/F`

is a field extension (i.e., `[field F] [field E] [algebra F E]`

) and if `E'/F'`

is another field extension, then an isomorphism of field extensions might consist of two ring isomorphisms `a : E → E'`

and `b : F → F'`

such that `a(f • e) = b(f) • a(e)`

. Is this a reasonable definition to make, and if so, where should it go in mathlib?

If this does end up in mathlib, then the next thing to do would be to prove that various things are preserved by it (i.e., integral elements, minimal polynomials, separable extensions, normal extensions, galois extensions, dimension, findim, etc...)

#### Thomas Browning (Nov 02 2020 at 21:33):

also, it might not be necessary for the definition to require F and E to be fields

#### Thomas Browning (Nov 02 2020 at 21:36):

the reason why we want such a definition is that the usual notion of an algebra isomorphism doesn't work when the base field changes. For example, if you know something about the extension E/(bot : intermediate_field F E) and want to conclude the same thing about E/F

#### Kevin Buzzard (Nov 02 2020 at 21:43):

Could one split this into two simpler "transport" problems -- if you have `algebra F E`

and an F-algebra F' then by tensoring you get `algebra F' (E \otimes_F F')`

, and if F' is isomorphic to F you can port stuff along that construction. And then you can restrict to a constant base and talk about F-algebra isomorphisms E -> E' and transport stuff along that. Maybe it's easier to approach in two steps like that? Not sure though.

#### Adam Topaz (Nov 02 2020 at 21:44):

There was some discussion about semilinear algebra recently. Whatever happened with that? This could be an extension of that.

#### Patrick Lutz (Nov 02 2020 at 21:49):

Kevin Buzzard said:

Could one split this into two simpler "transport" problems -- if you have

`algebra F E`

and an F-algebra F' then by tensoring you get`algebra F' (E \otimes_F F')`

, and if F' is isomorphic to F you can port stuff along that construction. And then you can restrict to a constant base and talk about F-algebra isomorphisms E -> E' and transport stuff along that. Maybe it's easier to approach in two steps like that? Not sure though.

What if you don't automatically know that `F'`

is an `F`

-algebra?

#### Thomas Browning (Nov 02 2020 at 21:51):

for example, F and F'=(bot : intermediate_field F E). F' is an F-algebra, but thinking of F as an F'-algebra is a little weird.

#### Patrick Lutz (Nov 02 2020 at 21:52):

Actually, it is true that so far we only need to change either `F`

or `E`

and not both at once. But I think there are two advantages to formalizing a transformation of field extensions `F/E -> F'/E'`

. First, it is possible that at some point we will need to change both the base field and the extension for isomorphic copies at the same time; you could imagine needing to know that `top/bot`

(as intermediate fields of `E/F`

) is the same as `E/F`

or something. Second, when proving that things like separability or normality are preserved by isomorphism, it seems simpler to prove it a single time for this more general notion of isomorphism than to prove it both for isomorphism of the base field and isomorphism of the extension

#### Kevin Buzzard (Nov 02 2020 at 21:53):

But you could make the `equiv`

surely? And then push along some noncomputable map or whatever, but the theorems won't care about computability.

#### Kevin Buzzard (Nov 02 2020 at 21:54):

One argument for biting the bullet and changing both at once is that one could imagine later on wanting to replace a short exact sequence $0\to A\to B\to C\to 0$ by an isomorphic one $0\to A' \to B' \to C' \to 0$ and here it seems tricky to change them one at a time.

#### Patrick Lutz (Nov 02 2020 at 21:54):

Kevin Buzzard said:

But you could make the

`equiv`

surely? And then push along some noncomputable map or whatever, but the theorems won't care about computability.

Are you replying to Thomas here? I think it's true that this would work for the specific case of `E/bot`

being isomorphic to `E/F`

. But in more general situations it might be annoying

#### Patrick Lutz (Nov 02 2020 at 21:54):

Actually, why isn't there already a notion of changing the base ring of an algebra? This doesn't seem super specific to fields

#### Kevin Buzzard (Nov 02 2020 at 21:55):

Changing the base ring of an algebra will surely be done using tensor product, right?

#### Kevin Buzzard (Nov 02 2020 at 21:55):

Well, I guess it depends on how you're changing it :-)

#### Patrick Lutz (Nov 02 2020 at 21:56):

Kevin Buzzard said:

Changing the base ring of an algebra will surely be done using tensor product, right?

Yeah, I guess so. I guess in the case of fields it's easier because you can only have isomorphism or embeddings

#### Kevin Buzzard (Nov 02 2020 at 21:56):

Aah. How about this? There should be some way of switching between `algebra F E`

and `F : subring E`

. You have the same E, so perhaps for your use case you want to think about subrings of E rather than extensions of F

#### Patrick Lutz (Nov 02 2020 at 21:57):

I guess in our case we actually only care about things isomorphic to `F`

#### Kevin Buzzard (Nov 02 2020 at 21:57):

in your case you'll be able to prove they're the same subring

#### Kevin Buzzard (Nov 02 2020 at 22:01):

You're running into a similar sort of issue which we ran into when doing the Artin-Tate Lemma in commutative algebra. We have this mental model where everything is easy, but when you translate it down into type theory it is suddenly more complicated than you want it to be. "Consider three rings $A\subseteq B\subseteq C$ becomes this nightmare of `A : subring B`

, `A : subring C`

, `B : subring C`

, `algebra A B`

, `algebra A C`

and `algebra B C`

, six different ideas which are all compatible in some way which becomes completely transparent from the set-theoretic perspective. After months of haitus, Kenny Lau came up with `is_scalar_tower`

which seems to work (it works for the Artin-Tate Lemma at least). Does it help you? You could get a tower from F to bot to E.

#### Thomas Browning (Nov 02 2020 at 22:04):

We've used is_scalar_tower a bit. For instance, with separable extensions we proved lemmas that the top and bottom of an is_scalar_tower are also separable. With normal however, you don't in general know that the bottom of an is_scalar_tower is also normal.

#### Thomas Browning (Nov 02 2020 at 22:05):

so in the example of showing that (E/bot is normal) iff (E/F is normal), I don't think that is_scalar_tower helps

#### Kevin Buzzard (Nov 02 2020 at 22:05):

This is a good test question!

#### Kevin Buzzard (Nov 02 2020 at 22:07):

E/F normal implies E/bot normal shouldn't be too hard. But the other way is interesting.

#### Kevin Buzzard (Nov 02 2020 at 22:10):

Oh but there are bundled subfields. Doesn't this help a lot in your use case? You should be able to prove that the subfields F and bot of E are equal, and then hopefully pass normal between them.

#### Thomas Browning (Nov 02 2020 at 22:11):

F isn't a subfield of E though

#### Thomas Browning (Nov 02 2020 at 22:11):

F is just a field, and E is just a field which happens to be an F-algebra

#### Kevin Buzzard (Nov 02 2020 at 22:11):

Right, but E is an F-algebra so presumably there's a construction which makes a subfield

#### Thomas Browning (Nov 02 2020 at 22:12):

that would be (bot : intermediate_field)

#### Thomas Browning (Nov 02 2020 at 22:12):

at least, that's what we've been using to turn F into a subfield of E

#### Kevin Buzzard (Nov 02 2020 at 22:13):

I don't know what `intermediate_field`

is. I'm talking about making a term of type `subfield E`

from `algebra F E`

. This shouldn't be too hard.

#### Kevin Buzzard (Nov 02 2020 at 22:13):

(and might be there already)

#### Thomas Browning (Nov 02 2020 at 22:15):

One option is to put a field structure on `set.range (algebra_map F E)`

(this is what we did a while ago, but it's painful). Now I would use `(bot : intermediate_field F E).to_subfield`

#### Kevin Buzzard (Nov 02 2020 at 22:16):

and I'm suggesting that one could prove that this is the subfield which one could build directly as the image of the algebra map $F\to E$.

#### Kevin Buzzard (Nov 02 2020 at 22:16):

(without using intermediate_field)

#### Kevin Buzzard (Nov 02 2020 at 22:17):

So what does your `normal`

predicate eat right now?

#### Thomas Browning (Nov 02 2020 at 22:17):

`[field F] [field E] [algebra F E]`

#### Thomas Browning (Nov 02 2020 at 22:18):

(that's what the field_theory folder uses for field extensions)

#### Thomas Browning (Nov 02 2020 at 22:19):

Kevin Buzzard said:

and I'm suggesting that one could prove that this is the subfield which one could build directly as the image of the algebra map $F\to E$.

You still have to do the hard work of transporting normality (for instance) across the algebra map from F to its image in E

#### Kevin Buzzard (Nov 02 2020 at 22:19):

So now we could define a second `normal'`

predicate on `subfield E`

, by saying that if `A : subfield E`

then `normal' A`

is true iff the corresponding `algebra \u A E`

was normal

#### Kevin Buzzard (Nov 02 2020 at 22:20):

I see, and then the issue is that you start with F then make the subfield and then make a new type and it's perhaps not equal to F

#### Thomas Browning (Nov 02 2020 at 22:20):

yes

#### Kevin Buzzard (Nov 02 2020 at 22:22):

you start with some abstract type F equipped with a map to E and end up with a subtype of E corresponding to the image of the map. And set theorists can't tell the difference.

#### Kevin Buzzard (Nov 02 2020 at 22:25):

So one needs to somehow push the entire problem over to `subfield E`

. I want to argue that `algebra F E`

is normal iff `F' : subfield E`

is `normal'`

iff `algebra \u bot E`

is normal. This is what you have to do to talk about E/bot being normal, right? You have to promote bot to some type (a subtype) and make E a bot-algebra? Is this what you mean when you talk about E/bot being normal?

#### Thomas Browning (Nov 02 2020 at 22:27):

yeah, when I say `normal bot E`

, there's secretly an algebra structure `algebra bot E`

#### Kevin Buzzard (Nov 02 2020 at 22:27):

(and bot is being promoted from a term to a type)

#### Thomas Browning (Nov 02 2020 at 22:27):

in general, if `K : intermediate_field F E`

then there is an algebra structure `algebra F K`

and `algebra K E`

#### Kevin Buzzard (Nov 02 2020 at 22:28):

What's the definition of normal?

#### Kevin Buzzard (Nov 02 2020 at 22:29):

It seems to me that this could be made to work if you knew normal iff splitting field, which presumably you guys did a while ago

#### Thomas Browning (Nov 02 2020 at 22:31):

something about minimal_polynomials, I think. But the point isn't to prove this specific thing about normality being preserved. There are also other cases where we want to transport some property along isomorphic field extensions, which is why I was thinking that some more general framework would be helpful.

#### Kevin Buzzard (Nov 02 2020 at 22:32):

I want to define K : subfield E to be `normal'`

iff `algebra \uK E`

is normal. Now one wants to prove that if algebra F E then this is normal iff the corresponding "F" : subfield E is normal, and one could do this by checking that the "same" polynomials worked.

#### Kevin Buzzard (Nov 02 2020 at 22:33):

Making some new structure saying that E/F and E'/F' are isomorphic isn't going to solve any problems though, right? You'll still have to go through the proof I'm outlining above (or find another one)

#### Kevin Buzzard (Nov 02 2020 at 22:33):

because you can't just pass mathematical predicates along isomorphisms.

#### Thomas Browning (Nov 02 2020 at 22:33):

yes, we'll have to do basically that proof

#### Thomas Browning (Nov 02 2020 at 22:33):

but it's a question of how to state it

#### Kevin Buzzard (Nov 02 2020 at 22:33):

I see

#### Patrick Lutz (Nov 02 2020 at 22:34):

it seems nicer to have a general statement that certain properties are preserved by isomorphism and then to prove that various isomorphisms exist than to prove for each instance that we care about that those properties are preserved

#### Patrick Lutz (Nov 02 2020 at 22:34):

even if right now we don't really need the greater generality

#### Kevin Buzzard (Nov 02 2020 at 22:35):

but what I'm suggesting is that if one makes a new structure which captures the idea of "F/E and F'/E' are isomorphic" then that structure itself doesn't solve any problems, in fact in some sense it opens up a big class of problems each of which needs to be solved individually.

#### Kevin Buzzard (Nov 02 2020 at 22:36):

you'll have to prove that for each instance you care about the properties are preserved anyway

#### Kevin Buzzard (Nov 02 2020 at 22:36):

and the proof that normality is preserved is going to be harder in this setting because you'll have to control the top field as well as the bottom one

#### Thomas Browning (Nov 02 2020 at 22:38):

That's true, but it seems better to me to have this work all done in one place (for each property that is preserved). Get it over and done with.

#### Mario Carneiro (Nov 02 2020 at 22:40):

I agree with kevin that two isomorphisms are harder than one

#### Mario Carneiro (Nov 02 2020 at 22:41):

what applications would this be put to?

#### Thomas Browning (Nov 02 2020 at 22:42):

right now, the main thing is transporting various properties between E/F and E/(bot : intermediate_field) and (top : intermediate_field)/F

#### Kevin Buzzard (Nov 02 2020 at 22:42):

@Mario Carneiro you were saying the other day that this transfer/transport/whatever it's called tactic has never really been a well-defined problem. But instances do pop up. Here is one. If we have ring homomorphisms $a:F\to E$ and $a':F' \to E'$ which are isomorphic in the sense that there are isomorphisms $F\to F'$ and $E\to E'$ making the square commute, then there are a ton of mathematical predicates which one can put on ring homomorphisms (being finite type, module finite, integral, etc) and with extra assumptions (e.g. everything is a field) then there are even more (being normal, separable, Galois...). At the minute, transferring every predicate across involves some pain, and there are a fair few predicates that show up in Galois theory.

#### Kevin Buzzard (Nov 02 2020 at 22:43):

But one also has to think carefully about whether if there was some way of passing mathematical predicates along isomorphisms, whether it would actually solve the problem at hend.

#### Mario Carneiro (Nov 02 2020 at 22:43):

I agree that all of these theorems should exist, but I don't think they will be used particularly often

#### Mario Carneiro (Nov 02 2020 at 22:44):

We have ring equivs, we have noetherian rings, therefore we should have the theorem that says they cohere

#### Patrick Lutz (Nov 02 2020 at 22:45):

Actually, this sort of thing about properties that "obviously" carry across isomorphisms seems to come up all the time in formalization and be a big pain. Why can't this be automated? There is already a decent mathematical way to capture many instances of this: first order definable properties of models in a language transfer across isomorphisms of models in that language. Why can't proof assistants do this automatically? Like if I define a new type of structure I should automatically get the right notion of isomorphism and any property stated in a first order way should automatically transfer over isomorphisms

#### Mario Carneiro (Nov 02 2020 at 22:45):

It can't be automated until it is done manually

#### Patrick Lutz (Nov 02 2020 at 22:46):

I'm not totally sure what you mean. I agree that right now Lean does not even have the infrastructure to do this sort of thing, but why not?

#### Mario Carneiro (Nov 02 2020 at 22:47):

It has plenty of infrastructure to support this in principle. The problem is that we don't know what the result should actually be

#### Mario Carneiro (Nov 02 2020 at 22:47):

so it needs to first be done by hand enough times to make the pattern clear

#### Patrick Lutz (Nov 02 2020 at 22:48):

I see what you mean now

#### Mario Carneiro (Nov 02 2020 at 22:48):

I have heard people argue for this for a long time but no one is putting in the legwork to write out isomorphism theorems manually

#### Patrick Lutz (Nov 02 2020 at 22:49):

I guess the basic model theory result seems like it captures many instances of this pattern but not all, and I'm not sure how it should be actually implemented in a usable way in a proof assistant

#### Mario Carneiro (Nov 02 2020 at 22:49):

in any case, the proofs are all fairly simple, we may find out that it's not even worth the work of automating because the theorems themselves are all that we needed

#### Kevin Lacker (Nov 02 2020 at 22:53):

i've been looking for good target problems to try out `rewrite_search`

or similar automatic tactics on and i'm curious what people would want automation to do here - is there some set of theorems that you would like to write out the statements and then have the automation automatically find a proof? or does the automation need to be generating the theorems themselves?

#### Alex J. Best (Nov 02 2020 at 22:54):

There is some progress towards automation of this by @Scott Morrison at https://leanprover.zulipchat.com/#narrow/stream/116395-maths/topic/definition.20of.20integrally.20closed/near/199303207

#### Patrick Lutz (Nov 02 2020 at 22:57):

Kevin Lacker said:

i've been looking for good target problems to try out

`rewrite_search`

or similar automatic tactics on and i'm curious what people would want automation to do here - is there some set of theorems that you would like to write out the statements and then have the automation automatically find a proof? or does the automation need to be generating the theorems themselves?

Either way would be helpful I guess. In my ideal world, once I know that two things are isomorphic, any time one of them appears in a certain type of expression, I can simply replace it with the other one. But even something that can just automatically fill in proofs would be nice

#### Thomas Browning (Nov 02 2020 at 23:00):

Kevin Buzzard said:

you'll have to prove that for each instance you care about the properties are preserved anyway

So we do need some theorems stating that certain properties are preserved. The question is: In the case of field extensions, what's the right way to state changing the base field?

#### Thomas Browning (Nov 02 2020 at 23:01):

One option that Kevin might be hinting at is to have theorems relating things to subfield E

#### Thomas Browning (Nov 02 2020 at 23:01):

i.e., that properties are preserved when passing to subfield E

#### Thomas Browning (Nov 02 2020 at 23:01):

and then if the subfields agree, then obviously the property is preserved

#### Thomas Browning (Nov 02 2020 at 23:08):

So two options so far are:

(a) prove theorems that properties are preserved when dealing with isomorphic F-algebras (so that you can change the top), and theorems that properties are preserved when passing to `subfield E`

(so that you can change the bottom).

(b) define a general notion of field extension isomorphism (as described at the top of the thread) and prove that properties are preserved by such an isomorphism.

Any others?

#### Mario Carneiro (Nov 02 2020 at 23:12):

I should note that this doesn't require any grand planning. Theorems about preservation under isomorphisms or homomorphisms or surjective homs or subfield extensions are often specific to the context. State it using the language idiomatic to that part of the library, and don't worry about putting all these isomorphism theorems under one banner

#### Kevin Buzzard (Nov 02 2020 at 23:14):

Just thinking about it a bit more (whilst cleaning the kitchen) I realise that transferring a property of $a:F\to E$ over to a property of $a' : F' \to E'$ still feels like a two step process. We have isomorphisms $i:F\to F'$ and $j:E\to E'$ making a commutative square, but now to move from $a$ to $a'$ it feels like the natural way to go is via $a'\circ i:F\to E'$, thus splitting up the transfer problem into two simpler transfer problems of moving from $F\to E$ to $F\to E'$ and from $F\to E'$ to $F'\to E'$ (here using the inverse of $i$).

#### Mario Carneiro (Nov 02 2020 at 23:15):

Can't you also transfer `a:F->E`

to `a:F ~= F'`

where `F' : subfield E`

?

#### Mario Carneiro (Nov 02 2020 at 23:15):

If you have a set-sized class of all subfields, you can transfer structure that way

#### Thomas Browning (Nov 02 2020 at 23:16):

Mario Carneiro said:

Can't you also transfer

`a:F->E`

to`a:F ~= F'`

where`F' : subfield E`

?

Isn't this option (a) above?

#### Kevin Buzzard (Nov 02 2020 at 23:16):

Yes, this is somehow what I was thinking about earlier: because in this situation all maps are injective (any field homomorphism is injective) every field map $F\to E$ is isomorphic to one where $F$ is a subfield of $E$.

#### Thomas Browning (Nov 02 2020 at 23:17):

One slight issue with the subfield approach is that it isn't the most general. Properties like separable and normal are stated in greater generality than just fields (although maybe you could replace subfields with subrings?)

#### Kevin Buzzard (Nov 02 2020 at 23:18):

right, one could imagine working in some appropriate generality which will change depending on what predicate is being transferred.

#### Mario Carneiro (Nov 02 2020 at 23:18):

it's a boon if the collection of F such that E/F is set-sized though

#### Mario Carneiro (Nov 02 2020 at 23:19):

at least up to isomorphism

#### Patrick Lutz (Nov 02 2020 at 23:19):

Why is that useful?

#### Mario Carneiro (Nov 02 2020 at 23:19):

It means you can construct universal objects more easily

#### Mario Carneiro (Nov 02 2020 at 23:20):

I don't know if I can give a specific example off hand though

#### Patrick Lutz (Nov 02 2020 at 23:20):

I see. But that doesn't seem to say which way we should solve this particular problem since in either case, there is still a set-sized collection with a representative from every isomorphism class

#### Mario Carneiro (Nov 02 2020 at 23:20):

sure, but we have regular isos for that

Last updated: May 10 2021 at 07:15 UTC