Normal Field Extension

Stream: general

[Maik Fücks]

Hello,

I am proving the Fundamental theorem of Algebra with Galoistheory and am a bit stuck on proving a certain extension is Galois (especially normal, separability is no problem): The setting is the following:

Let $E|\mathbb{C}$ be a finite dimensional extension and $\alpha$ the primitive Element such that $E = \mathbb{R}(\alpha).$
Now, let $f$ be the minpol of $\alpha$ over $\mathbb{R}$ and $L$ be the Splittingfield of $\alpha$ over $\mathbb{R}$.
What i want is, that then $L| \mathbb{C}$ is a finite dimensional, normal field extension aswell.
I already had some trouble proving that $L$ is an extension of $\mathbb{C}$ but composing RingHoms to get the Algebra Stucture worked. Now it looks like this

$$\mathbb{R} \hookrightarrow \mathbb{C} \hookrightarrow E \cong\mathbb{R}(\alpha) \cong\text{AdjoinRoot f }\hookrightarrow L$$

So this worked, but now im stuck trying to prove, that $L$ over $\mathbb{C}$ is a normal Field extension.
I tried two ways, first using 'Normal.of_isSplittingField' and the second using 'Normal.tower_top_of_normal'.
In both cases the problem seems to be, 'IsScalarTower $\mathbb{R}$ $\mathbb{C}$ $L$ ' doesnt hold, and i couldnt prove it (and im not sure its even possible), because my $L$ over $\mathbb{R}$ extension is "abstract" in some sense ($L$ is the splitting field of $f$ over $\mathbb{R}$) and my $L$ over $\mathbb{C}$ extension is constructed, and i dont think the composition of $L| \mathbb{C}$ and $\mathbb{C}| \mathbb{R}$ is equal to my abstract extension $L| \mathbb{R}$ .
Does anyone have an idea how to get around here? Gladly appreciate some thoughts!
Kind Regards,
Maik

P.s.: Is there a better way to mix latex with normal text? (fixed :=))

[Mauricio Collares]

You can use double dollar signs (instead of single dollar signs as usual) for inline LaTeX: $1+2=3$ (click on the three dots next to the message timestamp and then on "View original message" to view its source)

[Thomas Browning]

You can try to prove IsScalarTower by using docs#IsScalarTower.of_algHom or docs#IsScalarTower.of_algebraMap_eq

[Kevin Buzzard]

Yes I would expect the IsScalarTower claim to be true -- if it's not then a fundamental diagram doesn't commute, which shouldn't happen.

[Kevin Buzzard]

And the best way to ask a question here, especially a technical question of this nature, is to post a #mwe .

[Maik Fücks]

Hello, sorry for the kindof late response, i had no time to work on the project previous week. Here is a (not so small) minimal working example:

import Mathlib.Algebra.Field.Basic
import Mathlib.Analysis.SpecialFunctions.PolarCoord
import Mathlib.FieldTheory.SeparableClosure
import Mathlib.RingTheory.IsAdjoinRoot


/-Preamble-/
open Module FiniteDimensional Polynomial

theorem complex_fin_ext_finrank_eq_one (L' : Type) [Field L'] [Algebra ℂ L'] [FiniteDimensional ℂ L'] : finrank ℂ L' = 1 := by
  /-Asssume negation for contradiction-/
  by_contra hrankn1; push_neg at hrankn1
/-Know that for finite dimensional, finrank > 0-/
  have hfrpos : 0 < finrank ℂ L' := finrank_pos
/-Use primitive Element theorem to get α ∈ L' with L' = ℝ(α) -/
  obtain ⟨α,hα⟩ := Field.exists_primitive_element ℝ L'
/-α is integral-/
  have hα₁ : IsIntegral ℝ α := by exact Algebra.IsIntegral.isIntegral α
/-Let f be the minimal polynomial of α OVER THE REALS ℝ! -/
  let f := minpoly ℝ α
/-Now let L be the splitting field of f-/
  let L := SplittingField f
/-It is a Galois extension of ℝ-/
  have hLgal : IsGalois ℝ L := by exact IsGalois.mk
