mathlib3 documentation

field_theory.normal

Normal field extensions #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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_is_splitting_field and normal.exists_is_splitting_field).

Main Definitions #

source
@[class]
structure normal (F : Type u_1) (K : Type u_2) [field F] [field K] [algebra F K] :
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.

Instances of this typeclass
source
theorem normal.is_algebraic {F : Type u_1} {K : Type u_2} [field F] [field K] [algebra F K] (h : normal F K) (x : K) :
is_algebraic F x
source
theorem normal.is_integral {F : Type u_1} {K : Type u_2} [field F] [field K] [algebra F K] (h : normal F K) (x : K) :
is_integral F x
source
theorem normal.splits {F : Type u_1} {K : Type u_2} [field F] [field K] [algebra F K] (h : normal F K) (x : K) :
polynomial.splits (algebra_map F K) (minpoly F x)
source
theorem normal_iff {F : Type u_1} {K : Type u_2} [field F] [field K] [algebra F K] :
normal F K ↔ ∀ (x : K), is_integral F x ∧ polynomial.splits (algebra_map F K) (minpoly F x)
source
theorem normal.out {F : Type u_1} {K : Type u_2} [field F] [field K] [algebra F K] :
normal F K → ∀ (x : K), is_integral F x ∧ polynomial.splits (algebra_map F K) (minpoly F x)
source
@[protected, instance]
def normal_self (F : Type u_1) [field F] :
normal F F
source
theorem normal.exists_is_splitting_field (F : Type u_1) (K : Type u_2) [field F] [field K] [algebra F K] [h : normal F K] [finite_dimensional F K] :
∃ (p : polynomial F), polynomial.is_splitting_field F K p
source
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] [is_scalar_tower F K E] [h : normal F E] :
normal K E
source
theorem alg_hom.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] [is_scalar_tower F K E] [h : normal F E] (ϕ : E →ₐ[F] K) :
function.bijective ⇑ϕ
source
theorem normal.of_alg_equiv {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'
source
theorem alg_equiv.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'
source
theorem normal.of_is_splitting_field {F : Type u_1} [field F] {E : Type u_3} [field E] [algebra F E] (p : polynomial F) [hFEp : polynomial.is_splitting_field F E p] :
normal F E
source
@[protected, instance]
def intermediate_field.normal_supr (F : Type u_1) (K : Type u_2) [field F] [field K] [algebra F K] {ι : Type u_3} (t : ι → intermediate_field F K) [h : ∀ (i : ι), normal F ↥(t i)] :
normal F (↥⨆ (i : ι), t i)

A compositum of normal extensions is normal

source
@[simp]
theorem intermediate_field.restrict_scalars_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] [is_scalar_tower F K L] {E : intermediate_field K L} :
normal F ↥(intermediate_field.restrict_scalars F E) ↔ normal F ↥E
source
def alg_hom.restrict_normal_aux {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₂] [is_scalar_tower F E K₁] [is_scalar_tower F E K₂] [h : normal F E] :
↥((is_scalar_tower.to_alg_hom F E K₁).range) →ₐ[F] ↥((is_scalar_tower.to_alg_hom F E K₂).range)

Restrict algebra homomorphism to image of normal subfield

Equations
source
noncomputable def alg_hom.restrict_normal {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₂] [is_scalar_tower F E K₁] [is_scalar_tower F E K₂] [normal F E] :
E →ₐ[F] E

Restrict algebra homomorphism to normal subfield

Equations
source
noncomputable def alg_hom.restrict_normal' {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₂] [is_scalar_tower F E K₁] [is_scalar_tower F E K₂] [normal F E] :
E ≃ₐ[F] E

Restrict algebra homomorphism to normal subfield (alg_equiv version)

Equations
source
@[simp]
theorem alg_hom.restrict_normal_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₂] [is_scalar_tower F E K₁] [is_scalar_tower F E K₂] [normal F E] (x : E) :
⇑(algebra_map E K₂) (⇑(ϕ.restrict_normal E) x) = ⇑ϕ (⇑(algebra_map E K₁) x)
source
theorem alg_hom.restrict_normal_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₃] [is_scalar_tower F E K₁] [is_scalar_tower F E K₂] [is_scalar_tower F E K₃] [normal F E] :
(ψ.restrict_normal E).comp (ϕ.restrict_normal E) = (ψ.comp ϕ).restrict_normal E
source
theorem alg_hom.field_range_of_normal {F : Type u_1} {K : Type u_2} [field F] [field K] [algebra F K] {E : intermediate_field F K} [normal F ↥E] (f : ↥E →ₐ[F] K) :
f.field_range = E
source
noncomputable def alg_equiv.restrict_normal {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₂] [is_scalar_tower F E K₁] [is_scalar_tower F E K₂] [h : normal F E] :
E ≃ₐ[F] E

Restrict algebra isomorphism to a normal subfield

