Mathlib.FieldTheory.Normal.Basic

Normal.exists_isSplittingField theorem

[h : Normal F K] [FiniteDimensional F K] : ∃ p : F[X], IsSplittingField F K p

Full source

theorem Normal.exists_isSplittingField [h : Normal F K] [FiniteDimensional F K] :
    ∃ p : F[X], IsSplittingField F K p := by
  classical
  let s := Basis.ofVectorSpace F K
  refine
    ⟨∏ x, minpoly F (s x), splits_prod _ fun x _ => h.splits (s x),
      Subalgebra.toSubmodule.injective ?_⟩
  rw [Algebra.top_toSubmodule, eq_top_iff, ← s.span_eq, Submodule.span_le, Set.range_subset_iff]
  refine fun x =>
    Algebra.subset_adjoin
      (Multiset.mem_toFinset.mpr <|
        (mem_roots <|
              mt (Polynomial.map_eq_zero <| algebraMap F K).1 <|
                Finset.prod_ne_zero_iff.2 fun x _ => ?_).2 ?_)
  · exact minpoly.ne_zero (h.isIntegral (s x))
  rw [IsRoot.def, eval_map, ← aeval_def, map_prod]
  exact Finset.prod_eq_zero (Finset.mem_univ _) (minpoly.aeval _ _)

Existence of Splitting Field Polynomial for Finite-Dimensional Normal Extensions

Informal description

Let $K$ be a finite-dimensional normal field extension of $F$. Then there exists a polynomial $p \in F[X]$ such that $K$ is a splitting field of $p$ over $F$.

Normal.of_isSplittingField theorem

(p : F[X]) [hFEp : IsSplittingField F E p] : Normal F E

Full source

