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) [Field F] [Field K] [Algebra F K] : Prop

• isAlgebraic' : Algebra.IsAlgebraic F K
• splits' : ∀ (x : K), Polynomial.Splits (algebraMap F K) (minpoly F x)

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.

theorem Normal.isAlgebraic {F : Type u_1} {K : Type u_2} [Field F] [Field K] [Algebra F K] : Normal F K → ∀ (x : K), IsAlgebraic F x

theorem Normal.isIntegral {F : Type u_1} {K : Type u_2} [Field F] [Field K] [Algebra F K] (h : Normal F K) (x : K) : IsIntegral F x

theorem Normal.splits {F : Type u_1} {K : Type u_2} [Field F] [Field K] [Algebra F K] : Normal F K → ∀ (x : K), Polynomial.Splits (algebraMap F K) (minpoly F x)

theorem normal_iff {F : Type u_1} {K : Type u_2} [Field F] [Field K] [Algebra F K] : Normal F K ↔ ∀ (x : K), IsIntegral F x ∧ Polynomial.Splits (algebraMap F K) (minpoly F x)

theorem Normal.out {F : Type u_1} {K : Type u_2} [Field F] [Field K] [Algebra F K] : Normal F K → ∀ (x : K), IsIntegral F x ∧ Polynomial.Splits (algebraMap F K) (minpoly F x)

instance normal_self (F : Type u_1) [Field F] : Normal F F

Equations

• normal_self = normal_self.proof_1

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.IsSplittingField F K p

theorem Normal.tower_top_of_normal (F : Type u_1) (K : Type u_2) [Field F] [Field K] [Algebra F K] (E : Type u_3) [Field E] [Algebra F E] [Algebra K E] [IsScalarTower F K E] [h : Normal F E] : Normal K E

theorem AlgHom.normal_bijective (F : Type u_1) (K : Type u_2) [Field F] [Field K] [Algebra F K] (E : Type u_3) [Field E] [Algebra F E] [Algebra K E] [IsScalarTower F K E] [h : Normal F E] (ϕ : E →ₐ[F] K) : Function.Bijective ↑ϕ

