Finite field extension is obtained by adjoining basis

Stream: new members

[Sebastian Monnet]

Let $E/K$ be a finite field extension, and let $v_1,\ldots, v_n$ be a $K$-basis for $E$. I would like to show that the $v_i$ generate $E$ as a field over $K$. I have stated this as the following lemma.

import tactic
import field_theory.galois
import data.set.basic
import algebra.group.basic

open_locale classical


lemma gen_by_basis {K L : Type*} [field K] [field L] [algebra K L]
{E : intermediate_field K L} (h_findim : finite_dimensional K E) :
E = intermediate_field.adjoin K (finset.univ.image ((algebra_map ↥E L) ∘
finite_dimensional.fin_basis K E)) :=
begin
  sorry,
end

Ideally I'd like to prove the statement in its current form, because it works in the context of a larger proof, but if I've stated it in the "wrong" way, I'd be grateful for help fixing that too.

[Kevin Buzzard]

I think the statement's fine, although I would be tempted to put the more complex term on the left because this is the convention (simp lemmas simplify the LHS to the RHS). I think I'd go for apply le_antisymm as the first line.

[Thomas Browning]

@Sebastian Monnet What is the larger result that you are trying to prove?

[Kevin Buzzard]

You could just use set.range instead of finset.univ.image. Here's one way:

import tactic
import field_theory.galois
import data.set.basic
import algebra.group.basic

open_locale classical


lemma gen_by_basis {K L : Type*} [field K] [field L] [algebra K L]
{E : intermediate_field K L} (h_findim : finite_dimensional K E) :
E = intermediate_field.adjoin K (set.range ((algebra_map ↥E L) ∘
finite_dimensional.fin_basis K E)) :=
begin
  apply le_antisymm,
  {
    sorry },
  { rw intermediate_field.adjoin_le_iff,
    intros l hl,
    simp only [set.mem_range, function.comp_app] at hl,
    rcases hl with ⟨i, rfl⟩,
    let e := (finite_dimensional.fin_basis K ↥E) i,
    exact e.2 }
end

[Kevin Buzzard]

Thomas Browning said:

Sebastian Monnet What is the larger result that you are trying to prove?

He's defining the Krull topology on Galois groups.

[Thomas Browning]

I guess I'm wondering what the result one level up is. When I was working in field theory, working with bases was very painful, but there were usually nice ways to work around them.

[Kevin Buzzard]

It's the definition of the normal closure of an intermediate field E in an extension L/K as the subfield of L obtained by adjoining all the roots of the min polys of a basis.

[Kevin Buzzard]

I mean, it's probably not even the normal closure in any sense, if L/K isn't normal

[Thomas Browning]

Ah, I see. You could also adjoin all roots of all minimal polynomials, but maybe that's not as nice to work with.

[Kevin Buzzard]

then it's not clear that if E/K is findim then NC(E)/K is

[Sebastian Monnet]

Thomas Browning said:

Ah, I see. You could also adjoin all roots of all minimal polynomials, but maybe that's not as nice to work with.

So, the point is that given a finite subextension extension $E/K$ of some extension $L/K$, I need another finite subextension $N/K$ such that for every $K$-algebra equivalence $\sigma:L \to L$, we have $\sigma(E) \subseteq N$. I have defined $N$ by adjoining the roots in $L$ of the product of minimum polynomials of a $K$ basis for $E$, and now I'm trying to prove that indeed $\sigma(E) \subseteq L$. In order to do that, I need the fact that $E$ is generated by its basis, from which it follows that $\sigma(E)$ is generated by the image of the basis. I have almost the whole proof, dependent on this sorried lemma and also one other detail that I'm currently working on.

[Johan Commelin]

@Sebastian Monnet In your example, you are picking an arbitrary basis using choice using the finite-dimensionality assumption. I think it might be better to include an arbitrary basis in your assumptions.

[Johan Commelin]

In general, there should be a lemma saying that if $B/A$ is generated by s as a module, then it's also generated by s as algebra (or intermediate field, when this applies).

