Documentation

Mathlib.FieldTheory.Normal.Basic

Normal field extensions #

In this file we prove that for a finite extension, being normal is the same as being a splitting field (Normal.of_isSplittingField and Normal.exists_isSplittingField).

Additional Results #

source
theorem Normal.exists_isSplittingField (F : Type u_1) (K : Type u_2) [Field F] [Field K] [Algebra F K] [h : Normal F K] [FiniteDimensional F K] :
∃ (p : Polynomial F), Polynomial.IsSplittingField F K p
source
theorem Normal.of_isSplittingField {F : Type u_1} [Field F] {E : Type u_3} [Field E] [Algebra F E] (p : Polynomial F) [hFEp : Polynomial.IsSplittingField F E p] :
Normal F E

Stacks Tag 09HU (Normal part)

source
instance Polynomial.SplittingField.instNormal {F : Type u_1} [Field F] (p : Polynomial F) :
Normal F p.SplittingField
source
instance IntermediateField.normal_iSup (F : Type u_1) (K : Type u_2) [Field F] [Field K] [Algebra F K] {ι : Type u_3} (t : ι → IntermediateField F K) [h : ∀ (i : ι), Normal F ↥(t i)] :
Normal F ↥(⨆ (i : ι), t i)

A compositum of normal extensions is normal.

source
theorem IntermediateField.splits_of_mem_adjoin (F : Type u_1) (K : Type u_2) [Field F] [Field K] [Algebra F K] {L : Type u_3} [Field L] [Algebra F L] {S : Set K} (splits : ∀ x ∈ S, IsIntegral F x ∧ Polynomial.Splits (algebraMap F L) (minpoly F x)) {x : K} (hx : x ∈ adjoin F S) :
Polynomial.Splits (algebraMap F L) (minpoly F x)

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.

