normal closure

Stream: maths

[Kevin Buzzard]

IF L/K is an algebraic field extension and E is an intermediate field, then one can define the "normal closure" N of E to be the sub-K-field of L generated by all the elements x of L such that the min poly of x is also the min poly of an element of E. I write the phrase in quotes because if L/K is not normal then N/K may not be normal either, although it is "normal within the context of subfields of L" in the sense that any K-field map phi : L -> L is guaranteed to send N into N. Note that E \subset N and that if E/K is finite then so is N/K. In particular L/K is a union of fields which are "finite normal closures" (for x in L set E=k(X)) and (because an injective linear map from a f.d.v.s to itself is surjective) we deduce the theorem that if L/K is algebraic then any K-field map L -> L is bijective. This trivially implies docs#alg_hom.normal_bijective (a map which after composition with an injection becomes a bijection must have already been a bijection) and furthermore I never used the assumption that L/K was normal, which is an assumption in the linked lemma. Have I made a mistake? Is there some general abstraction which this is a special case of? It feels like what is going on is that given an algebraic field extension L/K and a subset s of L there's an nclosure s : intermediate_field K L which is the smallest subfield containing s with this relative normality property, and presumably the theorem is that if L/K is normal then so is nclosure s / K. I'm assuming we don't have any of this stuff in mathlib?

[Kevin Buzzard]

So if L/K is algebraic then there's a predicate on intermediate_field K L called is_relatively_normal E which says "for all K-fields Q, and K-field morphisms f : L->Q, the image of E is independent of f" and the theorem is that E is relatively normal iff it's nclosure of itself. @Iván Sadofschi Costa @Thomas Browning What do you think? Maria Ines would like the theory of normal closures and I was just wondering what it should look like.

[Kevin Buzzard]

OK so based on some preliminary thoughts, I am wondering whether an algebraic field extension L/K being normal can be thought of as "L is a relatively normal subextension of L-bar/K", and there is a relative theory of normality which is not covered by what we have in mathlib. Here are some mathematical questions about this construction; I've formalised them so I may as well ask them in Lean:

import field_theory.adjoin

-- # Relative normal closures.

namespace intermediate_field

/-- If L/K is an (algebraic) field extension then the relative normal closure `nclosure K S`
of a subset S of L (for example, of a subfield E with K ⊆ E ⊆ L) is the intermediate
extension generated by all the elements of L which are zeros of the minimum polynomoals
of the elements of `S`. -/
def nclosure (K : Type*) [field K] {L : Type*} [field L] [algebra K L] (S : set L) :
  intermediate_field K L :=
adjoin K {x : L | ∃ s ∈ S, minpoly K x = minpoly K s }

variables {K L : Type*} [field K] [field L] [algebra K L]

/-- An intermediate subfield of `L/K` is (relatively) normal-closed over `K` if
it its own relative normal closure. -/
def is_nclosed (E : intermediate_field K L) : Prop := E = nclosure K E

-- another candidate definition
def is_nclosed' (E : intermediate_field K L) : Prop := ∃ T : set L, E = nclosure K T

variable {E : intermediate_field K L}

-- is this true?
lemma conjecture1 : is_nclosed E ↔ is_nclosed' E := sorry

-- if conjecture1 is false then this conjecture may need to be modified to use the
-- other definition of "is normal-closed" (however if conjecture 1 is
-- false then I might be barking up the wrong tree anyway)

