# Normal field extensions #

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

## Main Definitions #

• Normal F K where K is a field extension of F.
class Normal (F : Type u_1) (K : Type u_2) [] [] [Algebra F K] extends :

Typeclass for normal field extension: K is a normal extension of F iff the minimal polynomial of every element x in K splits in K, i.e. every conjugate of x is in K.

Instances
theorem Normal.splits' {F : Type u_1} {K : Type u_2} [] [] [Algebra F K] [self : Normal F K] (x : K) :
theorem Normal.isIntegral {F : Type u_1} {K : Type u_2} [] [] [Algebra F K] :
Normal F K∀ (x : K),
theorem Normal.splits {F : Type u_1} {K : Type u_2} [] [] [Algebra F K] :
Normal F K∀ (x : K), Polynomial.Splits () (minpoly F x)
theorem normal_iff {F : Type u_1} {K : Type u_2} [] [] [Algebra F K] :
Normal F K ∀ (x : K), Polynomial.Splits () (minpoly F x)
theorem Normal.out {F : Type u_1} {K : Type u_2} [] [] [Algebra F K] :
Normal F K∀ (x : K), Polynomial.Splits () (minpoly F x)
instance normal_self (F : Type u_1) [] :
Normal F F
Equations
• =
theorem Normal.exists_isSplittingField (F : Type u_1) (K : Type u_2) [] [] [Algebra F K] [h : Normal F K] [] :
∃ (p : ),
theorem Normal.tower_top_of_normal (F : Type u_1) (K : Type u_2) [] [] [Algebra F K] (E : Type u_3) [] [Algebra F E] [Algebra K E] [] [h : Normal F E] :
Normal K E
theorem AlgHom.normal_bijective (F : Type u_1) (K : Type u_2) [] [] [Algebra F K] (E : Type u_3) [] [Algebra F E] [Algebra K E] [] [h : Normal F E] (ϕ : E →ₐ[F] K) :
theorem Normal.of_algEquiv {F : Type u_1} {E : Type u_3} {E' : Type u_4} [] [] [Algebra F E] [Field E'] [Algebra F E'] [h : Normal F E] (f : E ≃ₐ[F] E') :
Normal F E'
theorem AlgEquiv.transfer_normal {F : Type u_1} {E : Type u_3} {E' : Type u_4} [] [] [Algebra F E] [Field E'] [Algebra F E'] (f : E ≃ₐ[F] E') :
Normal F E Normal F E'
theorem Normal.of_isSplittingField {F : Type u_1} {E : Type u_3} [] [] [Algebra F E] (p : ) [hFEp : ] :
Normal F E
instance Polynomial.SplittingField.instNormal {F : Type u_1} [] (p : ) :
Normal F p.SplittingField
Equations
• =
instance IntermediateField.normal_iSup (F : Type u_1) (K : Type u_2) [] [] [Algebra F K] {ι : Type u_3} (t : ι) [h : ∀ (i : ι), Normal F (t i)] :
Normal F (⨆ (i : ι), t i)

A compositum of normal extensions is normal

Equations
• =
theorem IntermediateField.splits_of_mem_adjoin (F : Type u_1) (K : Type u_2) [] [] [Algebra F K] {L : Type u_3} [] [Algebra F L] {S : Set K} (splits : xS, Polynomial.Splits () (minpoly F x)) {x : K} (hx : ) :

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.