source
instance IntermediateField.normal_sup (F : Type u_1) (K : Type u_2) [Field F] [Field K] [Algebra F K] (E E' : IntermediateField F K) [Normal F ↥E] [Normal F ↥E'] :
Normal F ↥(E ⊔ E')
source
instance IntermediateField.normal_iInf (F : Type u_1) (K : Type u_2) [Field F] [Field K] [Algebra F K] {ι : Type u_3} [hι : Nonempty ι] (t : ι → IntermediateField F K) [h : ∀ (i : ι), Normal F ↥(t i)] :
Normal F ↥(⨅ (i : ι), t i)

An intersection of normal extensions is normal.

source
instance IntermediateField.normal_inf (F : Type u_1) (K : Type u_2) [Field F] [Field K] [Algebra F K] (E E' : IntermediateField F K) [Normal F ↥E] [Normal F ↥E'] :
Normal F ↥(E ⊓ E')

Stacks Tag 09HP

source
theorem AlgHom.fieldRange_of_normal {F : Type u_1} {K : Type u_2} [Field F] [Field K] [Algebra F K] {E : IntermediateField F K} [Normal F ↥E] (f : ↥E →ₐ[F] K) :
f.fieldRange = E
source
noncomputable def AlgHom.liftNormal {F : Type u_1} [Field F] {K₁ : Type u_3} {K₂ : Type u_4} [Field K₁] [Field K₂] [Algebra F K₁] [Algebra F K₂] (ϕ : K₁ →ₐ[F] K₂) (E : Type u_6) [Field E] [Algebra F E] [Algebra K₁ E] [Algebra K₂ E] [IsScalarTower F K₁ E] [IsScalarTower F K₂ E] [h : Normal F E] :
E →ₐ[F] E

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.

Equations
Instances For
    source
    @[simp]
    theorem AlgHom.liftNormal_commutes {F : Type u_1} [Field F] {K₁ : Type u_3} {K₂ : Type u_4} [Field K₁] [Field K₂] [Algebra F K₁] [Algebra F K₂] (ϕ : K₁ →ₐ[F] K₂) (E : Type u_6) [Field E] [Algebra F E] [Algebra K₁ E] [Algebra K₂ E] [IsScalarTower F K₁ E] [IsScalarTower F K₂ E] [Normal F E] (x : K₁) :
    (ϕ.liftNormal E) ((algebraMap K₁ E) x) = (algebraMap K₂ E) (ϕ x)
    source
    @[simp]
    theorem AlgHom.restrict_liftNormal {F : Type u_1} [Field F] {K₁ : Type u_3} [Field K₁] [Algebra F K₁] (E : Type u_6) [Field E] [Algebra F E] [Algebra K₁ E] [IsScalarTower F K₁ E] (ϕ : K₁ →ₐ[F] K₁) [Normal F K₁] [Normal F E] :
    (ϕ.liftNormal E).restrictNormal K₁ = ϕ
    source
    noncomputable def AlgEquiv.liftNormal {F : Type u_1} [Field F] {K₁ : Type u_3} {K₂ : Type u_4} [Field K₁] [Field K₂] [Algebra F K₁] [Algebra F K₂] (χ : K₁ ≃ₐ[F] K₂) (E : Type u_6) [Field E] [Algebra F E] [Algebra K₁ E] [Algebra K₂ E] [IsScalarTower F K₁ E] [IsScalarTower F K₂ E] [Normal F E] :
    E ≃ₐ[F] E

    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.

    Equations
    Instances For
      source
      @[simp]
      theorem AlgEquiv.liftNormal_commutes {F : Type u_1} [Field F] {K₁ : Type u_3} {K₂ : Type u_4} [Field K₁] [Field K₂] [Algebra F K₁] [Algebra F K₂] (χ : K₁ ≃ₐ[F] K₂) (E : Type u_6) [Field E] [Algebra F E] [Algebra K₁ E] [Algebra K₂ E] [IsScalarTower F K₁ E] [IsScalarTower F K₂ E] [Normal F E] (x : K₁) :
      (χ.liftNormal E) ((algebraMap K₁ E) x) = (algebraMap K₂ E) (χ x)
      source
      @[simp]
      theorem AlgEquiv.restrict_liftNormal {F : Type u_1} [Field F] {K₁ : Type u_3} [Field K₁] [Algebra F K₁] (E : Type u_6) [Field E] [Algebra F E] [Algebra K₁ E] [IsScalarTower F K₁ E] (χ : K₁ ≃ₐ[F] K₁) [Normal F K₁] [Normal F E] :
      (χ.liftNormal E).restrictNormal K₁ = χ
      source
      theorem AlgEquiv.restrictNormalHom_surjective {F : Type u_1} [Field F] {K₁ : Type u_3} [Field K₁] [Algebra F K₁] (E : Type u_6) [Field E] [Algebra F E] [Algebra K₁ E] [IsScalarTower F K₁ E] [Normal F K₁] [Normal F E] :
      Function.Surjective ⇑(restrictNormalHom K₁)

      The group homomorphism given by restricting an algebra isomorphism to a normal subfield is surjective.

      source
      theorem Normal.minpoly_eq_iff_mem_orbit {F : Type u_1} [Field F] (E : Type u_6) [Field E] [Algebra F E] [h : Normal F E] {x y : E} :
      minpoly F x = minpoly F y ↔ x ∈ MulAction.orbit (E ≃ₐ[F] E) y
      source
      theorem isSolvable_of_isScalarTower (F : Type u_1) [Field F] (K₁ : Type u_3) [Field K₁] [Algebra F K₁] (E : Type u_6) [Field E] [Algebra F E] [Algebra K₁ E] [IsScalarTower F K₁ E] [Normal F K₁] [h1 : IsSolvable (K₁ ≃ₐ[F] K₁)] [h2 : IsSolvable (E ≃ₐ[K₁] E)] :
      IsSolvable (E ≃ₐ[F] E)
      source
      theorem minpoly.exists_algEquiv_of_root {K : Type u_6} {L : Type u_7} [Field K] [Field L] [Algebra K L] [Normal K L] {x y : L} (hy : IsAlgebraic K y) (h_ev : (Polynomial.aeval x) (minpoly K y) = 0) :
      ∃ (σ : L ≃ₐ[K] L), σ x = y

      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.

      source
      theorem minpoly.exists_algEquiv_of_root' {K : Type u_6} {L : Type u_7} [Field K] [Field L] [Algebra K L] [Normal K L] {x y : L} (hy : IsAlgebraic K y) (h_ev : (Polynomial.aeval x) (minpoly K y) = 0) :
      ∃ (σ : L ≃ₐ[K] L), σ y = x

      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.

      source
      instance Algebra.IsQuadraticExtension.normal (F : Type u_6) (K : Type u_7) [Field F] [Field K] [Algebra F K] [IsQuadraticExtension F K] :
      Normal F K

      A quadratic extension is normal.

      source
      @[deprecated Algebra.IsQuadraticExtension.normal (since := "2025-04-17")]
      theorem normal_of_finrank_eq_two (F : Type u_6) (K : Type u_7) [Field F] [Field K] [Algebra F K] [Algebra.IsQuadraticExtension F K] :
      Normal F K

      Alias of Algebra.IsQuadraticExtension.normal.

      A quadratic extension is normal.