@[stacks 09HU "Normal part"]
theorem Normal.of_isSplittingField (p : F[X]) [hFEp : IsSplittingField F E p] : Normal F E := by
  rcases eq_or_ne p 0 with (rfl | hp)
  · have := hFEp.adjoin_rootSet
    rw [rootSet_zero, Algebra.adjoin_empty] at this
    exact Normal.of_algEquiv
      (AlgEquiv.ofBijective (Algebra.ofId F E) (Algebra.bijective_algebraMap_iff.2 this.symm))
  refine normal_iff.mpr fun x ↦ ?_
  haveI : FiniteDimensional F E := IsSplittingField.finiteDimensional E p
  have hx := IsIntegral.of_finite F x
  let L := (p * minpoly F x).SplittingField
  have hL := splits_of_splits_mul' _ ?_ (SplittingField.splits (p * minpoly F x))
  · let j : E →ₐ[F] L := IsSplittingField.lift E p hL.1
    refine ⟨hx, splits_of_comp _ (j : E →+* L) (j.comp_algebraMap ▸ hL.2) fun a ha ↦ ?_⟩
    rw [j.comp_algebraMap] at ha
    letI : Algebra F⟮x⟯ L := ((algHomAdjoinIntegralEquiv F hx).symm ⟨a, ha⟩).toRingHom.toAlgebra
    let j' : E →ₐ[F⟮x⟯] L := IsSplittingField.lift E (p.map (algebraMap F F⟮x⟯)) ?_
    · change a ∈ j.range
      rw [← IsSplittingField.adjoin_rootSet_eq_range E p j,
            IsSplittingField.adjoin_rootSet_eq_range E p (j'.restrictScalars F)]
      exact ⟨x, (j'.commutes _).trans (algHomAdjoinIntegralEquiv_symm_apply_gen F hx _)⟩
    · rw [splits_map_iff, ← IsScalarTower.algebraMap_eq]; exact hL.1
  · rw [Polynomial.map_ne_zero_iff (algebraMap F L).injective, mul_ne_zero_iff]
    exact ⟨hp, minpoly.ne_zero hx⟩

Splitting Field Implies Normal Extension

Informal description

Let $ F $ be a field and $ E $ a field extension of $ F $. If $ E $ is a splitting field of some polynomial $ p \in F[X] $, then the extension $ E/F $ is normal.

Polynomial.SplittingField.instNormal instance

(p : F[X]) : Normal F p.SplittingField

Full source

instance Polynomial.SplittingField.instNormal (p : F[X]) : Normal F p.SplittingField :=
  Normal.of_isSplittingField p

Splitting Fields are Normal Extensions

Informal description

For any field $F$ and polynomial $p \in F[X]$, the splitting field of $p$ over $F$ is a normal extension of $F$.

IntermediateField.normal_iSup instance

 {ι : Type*} (t : ι → IntermediateField F K) [h : ∀ i, Normal F (t i)] : Normal F (⨆ i, t i : IntermediateField F K)

Full source

/-- A compositum of normal extensions is normal. -/
instance normal_iSup {ι : Type*} (t : ι → IntermediateField F K) [h : ∀ i, Normal F (t i)] :
    Normal F (⨆ i, t i : IntermediateField F K) := by
  refine { toIsAlgebraic := isAlgebraic_iSup fun i => (h i).1, splits' := fun x => ?_ }
  obtain ⟨s, hx⟩ := exists_finset_of_mem_supr'' (fun i => (h i).1) x.2
  let E : IntermediateField F K := ⨆ i ∈ s, adjoin F ((minpoly F (i.2 :)).rootSet K)
  have hF : Normal F E := by
    haveI : IsSplittingField F E (∏ i ∈ s, minpoly F i.snd) := by
      refine isSplittingField_iSup ?_ fun i _ => adjoin_rootSet_isSplittingField ?_
      · exact Finset.prod_ne_zero_iff.mpr fun i _ => minpoly.ne_zero ((h i.1).isIntegral i.2)
      · exact Polynomial.splits_comp_of_splits _ (algebraMap (t i.1) K) ((h i.1).splits i.2)
    apply Normal.of_isSplittingField (∏ i ∈ s, minpoly F i.2)
  have hE : E ≤ ⨆ i, t i := by
    refine iSup_le fun i => iSup_le fun _ => le_iSup_of_le i.1 ?_
    rw [adjoin_le_iff, ← image_rootSet ((h i.1).splits i.2) (t i.1).val]
    exact fun _ ⟨a, _, h⟩ => h ▸ a.2
  have := hF.splits ⟨x, hx⟩
  rw [minpoly_eq, Subtype.coe_mk, ← minpoly_eq] at this
  exact Polynomial.splits_comp_of_splits _ (inclusion hE).toRingHom this

Normality of Compositum of Normal Extensions

Informal description

For any family of intermediate fields $\{t_i\}_{i \in \iota}$ between fields $F$ and $K$, if each $t_i$ is a normal extension of $F$, then their compositum $\bigsqcup_{i \in \iota} t_i$ is also a normal extension of $F$.

IntermediateField.splits_of_mem_adjoin theorem

 {L} [Field L] [Algebra F L] {S : Set K} (splits : ∀ x ∈ S, IsIntegral F x ∧ (minpoly F x).Splits (algebraMap F L))
  {x : K} (hx : x ∈ adjoin F S) : (minpoly F x).Splits (algebraMap F L)

Full source

/-- If a set of algebraic elements in a field extension `K/F` have minimal polynomials that
  split in another extension `L/F`, then all minimal polynomials in the intermediate field
  generated by the set also split in `L/F`. -/
@[stacks 0BR3 "first part"]
theorem splits_of_mem_adjoin {L} [Field L] [Algebra F L] {S : Set K}
    (splits : ∀ x ∈ S, IsIntegral F x ∧ (minpoly F x).Splits (algebraMap F L)) {x : K}
    (hx : x ∈ adjoin F S) : (minpoly F x).Splits (algebraMap F L) := by
  let E : IntermediateField F L := ⨆ x : S, adjoin F ((minpoly F x.val).rootSet L)
  have normal : Normal F E := normal_iSup (h := fun x ↦
    Normal.of_isSplittingField (hFEp := adjoin_rootSet_isSplittingField (splits x x.2).2))
  have : ∀ x ∈ S, (minpoly F x).Splits (algebraMap F E) := fun x hx ↦ splits_of_splits
    (splits x hx).2 fun y hy ↦ (le_iSup _ ⟨x, hx⟩ : _ ≤ E) (subset_adjoin F _ <| by exact hy)
  obtain ⟨φ⟩ := nonempty_algHom_adjoin_of_splits fun x hx ↦ ⟨(splits x hx).1, this x hx⟩
  convert splits_comp_of_splits _ E.val.toRingHom (normal.splits <| φ ⟨x, hx⟩)
  rw [minpoly.algHom_eq _ φ.injective, ← minpoly.algHom_eq _ (adjoin F S).val.injective, val_mk]

Splitting of Minimal Polynomials in Field Adjoin of Elements with Split Minimal Polynomials

Informal description

Let $F$ be a field and $K$ an extension field of $F$. Given a subset $S \subseteq K$ such that for every $x \in S$, $x$ is integral over $F$ and the minimal polynomial of $x$ over $F$ splits in some extension field $L$ of $F$, then for any element $x$ in the intermediate field $F(S)$ generated by $S$ over $F$, the minimal polynomial of $x$ over $F$ also splits in $L$.

IntermediateField.normal_sup instance

(E E' : IntermediateField F K) [Normal F E] [Normal F E'] : Normal F (E ⊔ E' : IntermediateField F K)

Full source

instance normal_sup
    (E E' : IntermediateField F K) [Normal F E] [Normal F E'] :
    Normal F (E ⊔ E' : IntermediateField F K) :=
  iSup_bool_eq (f := Bool.rec E' E) ▸ normal_iSup (h := by rintro (_|_) <;> infer_instance)

Normality of the Join of Normal Extensions

Informal description

For any intermediate fields $E$ and $E'$ between fields $F$ and $K$, if both $E$ and $E'$ are normal extensions of $F$, then their join $E \sqcup E'$ is also a normal extension of $F$.

IntermediateField.normal_iInf instance

 {ι : Type*} [hι : Nonempty ι] (t : ι → IntermediateField F K) [h : ∀ i, Normal F (t i)] :
  Normal F (⨅ i, t i : IntermediateField F K)

Full source

/-- An intersection of normal extensions is normal. -/
@[stacks 09HP]
instance normal_iInf {ι : Type*} [hι : Nonempty ι]
    (t : ι → IntermediateField F K) [h : ∀ i, Normal F (t i)] :
    Normal F (⨅ i, t i : IntermediateField F K) := by
  refine { toIsAlgebraic := ?_, splits' := fun x => ?_ }
  · let f := inclusion (iInf_le t hι.some)
    exact Algebra.IsAlgebraic.of_injective f f.injective
  · have hx : ∀ i, Splits (algebraMap F (t i)) (minpoly F x) := by
      intro i
      rw [← minpoly.algHom_eq (inclusion (iInf_le t i)) (inclusion (iInf_le t i)).injective]
      exact (h i).splits' (inclusion (iInf_le t i) x)
    simp only [splits_iff_mem (splits_of_isScalarTower K (hx hι.some))] at hx ⊢
    rintro y hy - ⟨-, ⟨i, rfl⟩, rfl⟩
    exact hx i y hy

Infimum of Normal Extensions is Normal

Informal description

For any nonempty index set $\iota$ and a family of intermediate fields $(t_i)_{i \in \iota}$ between fields $F$ and $K$, if each $t_i$ is a normal extension of $F$, then the infimum $\bigsqcap_i t_i$ is also a normal extension of $F$.

IntermediateField.normal_inf instance

(E E' : IntermediateField F K) [Normal F E] [Normal F E'] : Normal F (E ⊓ E' : IntermediateField F K)

Full source

@[stacks 09HP]
instance normal_inf
    (E E' : IntermediateField F K) [Normal F E] [Normal F E'] :
    Normal F (E ⊓ E' : IntermediateField F K) :=
  iInf_bool_eq (f := Bool.rec E' E) ▸ normal_iInf (h := by rintro (_|_) <;> infer_instance)

Intersection of Normal Extensions is Normal

Informal description

For any intermediate fields $ E $ and $ E' $ between fields $ F $ and $ K $, if both $ E $ and $ E' $ are normal extensions of $ F $, then their intersection $ E \sqcap E' $ is also a normal extension of $ F $.

AlgHom.fieldRange_of_normal theorem

{E : IntermediateField F K} [Normal F E] (f : E →ₐ[F] K) : f.fieldRange = E

Full source

theorem AlgHom.fieldRange_of_normal {E : IntermediateField F K} [Normal F E]
    (f : E →ₐ[F] K) : f.fieldRange = E := by
  let g := f.restrictNormal' E
  rw [← show E.val.comp ↑g = f from DFunLike.ext_iff.mpr (f.restrictNormal_commutes E),
    ← AlgHom.map_fieldRange, AlgEquiv.fieldRange_eq_top g, ← AlgHom.fieldRange_eq_map,
    IntermediateField.fieldRange_val]

Range of Algebra Homomorphism on Normal Extension Equals Itself

Informal description

Let $F$ be a field and $K$ a field extension of $F$. For any intermediate field $E$ between $F$ and $K$ that is normal over $F$, and any $F$-algebra homomorphism $f \colon E \to K$, the range of $f$ is equal to $E$ itself.

AlgHom.liftNormal definition

[h : Normal F E] : E →ₐ[F] E

Full source

/-- If `E/Kᵢ/F` are towers of fields with `E/F` normal then we can lift
  an algebra homomorphism `ϕ : K₁ →ₐ[F] K₂` to `ϕ.liftNormal E : E →ₐ[F] E`. -/
@[stacks 0BME "Part 2"]
noncomputable def AlgHom.liftNormal [h : Normal F E] : E →ₐ[F] E :=
  @AlgHom.restrictScalars F K₁ E E _ _ _ _ _ _
      ((IsScalarTower.toAlgHom F K₂ E).comp ϕ).toRingHom.toAlgebra _ _ _ _ <|
    Nonempty.some <|
      @IntermediateField.nonempty_algHom_of_adjoin_splits _ _ _ _ _ _ _
        ((IsScalarTower.toAlgHom F K₂ E).comp ϕ).toRingHom.toAlgebra _
        (fun x _ ↦ ⟨(h.out x).1.tower_top,
          splits_of_splits_of_dvd _ (map_ne_zero (minpoly.ne_zero (h.out x).1))
            -- Porting note: had to override typeclass inference below using `(_)`
            (by rw [splits_map_iff, ← @IsScalarTower.algebraMap_eq _ _ _ _ _ _ (_) (_) (_)]
                exact (h.out x).2)
            (minpoly.dvd_map_of_isScalarTower F K₁ x)⟩)
        (IntermediateField.adjoin_univ _ _)

Lift of algebra homomorphism to normal extension

Informal description

Given a tower of field extensions $ E/K_1/F $ with $ E/F $ normal, the function `AlgHom.liftNormal` lifts an algebra homomorphism $ \phi : K_1 \to K_2 $ to an algebra homomorphism $ \phi.\text{liftNormal} E : E \to E $ over $ F $. This is constructed by restricting scalars and using the fact that $ E $ is normal to ensure the extension exists.

AlgHom.liftNormal_commutes theorem

[Normal F E] (x : K₁) : ϕ.liftNormal E (algebraMap K₁ E x) = algebraMap K₂ E (ϕ x)

Full source

@[simp]
theorem AlgHom.liftNormal_commutes [Normal F E] (x : K₁) :
    ϕ.liftNormal E (algebraMap K₁ E x) = algebraMap K₂ E (ϕ x) :=
  -- Porting note: This seems to have been some sort of typeclass override trickery using `by apply`
  -- Now we explicitly specify which typeclass to override, using `(_)` instead of `_`
  @AlgHom.commutes K₁ E E _ _ _ _ (_) _ _

Commutativity of Lifted Homomorphism on Normal Extension

Informal description

Let $F$ be a field and $E$ a normal extension of $F$. Given an algebra homomorphism $\phi \colon K_1 \to K_2$ between intermediate fields $K_1$ and $K_2$ of $E/F$, and any element $x \in K_1$, the lifted homomorphism $\phi.\text{liftNormal}\, E$ satisfies \[ \phi.\text{liftNormal}\, E \big(\iota_{K_1 \to E}(x)\big) = \iota_{K_2 \to E}(\phi(x)), \] where $\iota_{K_i \to E}$ denotes the canonical inclusion map from $K_i$ to $E$.

AlgHom.restrict_liftNormal theorem

(ϕ : K₁ →ₐ[F] K₁) [Normal F K₁] [Normal F E] : (ϕ.liftNormal E).restrictNormal K₁ = ϕ

Full source

@[simp]
theorem AlgHom.restrict_liftNormal (ϕ : K₁ →ₐ[F] K₁) [Normal F K₁] [Normal F E] :
    (ϕ.liftNormal E).restrictNormal K₁ = ϕ :=
  AlgHom.ext fun x =>
    (algebraMap K₁ E).injective
      (Eq.trans (AlgHom.restrictNormal_commutes _ K₁ x) (ϕ.liftNormal_commutes E x))

Restriction of Lifted Homomorphism to Intermediate Normal Extension Equals Original Homomorphism

Informal description

Let $ F $ be a field and $ K_1 $, $ E $ be normal extensions of $ F $ with $ K_1 \subseteq E $. For any algebra homomorphism $ \phi \colon K_1 \to K_1 $ over $ F $, the restriction of the lifted homomorphism $ \phi.\text{liftNormal}\, E $ back to $ K_1 $ equals $ \phi $. In other words, \[ (\phi.\text{liftNormal}\, E)|_{K_1} = \phi. \]

AlgEquiv.liftNormal definition

[Normal F E] : E ≃ₐ[F] E

Full source

/-- If `E/Kᵢ/F` are towers of fields with `E/F` normal then we can lift
  an algebra isomorphism `ϕ : K₁ ≃ₐ[F] K₂` to `ϕ.liftNormal E : E ≃ₐ[F] E`. -/
noncomputable def AlgEquiv.liftNormal [Normal F E] : E ≃ₐ[F] E :=
  AlgEquiv.ofBijective (χ.toAlgHom.liftNormal E) (AlgHom.normal_bijective F E E _)

Lift of algebra isomorphism to normal extension

Informal description

Given a tower of field extensions $ E/K_1/F $ with $ E/F $ normal, the function `AlgEquiv.liftNormal` lifts an algebra isomorphism $ \chi : K_1 \simeq K_2 $ to an algebra isomorphism $ \chi.\text{liftNormal} E : E \simeq E $ over $ F $. This is constructed by restricting scalars and using the fact that $ E $ is normal to ensure the extension exists.

AlgEquiv.liftNormal_commutes theorem

[Normal F E] (x : K₁) : χ.liftNormal E (algebraMap K₁ E x) = algebraMap K₂ E (χ x)

Full source

@[simp]
theorem AlgEquiv.liftNormal_commutes [Normal F E] (x : K₁) :
    χ.liftNormal E (algebraMap K₁ E x) = algebraMap K₂ E (χ x) :=
  χ.toAlgHom.liftNormal_commutes E x

Commutativity of Lifted Isomorphism on Normal Extension

Informal description

Let $F$ be a field and $E$ a normal extension of $F$. Given an algebra isomorphism $\chi \colon K_1 \simeq K_2$ between intermediate fields $K_1$ and $K_2$ of $E/F$, and any element $x \in K_1$, the lifted isomorphism $\chi.\text{liftNormal}\, E$ satisfies \[ \chi.\text{liftNormal}\, E \big(\iota_{K_1 \to E}(x)\big) = \iota_{K_2 \to E}(\chi(x)), \] where $\iota_{K_i \to E}$ denotes the canonical inclusion map from $K_i$ to $E$.

AlgEquiv.restrict_liftNormal theorem

(χ : K₁ ≃ₐ[F] K₁) [Normal F K₁] [Normal F E] : (χ.liftNormal E).restrictNormal K₁ = χ

Full source

@[simp]
theorem AlgEquiv.restrict_liftNormal (χ : K₁ ≃ₐ[F] K₁) [Normal F K₁] [Normal F E] :
    (χ.liftNormal E).restrictNormal K₁ = χ :=
  AlgEquiv.ext fun x =>
    (algebraMap K₁ E).injective
      (Eq.trans (AlgEquiv.restrictNormal_commutes _ K₁ x) (χ.liftNormal_commutes E x))

Restriction of Lifted Automorphism to Intermediate Normal Extension Recovers Original Automorphism

Informal description

Let $ F $ be a field, $ K_1 $ and $ E $ be normal extensions of $ F $ with $ K_1 \subseteq E $. For any algebra automorphism $ \chi \colon K_1 \simeq K_1 $ over $ F $, the restriction of the lifted automorphism $ \chi.\text{liftNormal}\, E $ back to $ K_1 $ equals $ \chi $. In other words, the following diagram commutes: \[ \begin{tikzcd} E \arrow{r}{\chi.\text{liftNormal}\, E} & E \\ K_1 \arrow{u} \arrow{r}[swap]{\chi} & K_1 \arrow{u} \end{tikzcd} \] where the vertical maps are the canonical inclusions.

AlgEquiv.restrictNormalHom_surjective theorem

 [Normal F K₁] [Normal F E] : Function.Surjective (AlgEquiv.restrictNormalHom K₁ : (E ≃ₐ[F] E) → K₁ ≃ₐ[F] K₁)

Full source

/-- The group homomorphism given by restricting an algebra isomorphism to a normal subfield
is surjective. -/
theorem AlgEquiv.restrictNormalHom_surjective [Normal F K₁] [Normal F E] :
    Function.Surjective (AlgEquiv.restrictNormalHom K₁ : (E ≃ₐ[F] E) → K₁ ≃ₐ[F] K₁) := fun χ =>
  ⟨χ.liftNormal E, χ.restrict_liftNormal E⟩

Surjectivity of Restriction Homomorphism for Normal Field Extensions

Informal description

Let $ F $ be a field, and let $ K_1 $ and $ E $ be normal extensions of $ F $ with $ K_1 \subseteq E $. The restriction homomorphism \[ \text{AlgEquiv.restrictNormalHom}\, K_1 \colon \text{Aut}_F(E) \to \text{Aut}_F(K_1) \] is surjective, where $\text{Aut}_F(E)$ and $\text{Aut}_F(K_1)$ denote the groups of $F$-algebra automorphisms of $E$ and $K_1$ respectively. In other words, every $F$-algebra automorphism of $K_1$ can be extended to an $F$-algebra automorphism of $E$.

Normal.minpoly_eq_iff_mem_orbit theorem

[h : Normal F E] {x y : E} : minpoly F x = minpoly F y ↔ x ∈ MulAction.orbit (E ≃ₐ[F] E) y

Full source

theorem Normal.minpoly_eq_iff_mem_orbit [h : Normal F E] {x y : E} :
    minpolyminpoly F x = minpoly F y ↔ x ∈ MulAction.orbit (E ≃ₐ[F] E) y := by
  refine ⟨fun he ↦ ?_, fun ⟨f, he⟩ ↦ he ▸ minpoly.algEquiv_eq f y⟩
  obtain ⟨φ, hφ⟩ := exists_algHom_of_splits_of_aeval (normal_iff.mp h) (he ▸ minpoly.aeval F x)
  exact ⟨AlgEquiv.ofBijective φ (φ.normal_bijective F E E), hφ⟩

Minimal Polynomial Equality Characterizes Galois Orbits in Normal Extensions

Informal description

Let $E$ be a normal field extension of $F$. For any two elements $x, y \in E$, the minimal polynomial of $x$ over $F$ equals the minimal polynomial of $y$ over $F$ if and only if $x$ belongs to the orbit of $y$ under the action of the group of $F$-algebra automorphisms of $E$.

isSolvable_of_isScalarTower theorem

 [Normal F K₁] [h1 : IsSolvable (K₁ ≃ₐ[F] K₁)] [h2 : IsSolvable (E ≃ₐ[K₁] E)] : IsSolvable (E ≃ₐ[F] E)

Full source

theorem isSolvable_of_isScalarTower [Normal F K₁] [h1 : IsSolvable (K₁ ≃ₐ[F] K₁)]
    [h2 : IsSolvable (E ≃ₐ[K₁] E)] : IsSolvable (E ≃ₐ[F] E) := by
  let f : (E ≃ₐ[K₁] E) →* E ≃ₐ[F] E :=
    { toFun := fun ϕ =>
        AlgEquiv.ofAlgHom (ϕ.toAlgHom.restrictScalars F) (ϕ.symm.toAlgHom.restrictScalars F)
          (AlgHom.ext fun x => ϕ.apply_symm_apply x) (AlgHom.ext fun x => ϕ.symm_apply_apply x)
      map_one' := AlgEquiv.ext fun _ => rfl
      map_mul' := fun _ _ => AlgEquiv.ext fun _ => rfl }
  refine
    solvable_of_ker_le_range f (AlgEquiv.restrictNormalHom K₁) fun ϕ hϕ =>
      ⟨{ ϕ with commutes' := fun x => ?_ }, AlgEquiv.ext fun _ => rfl⟩
  exact Eq.trans (ϕ.restrictNormal_commutes K₁ x).symm (congr_arg _ (AlgEquiv.ext_iff.mp hϕ x))

Solvability of Automorphism Group in Field Extension Tower

Informal description

Let $ F \subseteq K_1 \subseteq E $ be a tower of field extensions where $ K_1 $ is a normal extension of $ F $. If the group of $ F $-algebra automorphisms of $ K_1 $ is solvable and the group of $ K_1 $-algebra automorphisms of $ E $ is solvable, then the group of $ F $-algebra automorphisms of $ E $ is also solvable.

minpoly.exists_algEquiv_of_root theorem

 [Normal K L] {x y : L} (hy : IsAlgebraic K y) (h_ev : (Polynomial.aeval x) (minpoly K y) = 0) :
  ∃ σ : L ≃ₐ[K] L, σ x = y

Full source

/-- If `x : L` is a root of `minpoly K y`, then we can find `(σ : L ≃ₐ[K] L)` with `σ x = y`.
  That is, `x` and `y` are Galois conjugates. -/
theorem exists_algEquiv_of_root [Normal K L] {x y : L} (hy : IsAlgebraic K y)
    (h_ev : (Polynomial.aeval x) (minpoly K y) = 0) : ∃ σ : L ≃ₐ[K] L, σ x = y := by
  have hx : IsAlgebraic K x := ⟨minpoly K y, ne_zero hy.isIntegral, h_ev⟩
  set f : K⟮x⟯ ≃ₐ[K] K⟮y⟯ := algEquiv hx (eq_of_root hy h_ev)
  have hxy : (liftNormal f L) ((algebraMap (↥K⟮x⟯) L) (AdjoinSimple.gen K x)) = y := by
    rw [liftNormal_commutes f L, algEquiv_apply, AdjoinSimple.algebraMap_gen K y]
  exact ⟨(liftNormal f L), hxy⟩

Existence of Galois Conjugates in Normal Extensions

Informal description

Let $ L $ be a normal field extension of $ K $. For any elements $ x, y \in L $ such that $ y $ is algebraic over $ K $ and $ x $ is a root of the minimal polynomial of $ y $ over $ K $, there exists a $ K $-algebra automorphism $ \sigma \colon L \to L $ such that $ \sigma(x) = y $.

minpoly.exists_algEquiv_of_root' theorem

 [Normal K L] {x y : L} (hy : IsAlgebraic K y) (h_ev : (Polynomial.aeval x) (minpoly K y) = 0) :
  ∃ σ : L ≃ₐ[K] L, σ y = x

Full source

/-- If `x : L` is a root of `minpoly K y`, then we can find `(σ : L ≃ₐ[K] L)` with `σ y = x`.
  That is, `x` and `y` are Galois conjugates. -/
theorem exists_algEquiv_of_root' [Normal K L] {x y : L} (hy : IsAlgebraic K y)
    (h_ev : (Polynomial.aeval x) (minpoly K y) = 0) : ∃ σ : L ≃ₐ[K] L, σ y = x := by
  obtain ⟨σ, hσ⟩ := exists_algEquiv_of_root hy h_ev
  use σ.symm
  rw [← hσ, symm_apply_apply]

Existence of Galois Conjugates in Normal Extensions (Symmetric Form)

Informal description

Let $L$ be a normal field extension of $K$. For any elements $x, y \in L$ such that $y$ is algebraic over $K$ and $x$ is a root of the minimal polynomial of $y$ over $K$, there exists a $K$-algebra automorphism $\sigma \colon L \to L$ such that $\sigma(y) = x$.

Algebra.IsQuadraticExtension.normal instance

(F K : Type*) [Field F] [Field K] [Algebra F K] [IsQuadraticExtension F K] : Normal F K

Full source

/--
A quadratic extension is normal.
-/
instance Algebra.IsQuadraticExtension.normal (F K : Type*) [Field F] [Field K] [Algebra F K]
    [IsQuadraticExtension F K] :
    Normal F K where
  splits' := by
    intro x
    obtain h | h := le_iff_lt_or_eq.mp (finrank_eq_two F K ▸ minpoly.natDegree_le x)
    · exact splits_of_natDegree_le_one _ (by rwa [Nat.le_iff_lt_add_one])
    · exact splits_of_natDegree_eq_two _ h (minpoly.aeval F x)

Normality of Quadratic Field Extensions

Informal description

For any field extension $ K $ of $ F $ that is quadratic (i.e., $ K $ is a free $ F $-algebra of rank 2), the extension $ K/F $ is normal. This means that every irreducible polynomial over $ F $ that has a root in $ K $ splits completely into linear factors in $ K $.

Additional Results