[Johan Commelin]

So I think you can generalise your statement a bit, which might also make it easier to prove.

[Sebastian Monnet]

Johan Commelin said:

Sebastian Monnet In your example, you are picking an arbitrary basis using choice using the finite-dimensionality assumption. I think it might be better to include an arbitrary basis in your assumptions.

Yeah that's a good point. I was hoping that lean would be just fixing a basis once and for all somewhere, but I have no idea what's going on under the hood

[Sebastian Monnet]

Johan Commelin said:

In general, there should be a lemma saying that if $B/A$ is generated by s as a module, then it's also generated by s as algebra (or intermediate field, when this applies).

Good idea. Looking through the library now :)

[Kevin Buzzard]

This normal-closure-like construction should probably have its own definition and API. Right now I'm not even 100% sure that the definition above gives a well-defined object ie independent of choice of basis. Right now Sebastian is only using the construction as a temporary measure. There's a good notion of algebraic closure of an intermediate field in a bigger field but I don't know if there's a good definition of normal closure. My vague worry is that the normal closure of a sub-intermediate field equipped with a different basis might not be contained in the normal closure of the bigger field, as Sebastian has defined it (subfield generated by roots of min polys of a basis)

[Johan Commelin]

Kevin Buzzard said:

He's defining the Krull topology on Galois groups.

Can you remind me why you need normal closure for this? I might be missing something obvious. But I think you only need to know what finite Galois subextensions are to define this topology, right?

[Kevin Buzzard]

