Zulip Chat Archive

Stream: Berkeley Lean Seminar

Topic: Restrict algebra equivalence


Patrick Lutz (Jan 09 2021 at 19:51):

I was thinking about alg_equiv.restrict_is_splitting_field and it seems to me like the theorem could actually be made more general without much more work (though maybe that's too naive). The current assumption is that K/E/FK/E/F is a tower of field extensions such that EE is the splitting field of some polynomial over FF. But shouldn't it be enough to assume that E/FE/F is a normal extension (not necessarily finite dimensional)? The proof is just that if you have an FF-algebra homomorphism φ:KK\varphi : K \to K then it restricts to a homomorphism of EE because everything in EE is the root of some polynomial and must therefore go to a root of the same polynomial which is also in EE by normality.

Thomas Browning (Jan 09 2021 at 20:33):

Yeah, I was realizing this. Unfortunately, we don't know that splitting fields are normal (it's a TODO in normal.lean). I was working on this a bit last night and it seems hard

Patrick Lutz (Jan 10 2021 at 01:38):

Thomas Browning said:

Yeah, I was realizing this. Unfortunately, we don't know that splitting fields are normal (it's a TODO in normal.lean). I was working on this a bit last night and it seems hard

We only know they're normal if the polynomial is separable right?

Kevin Buzzard (Jan 10 2021 at 01:39):

splitting field -> normal is one of the hardest theorems in a Galois theory course!

Thomas Browning (Jan 10 2021 at 01:44):

Patrick Lutz said:

Thomas Browning said:

Yeah, I was realizing this. Unfortunately, we don't know that splitting fields are normal (it's a TODO in normal.lean). I was working on this a bit last night and it seems hard

We only know they're normal if the polynomial is separable right?

Lean only knows this right now, but I know it in general

Kevin Buzzard (Jan 10 2021 at 01:46):

When I proved it in my course I used some awful proof. Someone told me afterwards that there was a proof by induction on degree in Dummitt and Foote but I was skeptical that it could be made to work. I went to take a look and found that they were right though.

Kevin Buzzard (Jan 10 2021 at 01:48):

I think I followed the proof in Garling's book (the book I'd learnt the theory from) which is much nastier. It introduces some auxiliary condition which it proves is equivalent to normality and also to splitting field. I seem to have a sketch of the D&F proof my crappy proof:

Kevin Buzzard (Jan 10 2021 at 01:53):

Say F/E is the splitting field of fE[X]f\in E[X]. Now say $$p\in E[X]$ is irreducible and has a root αF\alpha\in F. We want to show that pp splits completely in FF. Consider pF[X]p\in F[X]; it factors into irreducibles. Let q(X)q(X) be one of them. It suffices to show the degree of qq is 1. It's irreducible, so we can throw in a root β\beta and get F(β)=F[X]/(q)F(\beta)=F[X]/(q). Within F(β)F(\beta) we see that FF is a splitting field for ff over E(α)E(\alpha), and F(β)F(\beta) is a splitting field for ff over E(β)E(\beta). But E(α)E(\alpha) is isomorphic to E(β)E(\beta) via an isomorphism sending ff to ff (because they're both E[X]/(p)E[X]/(p) and so if you know uniqueness up to (non-unique) isomorphism of splitting fields then you win because this implies [F(β):E(β)]=[F:E(α)][F(\beta):E(\beta)]=[F:E(\alpha)] so F(β)=FF(\beta)=F by a degree count.

Kevin Buzzard (Jan 10 2021 at 01:54):

