Restrict algebra equivalence

Stream: Berkeley Lean Seminar

[Patrick Lutz]

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/F$ is a tower of field extensions such that $E$ is the splitting field of some polynomial over $F$. But shouldn't it be enough to assume that $E/F$ is a normal extension (not necessarily finite dimensional)? The proof is just that if you have an $F$-algebra homomorphism $\varphi : K \to K$ then it restricts to a homomorphism of $E$ because everything in $E$ is the root of some polynomial and must therefore go to a root of the same polynomial which is also in $E$ by normality.

[Thomas Browning]

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]

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]

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

[Thomas Browning]

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]

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]

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]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

The point is that one finite extension of $E$, 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]

df.png

[Kevin Buzzard]

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]

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

[Thomas Browning]

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]

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

[Thomas Browning]

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]

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

[Patrick Lutz]

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/F$ is a tower of field extensions and $E$ is the splitting field of some polynomial and $K$ is finite degree over $E$ then the restriction map $Aut(K/F) \to Aut(E/F)$ is surjective. But I think this is only true if $K/F$ is Galois, right? Otherwise you could have a situation where, for example, there is some $\alpha$ in $E$ which has a square root in $K$ but one of its conjugates does not.

[Thomas Browning]

I think that you're right

[Patrick Lutz]

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]

Actually, can we just do it by counting?

[Patrick Lutz]

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

[Patrick Lutz]

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

[Patrick Lutz]

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

[Patrick Lutz]

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

[Patrick Lutz]

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

[Thomas Browning]

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

[Thomas Browning]

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]

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]

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

[Thomas Browning]

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]

yeah, I guess you're right

[Patrick Lutz]

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]

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

[Thomas Browning]

like with alg_hom_equiv_sigma

[Patrick Lutz]

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]

Oh, I didn't realize that

[Patrick Lutz]

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]

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

[Thomas Browning]

Right after the induction lemmas

[Thomas Browning]

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]

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

[Patrick Lutz]

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

I fixed it in a recent commit

[Thomas Browning]

it should go the other way now

[Thomas Browning]

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

[Patrick Lutz]

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]

Yeah, things were weird for me too

[Patrick Lutz]

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

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

[Patrick Lutz]

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]

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]

Kevin Buzzard said:

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

#5768