Normal Galois Correspondence

Stream: Berkeley Lean Seminar

[Sean Gonzales]

In trying to prove that normal extensions correspond to normal subgroups, I need to show that if $L/F$ is a Galois extension and $K$ is an intermediate field, then the fixing subgroup of $K$ is normal iff $\text{Gal}(L/F)$ stabilizes $K$. Assuming the fixing subgroup of $K$ is normal, how I would think to do this is to take an element $x \in K$ and $g \in \text{Gal}(L/F)$, and show that for any $h \in \text{Gal}(L/K)$ we have $h \cdot (g \cdot x) = g \cdot x$, hence $g \cdot x \in K$. However, I'm having trouble using this characterization of fixed fields. My scratchwork attempt so far is this:

import field_theory.galois

lemma normal_iff_fixing (F L : Type*)
  [field F] [field L] [algebra F L] [is_galois F L]
  [finite_dimensional F L] (K : intermediate_field F L) :
  K.fixing_subgroup.normal ↔ ∀ (g : L ≃ₐ[F] L) (x : L), x ∈ K → g • x ∈ K :=
begin
  split,
  {
    intros hk_normal g x hxk,
    have hk_fixing := is_galois.fixed_field_fixing_subgroup K,
    rw ← hk_fixing,
    rw intermediate_field.fixed_field,
    rw fixed_points.intermediate_field,
  },
  {

  },
end

What I want is to use the fact that an element is in $K$ if and only if an arbitrary element of $\text{Gal}(L/K)$ fixes it. I'm having trouble figuring out which rewrites will get me to this condition.

[Kevin Buzzard]

Can you add imports and any opens to make your code a #mwe ? (just edit your message, don't post a new one)

[Sean Gonzales]

There's a lemma in fixing_subgroup.lean which is essentially backwards of what I want: it says "an element is in a fixing subgroup of a set iff it fixes every element of the set". Rather, I want "an element is in a set iff every element of its fixing subgroup fixes it". Does this lemma exist? I'm having trouble locating it.

[Kevin Buzzard]

Here's a direct proof, if this helps:

import field_theory.galois

lemma normal_iff_fixing (F L : Type*)
  [field F] [field L] [algebra F L] [is_galois F L]
  [finite_dimensional F L] (K : intermediate_field F L) :
  K.fixing_subgroup.normal ↔ ∀ (g : L ≃ₐ[F] L) (x : L), x ∈ K → g • x ∈ K :=
begin
  split,
  {
    intros hk_normal g x hxk,
    have hk_fixing := is_galois.fixed_field_fixing_subgroup K,
    rw ← hk_fixing,
    rw intermediate_field.fixed_field,
    rw fixed_points.intermediate_field,
    -- goal contains a structure explicitly made with `{ }` constructor
    dsimp, -- now it doesn't
    rintro ⟨φ, hφ⟩,
    -- tidy up goal
    change φ (g x) = g x,
    -- move g on RHS to LHS
    suffices : g⁻¹ (φ (g x)) = x,
    { -- inelegant proof
      apply_fun g at this,
      rw ← alg_equiv.mul_apply at this,
      simpa, },
    -- close approximation to the goal
    have := hk_normal.conj_mem φ hφ g⁻¹ ⟨x, hxk⟩,
    -- simplifier can reconcile `this` with the goal
    simpa,
  },
  { sorry,

  },
end

[Sean Gonzales]

Ah, dsimp is what I needed. Thanks!

[Kevin Buzzard]

I only put it there for psychological purposes. You can delete it and the proof still works. dsimp does definitional tidying up, but the change tactic works up to definitional equality too, so you don't need the dsimp at all.

[Sean Gonzales]

Right, I mean to say dsimp clarified the explicit construction to me.