Equations
source
@[simp]
theorem alg_equiv.restrict_normal_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₂] [is_scalar_tower F E K₁] [is_scalar_tower F E K₂] [normal F E] (x : E) :
⇑(algebra_map E K₂) (⇑(χ.restrict_normal E) x) = ⇑χ (⇑(algebra_map E K₁) x)
source
theorem alg_equiv.restrict_normal_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₃] [is_scalar_tower F E K₁] [is_scalar_tower F E K₂] [is_scalar_tower F E K₃] [normal F E] :
(χ.trans ω).restrict_normal E = (χ.restrict_normal E).trans (ω.restrict_normal E)
source
noncomputable def alg_equiv.restrict_normal_hom {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₁] [is_scalar_tower F E K₁] [normal F E] :
(K₁ ≃ₐ[F] K₁) →* E ≃ₐ[F] E

Restriction to an normal subfield as a group homomorphism

Equations
source
@[simp]
theorem normal.alg_hom_equiv_aut_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₁] [is_scalar_tower F E K₁] [normal F E] (σ : E →ₐ[F] K₁) :
⇑(normal.alg_hom_equiv_aut F K₁ E) σ = σ.restrict_normal' E
source
@[simp]
theorem normal.alg_hom_equiv_aut_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₁] [is_scalar_tower F E K₁] [normal F E] (σ : E ≃ₐ[F] E) :
⇑((normal.alg_hom_equiv_aut F K₁ E).symm) σ = (is_scalar_tower.to_alg_hom F E K₁).comp σ.to_alg_hom
source
noncomputable def normal.alg_hom_equiv_aut (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₁] [is_scalar_tower 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 normal.alg_hom_equiv_aut is an equivalence.

Equations
source
noncomputable def alg_hom.lift_normal {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] [is_scalar_tower F K₁ E] [is_scalar_tower 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 ϕ.lift_normal E : E →ₐ[F] E.

Equations
source
@[simp]
theorem alg_hom.lift_normal_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] [is_scalar_tower F K₁ E] [is_scalar_tower F K₂ E] [normal F E] (x : K₁) :
⇑(ϕ.lift_normal E) (⇑(algebra_map K₁ E) x) = ⇑(algebra_map K₂ E) (⇑ϕ x)
source
@[simp]
theorem alg_hom.restrict_lift_normal {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] [is_scalar_tower F K₁ E] (ϕ : K₁ →ₐ[F] K₁) [normal F K₁] [normal F E] :
(ϕ.lift_normal E).restrict_normal K₁ = ϕ
source
noncomputable def alg_equiv.lift_normal {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] [is_scalar_tower F K₁ E] [is_scalar_tower 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 ϕ.lift_normal E : E ≃ₐ[F] E.

Equations
source
@[simp]
theorem alg_equiv.lift_normal_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] [is_scalar_tower F K₁ E] [is_scalar_tower F K₂ E] [normal F E] (x : K₁) :
⇑(χ.lift_normal E) (⇑(algebra_map K₁ E) x) = ⇑(algebra_map K₂ E) (⇑χ x)
source
@[simp]
theorem alg_equiv.restrict_lift_normal {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] [is_scalar_tower F K₁ E] (χ : K₁ ≃ₐ[F] K₁) [normal F K₁] [normal F E] :
(χ.lift_normal E).restrict_normal K₁ = χ
source
theorem alg_equiv.restrict_normal_hom_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] [is_scalar_tower F K₁ E] [normal F K₁] [normal F E] :
function.surjective ⇑(alg_equiv.restrict_normal_hom K₁)
source
theorem is_solvable_of_is_scalar_tower (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] [is_scalar_tower F K₁ E] [normal F K₁] [h1 : is_solvable (K₁ ≃ₐ[F] K₁)] [h2 : is_solvable (E ≃ₐ[K₁] E)] :
is_solvable (E ≃ₐ[F] E)
source
def normal_closure (F : Type u_1) (K : Type u_2) [field F] [field K] [algebra F K] (L : Type u_6) [field L] [algebra F L] [algebra K L] [is_scalar_tower F K L] :
intermediate_field K L

The normal closure of K in L.

Equations
Instances for ↥normal_closure
source
theorem normal_closure.restrict_scalars_eq_supr_adjoin (F : Type u_1) (K : Type u_2) [field F] [field K] [algebra F K] (L : Type u_6) [field L] [algebra F L] [algebra K L] [is_scalar_tower F K L] [h : normal F L] :
intermediate_field.restrict_scalars F (normal_closure F K L) = ⨆ (x : K), intermediate_field.adjoin F ((minpoly F x).root_set L)
source
@[protected, instance]
def normal_closure.normal (F : Type u_1) (K : Type u_2) [field F] [field K] [algebra F K] (L : Type u_6) [field L] [algebra F L] [algebra K L] [is_scalar_tower F K L] [h : normal F L] :
normal F ↥(normal_closure F K L)
source
@[protected, instance]
def normal_closure.is_finite_dimensional (F : Type u_1) (K : Type u_2) [field F] [field K] [algebra F K] (L : Type u_6) [field L] [algebra F L] [algebra K L] [is_scalar_tower F K L] [finite_dimensional F K] :
finite_dimensional F ↥(normal_closure F K L)
source
@[protected, instance]
def normal_closure.is_scalar_tower (F : Type u_1) (K : Type u_2) [field F] [field K] [algebra F K] (L : Type u_6) [field L] [algebra F L] [algebra K L] [is_scalar_tower F K L] :
is_scalar_tower F ↥(normal_closure F K L) L