/-Now we wish to show, that L|ℂ is a Galois Extension too, but lean fails to synthesize 'Algebra ℂ L'-/
/-So first of all we need to construct a term of type Algebra C L -/
/-Prove that ℝ(α) is isomorphic to L' by defining an isomorphism-/
  let iso₁ : (IntermediateField.adjoin ℝ {α}) ≃ₐ[ℝ] L' := by
    rw[hα]; exact IntermediateField.topEquiv
/-Then, prove that ℝ(α) is isomorphic to the field 'AdjoinRoot f', which basically says that no matter which root of f you adjoin,
  all those fields are isomorphic-/
  let iso₂ : (AdjoinRoot f) ≃ₐ[ℝ] (IntermediateField.adjoin ℝ {α}) := IntermediateField.adjoinRootEquivAdjoin ℝ hα₁
/-Composing both isomorphisms, we get an isomorphism from AdjoinRoot f to L' -/
  let iso : ((AdjoinRoot f) ≃ₐ[ℝ] L') := by exact ((id iso₁.symm).trans (id iso₂.symm)).symm
/-AdjoinRoot Ring can be 'lifted', i.e. embedded into another Ring, in which
  the polynomial has a root. Hence now we need to show, that under the embedding from ℝ to L, the polynomial f has a root γ in L-/
  have hγ : ∃ (γ : L), eval₂ (algebraMap ℝ L) γ f = 0 := by
  /-First, we need that deg f ≠ 0-/
    have hdegf : f.degree ≠ 0 := by
      by_contra hdeg0
      have hdegpos := degree_pos_of_irreducible (minpoly.irreducible hα₁)
      rw[hdeg0] at hdegpos
      simp at hdegpos
  /-Now we choose β : L which is a root of f in L. Such a root exists, because L is the splitting Field-/
    let β := rootOfSplits (algebraMap ℝ L) (SplittingField.splits f) hdegf
  /-This is the root we want.-/
    use β
  /-Beta does what what it should (being a root of f)-/
    exact map_rootOfSplits (algebraMap ℝ L) (SplittingField.splits f) hdegf
  obtain ⟨γ,hγ⟩ := hγ
/-Now that this is done, we can lift adjoinRoot f into L, to get and extension L|(AdjoinRoot f)-/
  let hadjL : Algebra (AdjoinRoot f) L := RingHom.toAlgebra (AdjoinRoot.lift (algebraMap ℝ L) γ hγ )
/-Now since Field extensions correspond to RingHoms and we have the Ringhomo from adj f to L and the isomorphism from L' to adj f, we can compose them
  to obtain a RingHom from L' to L, hence L is an L' Algebra, meaning L extends the Field L'-/
  let hL'L : Algebra L' L := ((algebraMap (AdjoinRoot f) L).comp (RingEquiv.toRingHom iso.symm)).toAlgebra
/-Hence finally L over ℂ is also a Field extension-/
  let hCL :=  ((algebraMap L' L).comp  (algebraMap ℂ L')).toAlgebra
/-Now we need that L|ℂ is normal, since separability is trivial. But this needs 'IsScalarTower ℝ ℂ L'-/
  have hsct : IsScalarTower ℝ ℂ L := by sorry
  have hCLnorm : Normal ℂ L := Normal.tower_top_of_normal ℝ ℂ L
  have hCLsep : Algebra.IsSeparable ℂ L := by exact Algebra.IsSeparable.of_integral ℂ L
  have hCLgal : IsGalois ℂ L := by exact IsGalois.mk


/-Irrelevant from here-/
  sorry

While i agree with both of you, i just dont see how to obtain the ScalarTower, since i dont see how algebraMap $\mathbb R$ $L$ given by the Splitting field coincides with the composition of algebraMap $\mathbb R$ $\mathbb C$ and algebraMap $\mathbb C$ $L$.
Thanks for your support!

[Kevin Buzzard]

One thing that jumps out immediately is that you say things like "So we show Algebra ℂ L first" but this is not a theorem which you show in Lean, this is data which you supply. In particular all the stuff near the end like have hadjL : Algebra (AdjoinRoot f) L :=... -- all those haves should be lets because you are making a definition, not proving a theorem.

[Kevin Buzzard]

This is also the case for your isomorphisms: a term of type(IntermediateField.adjoin ℝ {α}) ≃ₐ[ℝ] L' does not mean "these fields are isomorphic as R-algebras", it means "this is an isomorphism of R-algebras" so all the have hiso₁ : (IntermediateField.adjoin ℝ {α}) ≃ₐ[ℝ] L' := by... should be lets as well.

To a first approximation, Lean has two universes: Prop (the universe of true/false statements and their proofs) and Type (the universe of sets and elements). You use have for proofs in the Prop universe and let for the data in the Type universe.

[Maik Fücks]

Thanks for the advice! While i was aware of the distinction between have/let and prop/type it wasnt so clear in my mind and i mixed them up quite frequently, because i didnt notice any practically significant difference. I edited my mwe accordingly.

[Kevin Buzzard]

Re the have/let thing: I just want to mention that your comments like "Then, prove that ℝ(α) is isomorphic to the field AdjoinRoot f" are not quite representing the Lean code -- the comment should be something like "Then, let iso₂ be an isomorphism ...". I'm only flagging this because it's a common source of confusion for beginners. The difference is that have will construct the isomorphism and then immediately forget its definition (Lean forgets proofs, just remembering instead that the theorem is true, but you don't want to forget definitions because then you can't prove things about your definitions).

Now I had hoped that after changing the haves to lets then everything would be automatic, but it seems that still some work needs to be done. I took a look at this on the tube home and my first instinct is that you are losing information with let hadjL : Algebra (AdjoinRoot f) L := RingHom.toAlgebra (AdjoinRoot.lift (algebraMap ℝ L) γ hγ ) because AdjoinRoot.lift is a ring homomorphism rather than an $\R$-algebra homomorphism. If you knew it was an $\R$-algebra homomorphism then you get IsScalarTower \R (AdjoinRoot f) L for free, and because iso is also an $\R$-algebra hom you should get IsScalarTower \R L' L for free. Now IsScalarTower \R \C L' is true, and because IsScalarTower \C L' L is also true you win.

It's certainly true though that Lean is making this proof hard to formalise.

[Kevin Buzzard]

Oh, another thing which might make your life easier is this change:

  let hiso₁ : (IntermediateField.adjoin ℝ {α}) ≃ₐ[ℝ] L' :=
    (IntermediateField.equivOfEq hα).trans IntermediateField.topEquiv

Because you're constructing data here, not proving something, you shouldn't use tactics like rw (tactics are for proofs, they can generate ugly terms, which is not a problem in a proof but is a problem if you're using them to make definitions which you'll need to prove theorems about later).

[Maik Fücks]

Dear Kevin,
Many thanks for your much appreciated advise and effort! I will ponder over your words tomorrow, since i am too tired now. But they do shine some light on my situation already and took away a good portion of some growing frustration!

[Kevin Buzzard]

Other golfs/tricks: by_contra hrankn1; push_neg at hrankn1 -> by_contra! hrankn1 (by_contra + push_neg is a common idiom so there's a shortcut). And by exact can often be deleted: by means "switch from term mode to tactic mode" and exact means "switch from tactic mode to term mode".

[Maik Fücks]

Kevin Buzzard schrieb:

Re the have/let thing: I just want to mention that your comments like "Then, prove that ℝ(α) is isomorphic to the field AdjoinRoot f" are not quite representing the Lean code -- the comment should be something like "Then, let iso₂ be an isomorphism ...". I'm only flagging this because it's a common source of confusion for beginners. The difference is that have will construct the isomorphism and then immediately forget its definition (Lean forgets proofs, just remembering instead that the theorem is true, but you don't want to forget definitions because then you can't prove things about your definitions).

Now I had hoped that after changing the haves to lets then everything would be automatic, but it seems that still some work needs to be done. I took a look at this on the tube home and my first instinct is that you are losing information with let hadjL : Algebra (AdjoinRoot f) L := RingHom.toAlgebra (AdjoinRoot.lift (algebraMap ℝ L) γ hγ ) because AdjoinRoot.lift is a ring homomorphism rather than an $\R$-algebra homomorphism. If you knew it was an $\R$-algebra homomorphism then you get IsScalarTower \R (AdjoinRoot f) L for free, and because iso is also an $\R$-algebra hom you should get IsScalarTower \R L' L for free. Now IsScalarTower \R \C L' is true, and because IsScalarTower \C L' L is also true you win.

It's certainly true though that Lean is making this proof hard to formalise.

So i have tried this and i think i am still stuck on the same issue: The implicit SMul arguments of IsScalarTower are different; for one, there are the SMuls comming from the algebra structures, and then there are the SMuls comming from the Splittingfield. Everything i tried so far always failed at this detail, that there are two instances of SMul which i can't bring together. For example, following your advice, if we have an $\R$-Algebra hom from AdjoinRoot fto L, this does not give me the correct IsScalarTower \R AdjoinRoot f L proposition, because the implict SMul arguments differ. Same problem with the SMul instance induced byAdjoinRoot f. Here is a typical Errormessage:

type mismatch
  IsScalarTower.of_algHom ψadjL
has type
  @IsScalarTower ℝ (AdjoinRoot f) L Algebra.toSMul
    (@Algebra.toSMul (AdjoinRoot f) L CommRing.toCommSemiring CommSemiring.toSemiring ψadjL.toAlgebra)
    Algebra.toSMul : Prop
but is expected to have type
  @IsScalarTower ℝ (AdjoinRoot f) L (AdjoinRoot.instSMulAdjoinRoot f)
    (@Algebra.toSMul (AdjoinRoot f) L CommRing.toCommSemiring DivisionSemiring.toSemiring φadjL)
    (SplittingField.instSMulOfIsScalarTower f) : Prop

[Kevin Buzzard]

I think you need to keep track of the fact that everything is an $\R$-algebra (i.e. use AdjoinRoot.liftHom instead of AdjoinRoot.lift). This approach

  obtain ⟨γ,hγ⟩ := hγ
/-Now that this is done, we can lift adjoinRoot f into L, to get and extension L|(AdjoinRoot f)-/
  let foo2 : AdjoinRoot f →ₐ[ℝ] L := AdjoinRoot.liftHom f γ hγ
  let foo3 : L' →ₐ[ℝ] L := foo2.comp hiso.symm.toAlgHom
  let hL'L : Algebra L' L := RingHom.toAlgebra foo3
  have foo4 : IsScalarTower ℝ L' L :=
    IsScalarTower.of_algebraMap_eq <| IsScalarTower.algebraMap_apply ℝ L' L
/-Hence finally L over ℂ is also a Field extension-/
  let hCL : Algebra ℂ L :=  ((algebraMap L' L).comp  (algebraMap ℂ L')).toAlgebra
  have foo5 : IsScalarTower ℂ L' L := IsScalarTower.of_algebraMap_eq <| fun x ↦ rfl
  have foo6 : IsScalarTower ℝ ℂ L' := IsScalarTower.of_algebraMap_eq <| fun x ↦ rfl
  have hsct : IsScalarTower ℝ ℂ L := sorry -- a formal consequence of foo4, foo5 and foo6

seems to work, and IsScalarTower ℝ ℂ L should now be a formal consequence.

[Kevin Buzzard]

import Mathlib.Analysis.SpecialFunctions.PolarCoord
import Mathlib.FieldTheory.SeparableClosure

set_option linter.style.longLine false
/-Preamble-/
open FiniteDimensional Polynomial


theorem isScalarTower_iff_algebraMap_eq {K L M : Type*} [CommSemiring K] [CommSemiring L] [Semiring M]
    [Algebra K L] [Algebra L M] [Algebra K M] :
    IsScalarTower K L M ↔ ∀ (k : K), algebraMap K M k = algebraMap L M (algebraMap K L k) := by
  constructor
  · rintro ⟨h⟩
    intro k
    simp [Algebra.algebraMap_eq_smul_one, h]
  · intro h
    exact IsScalarTower.of_algebraMap_eq h

theorem isScalarTower_of_isScalarTower_of_IsScalarTower_of_IsScalarTower
    (A B C D : Type*) [CommSemiring A] [CommSemiring B] [CommSemiring C] [CommSemiring D]
    [Algebra A B] [Algebra A C] [Algebra A D] [Algebra B C] [Algebra B D] [Algebra C D]
    [h1 : IsScalarTower A B C] [h2 : IsScalarTower A C D] [h3 : IsScalarTower B C D] : IsScalarTower A B D := by
  rw [isScalarTower_iff_algebraMap_eq]
  intro a
  rw [isScalarTower_iff_algebraMap_eq.1 h3, isScalarTower_iff_algebraMap_eq.1 h2, isScalarTower_iff_algebraMap_eq.1 h1]

theorem complex_fin_ext_finrank_eq_one (L' : Type) [Field L'] [Algebra ℂ L'] [FiniteDimensional ℂ L'] : finrank ℂ L' = 1 := by
  /-Asssume negation for contradiction-/
  by_contra! hrankn1;
/-Know that for finite dimensional, finrank > 0-/
  have hfrpos : 0 < finrank ℂ L' := finrank_pos
/-Use primitive Element theorem to get α ∈ L' with L' = ℝ(α) -/
  obtain ⟨α,hα⟩ := Field.exists_primitive_element ℝ L'
/-α is integral-/
  have hα₁ : IsIntegral ℝ α := Algebra.IsIntegral.isIntegral α
/-Let f be the minimal polynomial of α OVER THE REALS ℝ! -/
  let f := minpoly ℝ α
/-Now let L be the splitting field of f-/
  let L := SplittingField f
/-It is a Galois extension of ℝ-/
  have hLgal : IsGalois ℝ L := IsGalois.mk
/-Now we wish to show, that L|ℂ is a Galois Extension too, but lean fails to synthesize 'Algebra ℂ L'-/
/-So we show Algebra ℂ L first:-/
/-Prove that ℝ(α) is isomorphic to L'-/
  let hiso₁ : (IntermediateField.adjoin ℝ {α}) ≃ₐ[ℝ] L' :=
    (IntermediateField.equivOfEq hα).trans IntermediateField.topEquiv
/-Then, prove that ℝ(α) is isomorphic to the field 'AdjoinRoot f', which basically says that no matter which root of f you adjoin,
  all those fields are isomorphic-/
  let hiso₂ : (AdjoinRoot f) ≃ₐ[ℝ] (IntermediateField.adjoin ℝ {α}) := IntermediateField.adjoinRootEquivAdjoin ℝ hα₁
/-Composing both isomorphisms, we get that AdjoinRoot f is isomorphic to L'-/
  let hiso : ((AdjoinRoot f) ≃ₐ[ℝ] L') := hiso₂.trans hiso₁
/-AdjoinRoot Ring can be 'lifted', i.e. embedded into another Ring, in which
  the polynomial has a root. Hence now we need to show, that under the embedding from ℝ to L, the polynomial f has a root γ in L-/
  have hγ : ∃ (γ : L), eval₂ (algebraMap ℝ L) γ f = 0 := by
  /-First, we need that deg f ≠ 0-/
    have hdegf : f.degree ≠ 0 := by
      by_contra hdeg0
      have hdegpos := degree_pos_of_irreducible (minpoly.irreducible hα₁)
      rw[hdeg0] at hdegpos
      simp at hdegpos
  /-Now we choose β : L which is a root of f in L. Such a root exists, because L is the splitting Field-/
    let β := rootOfSplits (algebraMap ℝ L) (SplittingField.splits f) hdegf
  /-This is the root we want.-/
    use β
  /-Beta does what what it should (being a root of f)-/
    exact map_rootOfSplits (algebraMap ℝ L) (SplittingField.splits f) hdegf
  obtain ⟨γ,hγ⟩ := hγ
/-Now that this is done, we can lift adjoinRoot f into L, to get and extension L|(AdjoinRoot f)-/
  let foo2 : AdjoinRoot f →ₐ[ℝ] L := AdjoinRoot.liftHom f γ hγ
  let foo3 : L' →ₐ[ℝ] L := foo2.comp hiso.symm.toAlgHom
  let hL'L : Algebra L' L := RingHom.toAlgebra foo3
  have foo4 : IsScalarTower ℝ L' L :=
    IsScalarTower.of_algebraMap_eq <| IsScalarTower.algebraMap_apply ℝ L' L
/-Hence finally L over ℂ is also a Field extension-/
  let hCL : Algebra ℂ L :=  ((algebraMap L' L).comp  (algebraMap ℂ L')).toAlgebra
  have foo5 : IsScalarTower ℂ L' L := IsScalarTower.of_algebraMap_eq <| fun x ↦ rfl
  have foo6 : IsScalarTower ℝ ℂ L' := IsScalarTower.of_algebraMap_eq <| fun x ↦ rfl
  have hsct : IsScalarTower ℝ ℂ L := isScalarTower_of_isScalarTower_of_IsScalarTower_of_IsScalarTower ℝ ℂ L' L
/-Now we need that L|ℂ is normal, since separability is trivial. But this needs 'IsScalarTower ℝ ℂ L'-/
  have hCLnorm : Normal ℂ L := Normal.tower_top_of_normal ℝ ℂ L
  have hCLsep : Algebra.IsSeparable ℂ L := by exact Algebra.IsSeparable.of_integral ℂ L
  have hCLgal : IsGalois ℂ L := by exact IsGalois.mk


/-Irrelevant from here-/
  sorry

[Maik Fücks]

/-Now that this is done, we can lift adjoinRoot f into L, to get an extension L|(AdjoinRoot f).
  THIS IS IMPORTANT: Using AdjoinRoot.lift was the main problem, since this only gives a Ringhom as embedding, and therefore
  "looses" the information, that infact it it as ℝ-Algebrahom from AdjoinRoot f to L.
  AdjoinRoot.liftHom fixes the problem, by keeping the ℝ-Algebra Information, hence we can build ScalarTowers from the AlgebraHoms later on:
-/
  let ψadjL : (AdjoinRoot f) →ₐ[ℝ] L :=  (AdjoinRoot.liftHom f γ hγ )
/-Here too, we not only say L is an L'-Algebra, meaning there is a Ringhom from L' to L, but we say that there exists an ℝ-Algebrahom from
  L' to L. This again keeps vital information to build the necessary scalartowers later on.
   -/
  let ψL'L :  L'  →ₐ[ℝ] L := ψadjL.comp iso.symm
/-But ofc it is also an Algebra-/
  let hL'l : Algebra L' L := RingHom.toAlgebra ψL'L
/-The following can also just be inferred now. It says, that the SMul of the ℝ-Algebra L is compatible with the SMuls of the ℝ-Algebra L'
  and the L'-Algebra L-/
  have hRL'L : IsScalarTower ℝ L' L := IsScalarTower.of_algebraMap_eq (IsScalarTower.algebraMap_apply ℝ L' L)
/-Composing the Ringhoms corresponding to the extnsions L'|ℂ and L|L' yields a Ringhom from ℂ to L, i.e. an Extension L|ℂ-/
  let hCL : Algebra ℂ L :=  ((algebraMap L' L).comp  (algebraMap ℂ L')).toAlgebra
/-Now we also have the desired ScalarTower properties, which were missing before:-/
  have hRCL' : IsScalarTower ℝ ℂ L' := IsScalarTower.of_algebraMap_eq (λ x ↦ rfl)
/-This is the crucial ScalarTower we need for 'Normal.tower_top_of_normal ℝ ℂ L'. We obtain it now, by composing Algebra Homomorphisms
  which we now have at hand, compared to before where we only had Ringhoms-/
  have hsct : IsScalarTower ℝ ℂ L := IsScalarTower.of_algHom ((IsScalarTower.toAlgHom ℝ L' L).comp (IsScalarTower.toAlgHom ℝ ℂ L'))
/-Now we need that L|ℂ is normal, since separability is trivial. But this needs 'IsScalarTower ℝ ℂ L'-/
  have hCLnorm : Normal ℂ L := Normal.tower_top_of_normal ℝ ℂ L
  have hCLsep : Algebra.IsSeparable ℂ L := Algebra.IsSeparable.of_integral ℂ L
  have hCLgal : IsGalois ℂ L := IsGalois.mk

Fantastic! It worked! Also, one doesnt even need have foo5 : IsScalarTower ℂ L' L := IsScalarTower.of_algebraMap_eq <| fun x ↦ rfl
Thank you so much for your invaluable help!

[Kevin Buzzard]

Thanks for asking a clear and coherent question in an area of interest to me.