theorem Normal.of_algEquiv {F : Type u_1} {E : Type u_3} {E' : Type u_4} [Field F] [Field E] [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} [Field F] [Field E] [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} [Field F] [Field E] [Algebra F E] (p : Polynomial F) [hFEp : Polynomial.IsSplittingField F E p] : Normal F E

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 { x // x ∈ t i }] : Normal F { x // x ∈ ⨆ (i : ι), t i }

A compositum of normal extensions is normal

Equations

• IntermediateField.normal_iSup = IntermediateField.normal_iSup.proof_1

instance IntermediateField.normal_sup (F : Type u_1) (K : Type u_2) [Field F] [Field K] [Algebra F K] (E : IntermediateField F K) (E' : IntermediateField F K) [Normal F { x // x ∈ E }] [Normal F { x // x ∈ E' }] : Normal F { x // x ∈ E ⊔ E' }

Equations

• IntermediateField.normal_sup = IntermediateField.normal_sup.proof_1

@[simp]

theorem IntermediateField.restrictScalars_normal {F : Type u_1} {K : Type u_2} {L : Type u_3} [Field F] [Field K] [Field L] [Algebra F L] [Algebra K L] [Algebra F K] [IsScalarTower F K L] {E : IntermediateField K L} : Normal F { x // x ∈ IntermediateField.restrictScalars F E } ↔ Normal F { x // x ∈ E }

def AlgHom.restrictNormalAux {F : Type u_1} {K₁ : Type u_3} {K₂ : Type u_4} [Field F] [Field K₁] [Field K₂] [Algebra F K₁] [Algebra F K₂] (ϕ : K₁ →ₐ[F] K₂) (E : Type u_6) [Field E] [Algebra F E] [Algebra E K₁] [Algebra E K₂] [IsScalarTower F E K₁] [IsScalarTower F E K₂] [h : Normal F E] : { x // x ∈ AlgHom.range (IsScalarTower.toAlgHom F E K₁) } →ₐ[F] { x // x ∈ AlgHom.range (IsScalarTower.toAlgHom F E K₂) }

Restrict algebra homomorphism to image of normal subfield

Equations

• One or more equations did not get rendered due to their size.

def AlgHom.restrictNormal {F : Type u_1} {K₁ : Type u_3} {K₂ : Type u_4} [Field F] [Field K₁] [Field K₂] [Algebra F K₁] [Algebra F K₂] (ϕ : K₁ →ₐ[F] K₂) (E : Type u_6) [Field E] [Algebra F E] [Algebra E K₁] [Algebra E K₂] [IsScalarTower F E K₁] [IsScalarTower F E K₂] [Normal F E] : E →ₐ[F] E

Restrict algebra homomorphism to normal subfield

Equations

• One or more equations did not get rendered due to their size.

def AlgHom.restrictNormal' {F : Type u_1} {K₁ : Type u_3} {K₂ : Type u_4} [Field F] [Field K₁] [Field K₂] [Algebra F K₁] [Algebra F K₂] (ϕ : K₁ →ₐ[F] K₂) (E : Type u_6) [Field E] [Algebra F E] [Algebra E K₁] [Algebra E K₂] [IsScalarTower F E K₁] [IsScalarTower F E K₂] [Normal F E] : E ≃ₐ[F] E

Restrict algebra homomorphism to normal subfield (AlgEquiv version)

Equations

• AlgHom.restrictNormal' ϕ E = AlgEquiv.ofBijective (AlgHom.restrictNormal ϕ E) (_ : Function.Bijective ↑(AlgHom.restrictNormal ϕ E))

@[simp]

theorem AlgHom.restrictNormal_commutes {F : Type u_1} {K₁ : Type u_3} {K₂ : Type u_4} [Field F] [Field K₁] [Field K₂] [Algebra F K₁] [Algebra F K₂] (ϕ : K₁ →ₐ[F] K₂) (E : Type u_6) [Field E] [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₂) (↑(AlgHom.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 F] [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) [Field E] [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] : AlgHom.comp (AlgHom.restrictNormal ψ E) (AlgHom.restrictNormal ϕ E) = AlgHom.restrictNormal (AlgHom.comp ψ ϕ) E

theorem AlgHom.fieldRange_of_normal {F : Type u_1} {K : Type u_2} [Field K] [Field F] [Algebra F K] {E : IntermediateField F K} [Normal F { x // x ∈ E }] (f : { x // x ∈ E } →ₐ[F] K) : AlgHom.fieldRange f = E

def AlgEquiv.restrictNormal {F : Type u_1} {K₁ : Type u_3} {K₂ : Type u_4} [Field F] [Field K₁] [Field K₂] [Algebra F K₁] [Algebra F K₂] (χ : K₁ ≃ₐ[F] K₂) (E : Type u_6) [Field E] [Algebra F E] [Algebra E K₁] [Algebra E K₂] [IsScalarTower F E K₁] [IsScalarTower F E K₂] [Normal F E] : E ≃ₐ[F] E

Restrict algebra isomorphism to a normal subfield

Equations

• AlgEquiv.restrictNormal χ E = AlgHom.restrictNormal' (↑χ) E

@[simp]

theorem AlgEquiv.restrictNormal_commutes {F : Type u_1} {K₁ : Type u_3} {K₂ : Type u_4} [Field F] [Field K₁] [Field K₂] [Algebra F K₁] [Algebra F K₂] (χ : K₁ ≃ₐ[F] K₂) (E : Type u_6) [Field E] [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₂) (↑(AlgEquiv.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 F] [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) [Field E] [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] : AlgEquiv.restrictNormal (AlgEquiv.trans χ ω) E = AlgEquiv.trans (AlgEquiv.restrictNormal χ E) (AlgEquiv.restrictNormal ω E)

def AlgEquiv.restrictNormalHom {F : Type u_1} {K₁ : Type u_3} [Field F] [Field K₁] [Algebra F K₁] (E : Type u_6) [Field E] [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

• One or more equations did not get rendered due to their size.

@[simp]

theorem Normal.algHomEquivAut_apply (F : Type u_1) (K₁ : Type u_3) [Field F] [Field K₁] [Algebra F K₁] (E : Type u_6) [Field E] [Algebra F E] [Algebra E K₁] [IsScalarTower F E K₁] [Normal F E] (σ : E →ₐ[F] K₁) : ↑(Normal.algHomEquivAut F K₁ E) σ = AlgHom.restrictNormal' σ E

@[simp]

theorem Normal.algHomEquivAut_symm_apply (F : Type u_1) (K₁ : Type u_3) [Field F] [Field K₁] [Algebra F K₁] (E : Type u_6) [Field E] [Algebra F E] [Algebra E K₁] [IsScalarTower F E K₁] [Normal F E] (σ : E ≃ₐ[F] E) : ↑(Normal.algHomEquivAut F K₁ E).symm σ = AlgHom.comp (IsScalarTower.toAlgHom F E K₁) ↑σ

def Normal.algHomEquivAut (F : Type u_1) (K₁ : Type u_3) [Field F] [Field K₁] [Algebra F K₁] (E : Type u_6) [Field E] [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.

noncomputable def AlgHom.liftNormal {F : Type u_1} [Field F] {K₁ : Type u_3} {K₂ : Type u_4} [Field F] [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

• AlgHom.liftNormal ϕ E = AlgHom.restrictScalars F (Nonempty.some (_ : Nonempty (E →ₐ[K₁] E)))

@[simp]

theorem AlgHom.liftNormal_commutes {F : Type u_1} {K₁ : Type u_3} {K₂ : Type u_4} [Field F] [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₁) : ↑(AlgHom.liftNormal ϕ E) (↑(algebraMap K₁ E) x) = ↑(algebraMap K₂ E) (↑ϕ x)

@[simp]

theorem AlgHom.restrict_liftNormal {F : Type u_1} {K₁ : Type u_3} [Field F] [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] : AlgHom.restrictNormal (AlgHom.liftNormal ϕ E) K₁ = ϕ

noncomputable def AlgEquiv.liftNormal {F : Type u_1} {K₁ : Type u_3} {K₂ : Type u_4} [Field F] [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

• AlgEquiv.liftNormal χ E = AlgEquiv.ofBijective (AlgHom.liftNormal (↑χ) E) (_ : Function.Bijective ↑(AlgHom.liftNormal (↑χ) E))

@[simp]

theorem AlgEquiv.liftNormal_commutes {F : Type u_1} {K₁ : Type u_3} {K₂ : Type u_4} [Field F] [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₁) : ↑(AlgEquiv.liftNormal χ E) (↑(algebraMap K₁ E) x) = ↑(algebraMap K₂ E) (↑χ x)

@[simp]

theorem AlgEquiv.restrict_liftNormal {F : Type u_1} {K₁ : Type u_3} [Field F] [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] : AlgEquiv.restrictNormal (AlgEquiv.liftNormal χ E) K₁ = χ

theorem AlgEquiv.restrictNormalHom_surjective {F : Type u_1} {K₁ : Type u_3} [Field F] [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 ↑(AlgEquiv.restrictNormalHom K₁)

theorem isSolvable_of_isScalarTower (F : Type u_1) (K₁ : Type u_3) [Field F] [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)