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] extends Algebra.IsAlgebraic : Prop

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.

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

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

theorem Normal.isIntegral {F : Type u_1} {K : Type u_2} [Field F] [Field K] [Algebra F K] : 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

• ⋯ = ⋯

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

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} [Field F] {E : Type u_3} [Field E] [Algebra F E] {E' : Type u_4} [Field E'] [Algebra F E'] [h : Normal F E] (f : E ≃ₐ[F] E') : Normal F E'

theorem AlgEquiv.transfer_normal {F : Type u_1} [Field F] {E : Type u_3} [Field E] [Algebra F E] {E' : Type u_4} [Field E'] [Algebra F E'] (f : E ≃ₐ[F] E') : Normal F E ↔ Normal F E'

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

instance Polynomial.SplittingField.instNormal {F : Type u_1} [Field F] (p : Polynomial F) : Normal F p.SplittingField

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯

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 ∈ IntermediateField.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.

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 ↥E] [Normal F ↥E'] : Normal F ↥(E ⊔ E')

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯

instance IntermediateField.normal_inf (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 ↥E] [Normal F ↥E'] : Normal F ↥(E ⊓ E')

Equations

• ⋯ = ⋯

@[simp]

theorem IntermediateField.restrictScalars_normal {F : Type u_1} {K : Type u_2} [Field F] [Field K] [Algebra F K] {L : Type u_3} [Field L] [Algebra F L] [Algebra K L] [IsScalarTower F K L] {E : IntermediateField K L} : Normal F ↥(IntermediateField.restrictScalars F E) ↔ Normal F ↥E

def AlgHom.restrictNormalAux {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 E K₁] [Algebra E K₂] [IsScalarTower F E K₁] [IsScalarTower F E K₂] [h : Normal F E] : ↥(IsScalarTower.toAlgHom F E K₁).range →ₐ[F] ↥(IsScalarTower.toAlgHom F E K₂).range

Restrict algebra homomorphism to image of normal subfield

Equations

• ϕ.restrictNormalAux E = { toFun := fun (x : ↥(IsScalarTower.toAlgHom F E K₁).range) => ⟨ϕ ↑x, ⋯⟩, map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯, commutes' := ⋯ }

def AlgHom.restrictNormal {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 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

• ϕ.restrictNormal E = ((↑(AlgEquiv.ofInjectiveField (IsScalarTower.toAlgHom F E K₂)).symm).comp (ϕ.restrictNormalAux E)).comp ↑(AlgEquiv.ofInjectiveField (IsScalarTower.toAlgHom F E K₁))

def AlgHom.restrictNormal' {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 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

• ϕ.restrictNormal' E = AlgEquiv.ofBijective (ϕ.restrictNormal E) ⋯

@[simp]

theorem AlgHom.restrictNormal_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 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} [Field F] {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) [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] : (ψ.restrictNormal E).comp (ϕ.restrictNormal E) = (ψ.comp ϕ).restrictNormal E

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

def AlgEquiv.restrictNormal {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 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

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

@[simp]

theorem AlgEquiv.restrictNormal_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 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} [Field F] {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) [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] : (χ.trans ω).restrictNormal E = (χ.restrictNormal E).trans (ω.restrictNormal E)

def AlgEquiv.restrictNormalHom {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 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

• AlgEquiv.restrictNormalHom E = MonoidHom.mk' (fun (χ : K₁ ≃ₐ[F] K₁) => χ.restrictNormal E) ⋯

@[simp]

theorem Normal.algHomEquivAut_apply (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 E K₁] [IsScalarTower F E K₁] [Normal F E] (σ : E →ₐ[F] K₁) : (Normal.algHomEquivAut F K₁ E) σ = σ.restrictNormal' E

@[simp]

theorem Normal.algHomEquivAut_symm_apply (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 E K₁] [IsScalarTower F E K₁] [Normal F E] (σ : E ≃ₐ[F] E) : (Normal.algHomEquivAut F K₁ E).symm σ = (IsScalarTower.toAlgHom F E K₁).comp ↑σ

def Normal.algHomEquivAut (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 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

• Normal.algHomEquivAut F K₁ E = { toFun := fun (σ : E →ₐ[F] K₁) => σ.restrictNormal' E, invFun := fun (σ : E ≃ₐ[F] E) => (IsScalarTower.toAlgHom F E K₁).comp ↑σ, left_inv := ⋯, right_inv := ⋯ }

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

• ϕ.liftNormal E = AlgHom.restrictScalars F ⋯.some

@[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)

@[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₁ = ϕ

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

• χ.liftNormal E = AlgEquiv.ofBijective ((↑χ).liftNormal E) ⋯

@[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)

@[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₁ = χ

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 ⇑(AlgEquiv.restrictNormalHom K₁)

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

@[simp]

theorem AlgEquiv.restrictNormalHom_id (F : Type u_7) (K : Type u_8) [Field F] [Field K] [Algebra F K] [Normal F K] : AlgEquiv.restrictNormalHom K = MonoidHom.id (K ≃ₐ[F] K)

The group homomorphism given by restricting an algebra isomorphism to itself is the identity map.

theorem IsScalarTower.AlgEquiv.restrictNormalHom_comp (F : Type u_7) (K₁ : Type u_8) (K₂ : Type u_9) (K₃ : Type u_10) [Field F] [Field K₁] [Field K₂] [Field K₃] [Algebra F K₁] [Algebra F K₂] [Algebra F K₃] [Algebra K₁ K₂] [Algebra K₁ K₃] [Algebra K₂ K₃] [IsScalarTower F K₁ K₃] [IsScalarTower F K₁ K₂] [IsScalarTower F K₂ K₃] [IsScalarTower K₁ K₂ K₃] [Normal F K₁] [Normal F K₂] : AlgEquiv.restrictNormalHom K₁ = (AlgEquiv.restrictNormalHom K₁).comp (AlgEquiv.restrictNormalHom K₂)

In a scalar tower K₃/K₂/K₁/F with K₁ and K₂ are normal over F, the group homomorphism given by the restriction of algebra isomorphisms of K₃ to K₁ is equal to the composition of the group homomorphism given by the restricting an algebra isomorphism of K₃ to K₂ and the group homomorphism given by the restricting an algebra isomorphism of K₂ to K₁

theorem IsScalarTower.AlgEquiv.restrictNormalHom_comp_apply (K₁ : Type u_7) (K₂ : Type u_8) {F : Type u_9} {K₃ : Type u_10} [Field F] [Field K₁] [Field K₂] [Field K₃] [Algebra F K₁] [Algebra F K₂] [Algebra F K₃] [Algebra K₁ K₂] [Algebra K₁ K₃] [Algebra K₂ K₃] [IsScalarTower F K₁ K₃] [IsScalarTower F K₁ K₂] [IsScalarTower F K₂ K₃] [IsScalarTower K₁ K₂ K₃] [Normal F K₁] [Normal F K₂] (f : K₃ ≃ₐ[F] K₃) : (AlgEquiv.restrictNormalHom K₁) f = (AlgEquiv.restrictNormalHom K₁) ((AlgEquiv.restrictNormalHom K₂) f)

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 : E} {y : E} : minpoly F x = minpoly F y ↔ x ∈ MulAction.orbit (E ≃ₐ[F] E) y

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)

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 : L} {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.

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 : L} {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.