instance IntermediateField.normal_sup (F : Type u_1) (K : Type u_2) [] [] [Algebra F K] (E : ) (E' : ) [Normal F E] [Normal F E'] :
Normal F (E E')
Equations
• =
@[simp]
theorem IntermediateField.restrictScalars_normal {F : Type u_1} {K : Type u_2} {L : Type u_3} [] [] [] [Algebra F L] [Algebra K L] [Algebra F K] [] {E : } :
Normal F E
def AlgHom.restrictNormalAux {F : Type u_1} {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) [] [Algebra F E] [Algebra E K₁] [Algebra E K₂] [IsScalarTower F E K₁] [IsScalarTower F E K₂] [h : Normal F E] :
().range →ₐ[F] ().range

Restrict algebra homomorphism to image of normal subfield

Equations
• ϕ.restrictNormalAux E = { toFun := fun (x : ().range) => ϕ x, , map_one' := , map_mul' := , map_zero' := , map_add' := , commutes' := }
Instances For
def AlgHom.restrictNormal {F : Type u_1} {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) [] [Algebra F E] [Algebra E K₁] [Algebra E K₂] [IsScalarTower F E K₁] [IsScalarTower F E K₂] [Normal F E] :

Restrict algebra homomorphism to normal subfield

Equations
• ϕ.restrictNormal E = ((().symm).comp (ϕ.restrictNormalAux E)).comp ()
Instances For
def AlgHom.restrictNormal' {F : Type u_1} {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) [] [Algebra F E] [Algebra E K₁] [Algebra E K₂] [IsScalarTower F E K₁] [IsScalarTower F E K₂] [Normal F E] :

Restrict algebra homomorphism to normal subfield (AlgEquiv version)

Equations
Instances For
@[simp]
theorem AlgHom.restrictNormal_commutes {F : Type u_1} {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) [] [Algebra F E] [Algebra E K₁] [Algebra E K₂] [IsScalarTower F E K₁] [IsScalarTower F E K₂] [Normal F E] (x : E) :
(algebraMap E K₂) ((ϕ.restrictNormal E) x) = ϕ ((algebraMap E K₁) x)
theorem AlgHom.restrictNormal_comp {F : Type u_1} {K₁ : Type u_3} {K₂ : Type u_4} {K₃ : Type u_5} [] [Field K₁] [Field K₂] [Field K₃] [Algebra F K₁] [Algebra F K₂] [Algebra F K₃] (ϕ : K₁ →ₐ[F] K₂) (ψ : K₂ →ₐ[F] K₃) (E : Type u_6) [] [Algebra F E] [Algebra E K₁] [Algebra E K₂] [Algebra E K₃] [IsScalarTower F E K₁] [IsScalarTower F E K₂] [IsScalarTower F E K₃] [Normal F E] :
(ψ.restrictNormal E).comp (ϕ.restrictNormal E) = (ψ.comp ϕ).restrictNormal E
theorem AlgHom.fieldRange_of_normal {F : Type u_1} {K : Type u_2} [] [] [Algebra F K] {E : } [Normal F E] (f : E →ₐ[F] K) :
f.fieldRange = E
def AlgEquiv.restrictNormal {F : Type u_1} {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) [] [Algebra F E] [Algebra E K₁] [Algebra E K₂] [IsScalarTower F E K₁] [IsScalarTower F E K₂] [Normal F E] :

Restrict algebra isomorphism to a normal subfield

Equations
• χ.restrictNormal E = (χ).restrictNormal' E
Instances For
@[simp]
theorem AlgEquiv.restrictNormal_commutes {F : Type u_1} {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) [] [Algebra F E] [Algebra E K₁] [Algebra E K₂] [IsScalarTower F E K₁] [IsScalarTower F E K₂] [Normal F E] (x : E) :
(algebraMap E K₂) ((χ.restrictNormal E) x) = χ ((algebraMap E K₁) x)
theorem AlgEquiv.restrictNormal_trans {F : Type u_1} {K₁ : Type u_3} {K₂ : Type u_4} {K₃ : Type u_5} [] [Field K₁] [Field K₂] [Field K₃] [Algebra F K₁] [Algebra F K₂] [Algebra F K₃] (χ : K₁ ≃ₐ[F] K₂) (ω : K₂ ≃ₐ[F] K₃) (E : Type u_6) [] [Algebra F E] [Algebra E K₁] [Algebra E K₂] [Algebra E K₃] [IsScalarTower F E K₁] [IsScalarTower F E K₂] [IsScalarTower F E K₃] [Normal F E] :
(χ.trans ω).restrictNormal E = (χ.restrictNormal E).trans (ω.restrictNormal E)
def AlgEquiv.restrictNormalHom {F : Type u_1} {K₁ : Type u_3} [] [Field K₁] [Algebra F K₁] (E : Type u_6) [] [Algebra F E] [Algebra E K₁] [IsScalarTower F E K₁] [Normal F E] :
(K₁ ≃ₐ[F] K₁) →* E ≃ₐ[F] E

Restriction to a normal subfield as a group homomorphism

Equations
Instances For
@[simp]
theorem Normal.algHomEquivAut_apply (F : Type u_1) (K₁ : Type u_3) [] [Field K₁] [Algebra F K₁] (E : Type u_6) [] [Algebra F E] [Algebra E K₁] [IsScalarTower F E K₁] [Normal F E] (σ : E →ₐ[F] K₁) :
() σ = σ.restrictNormal' E
@[simp]
theorem Normal.algHomEquivAut_symm_apply (F : Type u_1) (K₁ : Type u_3) [] [Field K₁] [Algebra F K₁] (E : Type u_6) [] [Algebra F E] [Algebra E K₁] [IsScalarTower F E K₁] [Normal F E] (σ : E ≃ₐ[F] E) :
().symm σ = ().comp σ
def Normal.algHomEquivAut (F : Type u_1) (K₁ : Type u_3) [] [Field K₁] [Algebra F K₁] (E : Type u_6) [] [Algebra F E] [Algebra E K₁] [IsScalarTower F E K₁] [Normal F E] :
(E →ₐ[F] K₁) E ≃ₐ[F] E

If K₁/E/F is a tower of fields with E/F normal then AlgHom.restrictNormal' is an equivalence.

Equations
• One or more equations did not get rendered due to their size.
Instances For
noncomputable def AlgHom.liftNormal {F : Type u_1} {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) [] [Algebra F E] [Algebra K₁ E] [Algebra K₂ E] [IsScalarTower F K₁ E] [IsScalarTower F K₂ E] [h : Normal 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
@[simp]
theorem AlgHom.liftNormal_commutes {F : Type u_1} {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) [] [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)
@[simp]
theorem AlgHom.restrict_liftNormal {F : Type u_1} {K₁ : Type u_3} [] [Field K₁] [Algebra F K₁] (E : Type u_6) [] [Algebra F E] [Algebra K₁ E] [IsScalarTower F K₁ E] (ϕ : K₁ →ₐ[F] K₁) [Normal F K₁] [Normal F E] :
(ϕ.liftNormal E).restrictNormal K₁ = ϕ
noncomputable def AlgEquiv.liftNormal {F : Type u_1} {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) [] [Algebra F E] [Algebra K₁ E] [Algebra K₂ E] [IsScalarTower F K₁ E] [IsScalarTower F K₂ E] [Normal 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
@[simp]
theorem AlgEquiv.liftNormal_commutes {F : Type u_1} {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) [] [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)
@[simp]
theorem AlgEquiv.restrict_liftNormal {F : Type u_1} {K₁ : Type u_3} [] [Field K₁] [Algebra F K₁] (E : Type u_6) [] [Algebra F E] [Algebra K₁ E] [IsScalarTower F K₁ E] (χ : K₁ ≃ₐ[F] K₁) [Normal F K₁] [Normal F E] :
(χ.liftNormal E).restrictNormal K₁ = χ
theorem AlgEquiv.restrictNormalHom_surjective {F : Type u_1} {K₁ : Type u_3} [] [Field K₁] [Algebra F K₁] (E : Type u_6) [] [Algebra F E] [Algebra K₁ E] [IsScalarTower F K₁ E] [Normal F K₁] [Normal F E] :
theorem Normal.minpoly_eq_iff_mem_orbit {F : Type u_1} [] (E : Type u_6) [] [Algebra F E] [h : Normal F E] {x : E} {y : E} :
theorem isSolvable_of_isScalarTower (F : Type u_1) (K₁ : Type u_3) [] [Field K₁] [Algebra F K₁] (E : Type u_6) [] [Algebra F E] [Algebra K₁ E] [IsScalarTower F K₁ E] [Normal F K₁] [h1 : IsSolvable (K₁ ≃ₐ[F] K₁)] [h2 : IsSolvable (E ≃ₐ[K₁] E)] :