lemma conjecture2 {E : intermediate_field K L} (hE : is_nclosed' E) {x y : L}
  (hxy : minpoly K x = minpoly K y) (hxE : x ∈ E) : y ∈ E :=
begin
  sorry
end

end intermediate_field

Everything typechecks for L/K arbitrary but minpoly returns junk values in this case, and this is really a question about minpoly. Say L/K is algebraic. Then there's a map from L to K[X] with finite fibres, sending an element of L to its min poly over K. Within the context of living in this fixed universe L/K, we can define two elements of L to be conjugate (more precisely L/K-conjugate) if their min polys over K are equal. Think of these things as "conjugacy classes". I want to define a subextension E/K of L/K to be relatively normal (with respect to the extension L/K) if it's a union of conjugacy classes, so just like in group theory. One question I don't know the answer to: take a random subset of L which is a union of conjugacy classes. Is the intermediate extension which it generates also a union of conjugacy classes? This is what it all boils down to.

[Kevin Buzzard]

It feels to me like this is might be related to "normal iff splitting field", which is a tricky proof in Galois theory (certainly I've made a real meal of this before when lecturing it) but you can't just apply the proof because in the relative situation maybe things aren't "absolutely normal", they're just normal within the context of L.

"splitting fields are normal" sounds to me like it's saying "in the case where L=K-bar, the subfield of L generated by a union of conjugacy classes is itself a union of conjugacy classes". I think that if we want to develop a nice theory of normal closures (which is where all this is coming from, María Inés needs normal closures in her work) then it might be nice to get to the bottom of this!

[Kevin Buzzard]

An algebraic extension N/K is normal iff "every irreducible polynomial over K with a root in N, splits in N". This is what I've been telling undergraduates for years and it's a really weird definition. How about "N/K is normal iff N is a union of conjugacy classes in the extension L/K with L=N-bar"? And "splitting field iff normal" says "a K-subfield of K-bar is a union of conj classes iff it's generated as a field by a union of conjugacy classes".

[Thomas Browning]

Do you think you could you also define the normal closure of K in L as the interemediate field generated by the images of the algebra maps K -> L ? Should this give the same thing?

[Johan Commelin]

You mean the intermediate field generated by the images of algebra maps E → L, right?
(There is only one alghom K → L.)

[Thomas Browning]

Oh interesting. I guess I was trying to say the images of the ring homs K -> L. But if you start with an intermediate field E of L/K, then yes, you might as well look at algebra homs E -> L.

[Kevin Buzzard]

Right, this is where it all started. I wanted to define normal closure of some algebraic extension A/B of fields, and I defined it to be the subfield generated by the images of all the B-homs from A into B-bar. To prove it's normal I wanted a condition saying that an algebraic extension A/B is normal iff for all B-fields C and B-algebra maps i j : A -> C, i(A) <= j(A) [and hence i(A)=j(A) by symmetry].

[Thomas Browning]

Another question: Do these definitions of the normal closure of a set "factor through" intermediate_field.adjoin? In other words, does nclosure K S = nclosure' (adjoin K S), where nclosure' E is defined as one of the following:

• The intermediate field of L/K generated by elements satisfying the minimal polynomial condition
• The intermediate field of L/K consisting of those elements satisfying the minimal polynomial condition (it's not immediately clear to me if this is automatically a field)
• The intermediate field of L/K generated by the images of alghoms E -> L

[Thomas Browning]

Because it would be really nice if you could just define: The normal closure of E is just the intermediate field of elements of L satisfying the minimal polynomial condition.

[Thomas Browning]

If so, then I think it's obvious that normal closure is idempotent (Let E' be the normal closure of E, and let E'' be the normal closure of E'. If x in E'', then x has the same minpoly as an element y of E', but y has the same minpoly of an element z of E, so x has the same minpoly as an element z of E, so x lies in E'). And idempotence of normal closure is just a restatement of @Kevin Buzzard's conjecture1, I think.

[Thomas Browning]

Thomas Browning said:

• The intermediate field of L/K consisting of those elements satisfying the minimal polynomial condition (it's not immediately clear to me if this is automatically a field)

Alas, I think this is not automatically a field, even if L/K is Galois. Take E=Q(sqrt[3]2). Then this bad definition doesn't contain any quadratic elements, but it should.

[Kevin Buzzard]

import field_theory.intermediate_field

universes u v

variables {K : Type u} [field K] {L : Type v} [field L] [algebra K L]

-- T could be an ID but not a general comm ring
def is_normal (E : intermediate_field K L) : Prop :=
∀ {T : Type v} [field T], by exactI
∀ [algebra K T], by exactI
∀ (φ ψ : L →ₐ[K] T), (φ : L → T) '' E.carrier = (ψ : L → T) '' E.carrier

Is this some standard abstraction? If L/K is algebraic and normal then I think that is_normal E iff E/K is normal.

[Kevin Buzzard]

If you just have a general algebraic E/K and you want to know if it's normal, just let L be E-bar. ("choose a geometric point")

[Kevin Buzzard]

but this definition is way cooler than "every irreducible polynomial which has a root in N splits completely in N".

[Kevin Buzzard]

Oh L is just junk.

[Kevin Buzzard]

This is it:

import field_theory.intermediate_field

universes u v

-- T could be an ID but not a general comm ring
def is_normal {K : Type u} [field K] {L : Type v} [field L] [algebra K L] : Prop :=
∀ {T : Type v} [field T], by exactI
∀ [algebra K T], by exactI
∀ (φ ψ : L →ₐ[K] T), set.range φ = set.range ψ

For algebraic extensions this should be equivalent to normal.

[Kevin Buzzard]

and I think that developing normal closure along those lines might be nicer.

[Iván Sadofschi Costa]

If L/K is algebraic then another equivalent way to define the normal closure of S in L would be to intersect with L the splitting field of S in some algebraic closure Lbar of L.

If L/K is algebraic and E is a subextension, I think we could define is_relatively_normal K E L as "∀ φ : L →ₐ[K] Lthe image of E by φ is equal to E". Then is_normal K L could be defined as is_relatively_normal K L (algebraic_closure L).

[Iván Sadofschi Costa]

Or maybe as ∀ T, is_relatively_normal K L T which avoids considering the algebraic closure and is more similar in spirit to the definition above.

[Junyan Xu]

@Kevin Buzzard For the original conjecture1 : is_nclosed E ↔ is_nclosed' E, i.e. if E is the nclosure of some set T in L, whether E must be the nclosure of itself, it turns out the answer is no, even if T is itself a field. The way I solved the problem is by converting it to a (finite) group theory problem using Galois theory: embed L/K into a Galois extension and for any intermediate field F, denote by $G_F$ the subgroup of the Galois group $G = G_K$ that fixes F. By considering all elements of L that share a minpoly with some element of T, you are considering all embeddings of subfields of T into L over K, since every subfield is generated by one element over K (assuming we are in the separable case). E := nclosure K T therefore correspond to the subgroup $G_E$ that is the intersection of all subgroups of the form $H^\sigma$, such that $\sigma\in G$, $G_T \leq H$, and $G_L \leq H^\sigma$, where H corresponds to intermediate fields of T/K, $\sigma$ corresponds to their embeddings into the big Galois extension over K, and $G_L \leq H^\sigma$ means we only consider the embeddings with image in L.

Now consider the following example: let $G=S_7$ be the symmetric group on {1,2,...,7}, let $G_T$ be the maximal subgroup fixing 7, and let $G_L$ be the subgroup of permutations preserving the partition 12|34|5|6|7, isomorphic to Z/2 x Z/2. Since $G_T$ is maximal, H can only be $G_T$ or $G$. $G_E$ is therefore equal to the intersection of conjugates of $G_T$ containing $G_L$, which is equal to the subgroup preserving the partition 1234|5|6|7, isomorphic to $S_4$. This is the subgroup corresponding to the E := nclosure K T. I claim that nclosure K E = L ≠ E. Notice that $G_E$ is a subgroup of the subgroup of $S_7$ preserving 1234|567. Since the intersectino of three conjugate of this subgroup, preserving 1234|567, 1256|347, 1257|346 respectively, is already equal to $G_L$ (preserving 12|34|5|6|7), the intersection of all $H^\sigma$ must be equal to $G_L$, meaning that nclosure K E = L. This gives rise to a counterexample to conjecture1 and shows that counterexamples exists with K = ℚ, for example.

[Kevin Buzzard]

Yeah, thanks, it looks like the relative version is hence uninteresting. I couldn't get the usual proof to generalise so I'm not surprised there's counterexamples. Thanks!