Aah, but uniqueness of splitting fields is what takes me ages :-(

Kevin Buzzard (Jan 10 2021 at 01:56):

Perhaps this is what D&F do better than me. If EE is a field and pE[X]p\in E[X] is a poly then TFAE: (1) F/EF/E is a splitting field for pp, (2) FF has property (*) for (E,p)(E,p). Property (*) is "if EKE\to K is an extension of fields then p(X)p(X) splits completely in KK iff there's an EE-algebra map FKF\to K".

Kevin Buzzard (Jan 10 2021 at 01:57):

I would not recommend this route. I don't remember the D&F proof.

Kevin Buzzard (Jan 10 2021 at 02:00):

The point is that one finite extension of EE, up to isomorphism, has property (*) because of the usual universal property proof; given two, (*) gives you a map between them which must be an iso for degree reasons.

Kevin Buzzard (Jan 10 2021 at 02:17):

df.png

Kevin Buzzard (Jan 10 2021 at 02:17):

there's the D+F proof and it's less horrible than mine. It gives uniqueness of splitting fields. Do we have that?

Thomas Browning (Jan 10 2021 at 02:29):

I think so (we can construct maps in both directions, and look at dimensions)

Thomas Browning (Jan 11 2021 at 07:28):

I've been working on splitting field implies normal. I was looking at this pdf: http://www.pitt.edu/~gmc/algebra/galoistheory.pdf

That pdf supposedly deduces Corollary 7.7 from Theorem 7.6. I formalized Theorem 7.6 (statement below, proof is done), but am struggling to see how to deduce "splitting field implies normal"

theorem main_theorem {F E K : Type*} [field F] [field E] [field K] [algebra F E] [algebra F K]
{S : finset E}
(hK :  x  S,  H : is_integral F (x : E), (minimal_polynomial H).splits (algebra_map F K)) :
nonempty ((adjoin F (S : set E)) →ₐ[F] K) :=

Thomas Browning (Jan 11 2021 at 07:28):

I guess, is this lifting result powerful enough to deduce "splitting field implies normal"?

Thomas Browning (Jan 11 2021 at 07:52):

Actually, I see a way forward. Assume that E/F is the splitting field of p. Let x be an element of E. Let m be the minimal polynomial of x over F. Let K be the splitting field of m over E (so now we have K/E/F). Let y be a root of m. We can use main_theorem to construct an F(y)-algebra homomorphism E(y) -> E. By dimensions, y is in E.

Thomas Browning (Jan 11 2021 at 07:52):

I won't finish this tonight, but it seems very doable.

Patrick Lutz (Jan 14 2021 at 05:23):

I was starting to think about alg_equiv.restrict_is_splitting_field_hom_surjective tonight and I think it's missing a hypothesis. Currently it says that if K/E/FK/E/F is a tower of field extensions and EE is the splitting field of some polynomial and KK is finite degree over EE then the restriction map Aut(K/F)Aut(E/F)Aut(K/F) \to Aut(E/F) is surjective. But I think this is only true if K/FK/F is Galois, right? Otherwise you could have a situation where, for example, there is some α\alpha in EE which has a square root in KK but one of its conjugates does not.

Thomas Browning (Jan 14 2021 at 05:25):

I think that you're right

Patrick Lutz (Jan 14 2021 at 05:28):

Also, the proof should be pretty similar to the proof that the splitting field of a separable polynomial is Galois. I wonder if we can factor out some common lemmas

Patrick Lutz (Jan 14 2021 at 05:30):

Actually, can we just do it by counting?

Patrick Lutz (Jan 14 2021 at 05:30):

it would be enough to know that the kernel has size Aut(K/F)/Aut(E/F)|Aut(K/F)|/|Aut(E/F)| right?

Patrick Lutz (Jan 14 2021 at 05:31):

which is equal to [K:F]/[E:F][K : F]/[E : F] if they're both Galois

Patrick Lutz (Jan 14 2021 at 05:31):

which is also equal to [K:E][K : E]

Patrick Lutz (Jan 14 2021 at 05:32):

so we would really just need to know that there are [K:E][K : E] automorphisms of KK which fix EE. But we know that already

Patrick Lutz (Jan 14 2021 at 05:32):

although this argument would require the extra assumption that EE is Galois, not just the splitting field of some polynomial

Thomas Browning (Jan 14 2021 at 05:37):

I feel like surjectivity should follow from some general lemma about lifting automorphisms

Thomas Browning (Jan 14 2021 at 05:40):

I recently proved this:

theorem main_theorem {F E K : Type*} [field F] [field E] [field K] [algebra F E] [algebra F K]
{S : finset E}
(hK :  x  S,  H : is_integral F (x : E), (minimal_polynomial H).splits (algebra_map F K)) :
nonempty ((adjoin F (S : set E)) →ₐ[F] K) :=

which tells you that an inclusion F -> K lifts to an inclusion F(S) -> K, provided that the minimal polynomial of each element of S splits in K.

Does this imply surjectivity? You want to lift an inclusion E -> K to an inclusion K->K, so you just need to know that K/E is generated by elements whose minimal polynomial (over E) splits in K

Thomas Browning (Jan 14 2021 at 05:42):

so does surjectivity hold as long as K is a splitting field over E? (this would be weaker than saying that K/F is Galois)

Patrick Lutz (Jan 14 2021 at 05:47):

I'm not sure I follow what you're saying. We need to lift a map E/FE/FE/F \to E/F to a map K/FK/FK/F \to K/F. But I don't exactly see how to do that from the theorem you just stated

Thomas Browning (Jan 14 2021 at 05:54):

Let me think. So start with an F-algebra homomorphism f : E -> E. This induces an F-algebra homomorphism g : E -> K. Let K' denote K with E-algebra structure given by g. Assume that K=E(S) where each element of S has minimal polynomial over E that splits in K. I think the theorem gives an E-algebra homomorphism E(S) -> K'. This is the same as an F-algebra homomorphism K -> K that extends g.

Patrick Lutz (Jan 14 2021 at 05:58):

yeah, I guess you're right

Patrick Lutz (Jan 14 2021 at 05:59):

It feels like having the two different instances of algebra E K floating around might confuse Lean but I guess it should be okay

Thomas Browning (Jan 14 2021 at 06:00):

You might need to have some @'s and ring_hom.to_algebra's floating around

Thomas Browning (Jan 14 2021 at 06:00):

like with alg_hom_equiv_sigma

Patrick Lutz (Jan 14 2021 at 20:17):

Thomas Browning said:

I recently proved this:

theorem main_theorem {F E K : Type*} [field F] [field E] [field K] [algebra F E] [algebra F K]
{S : finset E}
(hK :  x  S,  H : is_integral F (x : E), (minimal_polynomial H).splits (algebra_map F K)) :
nonempty ((adjoin F (S : set E)) →ₐ[F] K) :=

which tells you that an inclusion F -> K lifts to an inclusion F(S) -> K, provided that the minimal polynomial of each element of S splits in K.

Does this imply surjectivity? You want to lift an inclusion E -> K to an inclusion K->K, so you just need to know that K/E is generated by elements whose minimal polynomial (over E) splits in K

This theorem could also be used to construct the embedding F(a, b) -> (p * q).splitting_field that we need for the compositum case. But maybe you already realized that.

Thomas Browning (Jan 14 2021 at 20:26):

Oh, I didn't realize that

Patrick Lutz (Jan 15 2021 at 00:44):

Thomas Browning said:

I recently proved this:

theorem main_theorem {F E K : Type*} [field F] [field E] [field K] [algebra F E] [algebra F K]
{S : finset E}
(hK :  x  S,  H : is_integral F (x : E), (minimal_polynomial H).splits (algebra_map F K)) :
nonempty ((adjoin F (S : set E)) →ₐ[F] K) :=

which tells you that an inclusion F -> K lifts to an inclusion F(S) -> K, provided that the minimal polynomial of each element of S splits in K.

Does this imply surjectivity? You want to lift an inclusion E -> K to an inclusion K->K, so you just need to know that K/E is generated by elements whose minimal polynomial (over E) splits in K

Is this anywhere in the abel-ruffini branch right now?

Thomas Browning (Jan 15 2021 at 00:45):

Yes, it should be at the bottom of adjoin.lean

Thomas Browning (Jan 15 2021 at 00:45):

Right after the induction lemmas

Thomas Browning (Jan 15 2021 at 00:48):

It's possible that we'll also want a corollary stating nonempty (E →ₐ[F] K), assuming that (adjoin F (S : set E)) = top

Patrick Lutz (Jan 15 2021 at 00:49):

I agree. Although the use I mentioned earlier today doesn't require that form

Patrick Lutz (Jan 15 2021 at 01:39):

@Thomas Browning I think the fact that you made field_theory/adjoin.lean import field_theory/normal.lean has created a circular series of dependencies and so I can't get several files to compile

Thomas Browning (Jan 15 2021 at 01:39):

I fixed it in a recent commit

Thomas Browning (Jan 15 2021 at 01:39):

it should go the other way now

Thomas Browning (Jan 15 2021 at 01:40):

https://github.com/leanprover-community/mathlib/commit/aed1157e4212fd6a23ede26bce59fd47f184c22a

Patrick Lutz (Jan 15 2021 at 01:41):

Oh, I didn't see that you made more commits. The weird thing is that everything was still compiling fine in abel_ruffini.lean until I closed VS Code and opened it again. And then nothing would compile

Thomas Browning (Jan 15 2021 at 01:42):

Yeah, things were weird for me too

Patrick Lutz (Jan 15 2021 at 02:27):

@Thomas Browning I renamed the lemma is_integral to SBR_is_integral for now because it was conflicting with the usual meaning of is_integral

Thomas Browning (Jan 15 2021 at 02:29):

sure. I guess SBR.is_integral is fine outside the SBR namespace, but this is a problem inside the SBR namespace.

Patrick Lutz (Jan 15 2021 at 02:36):

Thomas Browning said:

sure. I guess SBR.is_integral is fine outside the SBR namespace, but this is a problem inside the SBR namespace.

yeah, that's the problem I was running into

Patrick Lutz (Jan 15 2021 at 02:37):

I'm fine renaming it anything I just want to make sure we can also use the normal is_integral inside the SBR namespace

Thomas Browning (Jan 16 2021 at 04:06):

Kevin Buzzard said:

splitting field -> normal is one of the hardest theorems in a Galois theory course!

#5768


Last updated: Dec 20 2023 at 11:08 UTC