Isomorphism of Field Extensions

Stream: maths

[Thomas Browning]

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]

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

[Thomas Browning]

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]

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]

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

[Patrick Lutz]

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]

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]

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]

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]

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]

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]

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]

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

[Kevin Buzzard]

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

[Patrick Lutz]

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]

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]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

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]

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]

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]

This is a good test question!

[Kevin Buzzard]

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

[Kevin Buzzard]

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]

F isn't a subfield of E though

[Thomas Browning]

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

[Kevin Buzzard]

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

[Thomas Browning]

that would be (bot : intermediate_field)

[Thomas Browning]

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

[Kevin Buzzard]

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]

(and might be there already)

[Thomas Browning]

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]

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]

(without using intermediate_field)

[Kevin Buzzard]

So what does your normal predicate eat right now?

[Thomas Browning]

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

[Thomas Browning]

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

[Thomas Browning]

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]

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]

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]

yes

[Kevin Buzzard]

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]

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]

yeah, when I say normal bot E, there's secretly an algebra structure algebra bot E

[Kevin Buzzard]

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

[Thomas Browning]

in general, if K : intermediate_field F E then there is an algebra structure algebra F K and algebra K E

[Kevin Buzzard]

What's the definition of normal?

[Kevin Buzzard]

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]

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]

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]

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]

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

[Thomas Browning]

yes, we'll have to do basically that proof

[Thomas Browning]

but it's a question of how to state it

[Kevin Buzzard]

I see

[Patrick Lutz]

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]

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

[Kevin Buzzard]

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]

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

[Kevin Buzzard]

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]

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]

I agree with kevin that two isomorphisms are harder than one

[Mario Carneiro]

what applications would this be put to?

[Thomas Browning]

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

[Kevin Buzzard]

@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]

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]

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

[Mario Carneiro]

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

[Patrick Lutz]

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]

It can't be automated until it is done manually

[Patrick Lutz]

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]

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]

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

[Patrick Lutz]

I see what you mean now

[Mario Carneiro]

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]

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]

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]

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]

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]

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]

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]

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

[Thomas Browning]

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

[Thomas Browning]

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

[Thomas Browning]

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]

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]

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]

Can't you also transfer a:F->E to a:F ~= F' where F' : subfield E?

[Mario Carneiro]

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

[Thomas Browning]

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]

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]

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]

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

[Mario Carneiro]

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

[Mario Carneiro]

at least up to isomorphism

[Patrick Lutz]

Why is that useful?

[Mario Carneiro]

It means you can construct universal objects more easily

[Mario Carneiro]

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

[Patrick Lutz]

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]

sure, but we have regular isos for that