That's correct, but he's also proving that Gal(L/E) is open if E/K is finite (basically as a proof that he's defined the right topology) and to do this he is using the theory of group filter bases (which Patrick set up for us in the perfectoid project and which is now in mathlib) and it apparently shows up in the axioms there.

[Kevin Buzzard]

There's a cheap method for getting the topology of the form "these sets should be open, now look at the group topology they generate" but with group topologies it turns out not to be true in general that the sup of the group topologies making given sets open still has all those given sets open, there was extensive discussion about this point last week

[Kevin Buzzard]

At the end of the day we want to prove the Galois correspondence for infinite extensions but I had not realised that we have still not proved that for finite extensions, the subgroup is normal iff the subfield is normal, and this construction could also be regarded as a step in the direction towards proving this

[Johan Commelin]

Yeah, that seems like good target on the way to the infinite gc

[Kevin Buzzard]

Interestingly, Sebastian is going to end up putting a topology on Aut_K(L) for an arbitrary extension of fields L/K. It coincides with the Krull topology in the case that the extension is Galois

[Kevin Buzzard]

I now wonder whether instead of working with intermediate_fields he could have worked with an arbitrary extension of commutative rings B/A and used subrings which were fg or Noetherian as A-modules for the basis of open sets

[Sebastian Monnet]

I'm still pretty stuck on this. I've reduced the statement to the following lemma.

lemma subalg_le_gen_by_basis {K L : Type*} [field K] [field L] [algebra K L]
{E : intermediate_field K L} (h_findim : finite_dimensional K E)
(b := finite_dimensional.fin_basis K ↥E)
(S : set L := (finset.image ((algebra_map ↥E L) ∘ b) finset.univ)) :
E.to_subalgebra ≤ algebra.adjoin K S :=
begin
   intros x hx,
   change x ∈ E at hx,
   let x' : ↥E := ⟨x, hx⟩,
   have hx' := basis.mem_span b x',
   apply algebra.span_le_adjoin K S,
   sorry,
end

As @Johan Commelin suggested, I used a lemma relating being generated as an algebra to being generated as a module, but now I basically have type-theoretic issues. Currently the hypothesis hx' is basically the same as the goal, but I need to map from ↥E to L. I tried mapping to L with something like

have h : (algebra_map ↥E L) x' ∈ submodule.algebra_map (algebra_map ↥E L) (submodule.span K (set.range ⇑b))

but this didn't work. I'm at a bit of a loss here, so I'd really appreciate any help!

[Eric Rodriguez]

opt param lets you do something like this:

  have := @subalg_le_gen_by_basis _ _ _ _ _ _ (show finite_dimensional ℚ (⊤ : intermediate_field ℚ ℂ), from sorry) _ {},

replace ℂ with something that's actually fin-dim over ℚ and you clearly have a contradiction

[Eric Rodriguez]

I think you ned to write the definition of S by hand

[Sebastian Monnet]

Eric Rodriguez said:

I think you ned to write the definition of S by hand

What do you mean by this? As in I need to just put (finset.univ.image ((algebra_map ↥E L) ∘ finite_dimensional.fin_basis K E)) every time I've written S?

[Eric Rodriguez]

yeah

[Yakov Pechersky]

Or have "hs : S = ..."

[Yakov Pechersky]

Such helper hypotheses usually work much better than relying on opt_param like (b := ...)

[Eric Rodriguez]

this seems like a much more palatable goal:

lemma subalg_le_gen_by_basis {K L : Type*} [field K] [field L] [algebra K L]
{E : intermediate_field K L} (h_findim : finite_dimensional K E)
(b := finite_dimensional.fin_basis K ↥E) :
E.to_subalgebra ≤ algebra.adjoin K (finset.image ((algebra_map ↥E L) ∘ b) finset.univ) :=
begin
   intros x hx,
   change x ∈ E at hx,
   let x' : ↥E := ⟨x, hx⟩,
   have hx' := basis.mem_span b x',
   apply algebra.span_le_adjoin K _,
   simp only [function.comp_app, finset.coe_image, finset.coe_univ, set.image_univ],
   rw set.range_comp,
   sorry
end

[Sebastian Monnet]

@Eric Rodriguez yes, that is much more palatable, thank you. I've progressed a little further and now have this:

lemma subalg_le_gen_by_basis' {K L : Type*} [field K] [field L] [algebra K L]
{E : intermediate_field K L} (h_findim : finite_dimensional K E)
(b := finite_dimensional.fin_basis K ↥E) :
E.to_subalgebra ≤ algebra.adjoin K (finset.image ((algebra_map ↥E L) ∘ b) finset.univ) :=
begin
   intros x hx,
   change x ∈ E at hx,
   let x' : ↥E := ⟨x, hx⟩,
   have hx' := basis.mem_span b x',
   apply algebra.span_le_adjoin K _,
   simp only [function.comp_app, finset.coe_image, finset.coe_univ, set.image_univ],
   rw set.range_comp,
   have h2 : (E.val '' set.range ⇑b) =
   (⇑(algebra_map ↥E L) '' set.range ⇑b),
   {
     ext y,
     split,
     {
        intro hy,
        exact hy,
     },
     {
       intro hy,
       exact hy,
     },
   },
   rw ← h2,
   sorry,
end

What I'd like to do now is

have h3 : submodule.span K ((E.val) '' (set.range ⇑b)) =
   submodule.map (E.val) (submodule.span K (set.range ⇑b))

but I can't because E.val is not the right kind of map. It's a K-algebra map and not a semilinear map over K. Do you have any idea how to coerce E.val into the form I need?

[Kevin Buzzard]

ext y, split, {intro hy, exact hy}, {intro hy, exact hy} is just a very long way of saying refl :-)

[Sebastian Monnet]

Kevin Buzzard said:

ext y, split, {intro hy, exact hy}, {intro hy, exact hy} is just a very long way of saying refl :-)

Good point

[Kevin Buzzard]

have h3 : submodule.span K ((E.val) '' (set.range ⇑b)) =
   submodule.map (E.val : E →ₗ[K] L) (submodule.span K (set.range ⇑b)),

seems to work for your h3.

[Kevin Buzzard]

(I guess there's a coercion from K-algebra ring maps to K-linear module maps, and linear things are semilinear; I don't quite understand linear algebra in Lean any more ;-) )