mathlib documentation

field_theory.normal

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

Main Definitions #

@[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
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) :
theorem normal.splits {F : Type u_1} {K : Type u_2} [field F] [field K] [algebra F K] (h : normal F K) (x : K) :
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)
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)
@[instance]
def normal_self (F : Type u_1) [field F] :
normal F F
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] :
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
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) :
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'
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'
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
@[instance]
def alg_hom.restrict_normal_aux {F : Type u_1} {K : Type u_2} [field F] [field K] [algebra F K] (ϕ : K →ₐ[F] K) (E : Type u_3) [field E] [algebra F E] [algebra E K] [is_scalar_tower F E K] [h : normal F E] :

Restrict algebra homomorphism to image of normal subfield

Equations
def alg_hom.restrict_normal {F : Type u_1} {K : Type u_2} [field F] [field K] [algebra F K] (ϕ : K →ₐ[F] K) (E : Type u_3) [field E] [algebra F E] [algebra E K] [is_scalar_tower F E K] [normal F E] :

Restrict algebra homomorphism to normal subfield

Equations
@[simp]
theorem alg_hom.restrict_normal_commutes {F : Type u_1} {K : Type u_2} [field F] [field K] [algebra F K] (ϕ : K →ₐ[F] K) (E : Type u_3) [field E] [algebra F E] [algebra E K] [is_scalar_tower F E K] [normal F E] (x : E) :
theorem alg_hom.restrict_normal_comp {F : Type u_1} {K : Type u_2} [field F] [field K] [algebra F K] (ϕ ψ : K →ₐ[F] K) (E : Type u_3) [field E] [algebra F E] [algebra E K] [is_scalar_tower F E K] [normal F E] :
def alg_equiv.restrict_normal {F : Type u_1} {K : Type u_2} [field F] [field K] [algebra F K] (χ : K ≃ₐ[F] K) (E : Type u_3) [field E] [algebra F E] [algebra E K] [is_scalar_tower F E K] [h : normal F E] :

Restrict algebra isomorphism to a normal subfield

Equations
@[simp]
theorem alg_equiv.restrict_normal_commutes {F : Type u_1} {K : Type u_2} [field F] [field K] [algebra F K] (χ : K ≃ₐ[F] K) (E : Type u_3) [field E] [algebra F E] [algebra E K] [is_scalar_tower F E K] [normal F E] (x : E) :
theorem alg_equiv.restrict_normal_trans {F : Type u_1} {K : Type u_2} [field F] [field K] [algebra F K] (χ ω : K ≃ₐ[F] K) (E : Type u_3) [field E] [algebra F E] [algebra E K] [is_scalar_tower F E K] [normal F E] :
def alg_equiv.restrict_normal_hom {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 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
def alg_hom.lift_normal {F : Type u_1} {K : Type u_2} [field F] [field K] [algebra F K] (ϕ : K →ₐ[F] K) (E : Type u_3) [field E] [algebra F E] [algebra K E] [is_scalar_tower F K E] [h : normal F E] :

If E/K/F is a tower of fields with E/F normal then we can lift an algebra homomorphism ϕ : K →ₐ[F] K to ϕ.lift_normal E : E →ₐ[F] E.

Equations
@[simp]
theorem alg_hom.lift_normal_commutes {F : Type u_1} {K : Type u_2} [field F] [field K] [algebra F K] (ϕ : K →ₐ[F] K) (E : Type u_3) [field E] [algebra F E] [algebra 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)
@[simp]
theorem alg_hom.restrict_lift_normal {F : Type u_1} {K : Type u_2} [field F] [field K] [algebra F K] (ϕ : K →ₐ[F] K) (E : Type u_3) [field E] [algebra F E] [algebra K E] [is_scalar_tower F K E] [normal F K] [normal F E] :
def alg_equiv.lift_normal {F : Type u_1} {K : Type u_2} [field F] [field K] [algebra F K] (χ : K ≃ₐ[F] K) (E : Type u_3) [field E] [algebra F E] [algebra K E] [is_scalar_tower F K E] [normal F E] :

If E/K/F is a tower of fields with E/F normal then we can lift an algebra isomorphism ϕ : K ≃ₐ[F] K to ϕ.lift_normal E : E ≃ₐ[F] E.

Equations
@[simp]
theorem alg_equiv.lift_normal_commutes {F : Type u_1} {K : Type u_2} [field F] [field K] [algebra F K] (χ : K ≃ₐ[F] K) (E : Type u_3) [field E] [algebra F E] [algebra 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)
@[simp]
theorem alg_equiv.restrict_lift_normal {F : Type u_1} {K : Type u_2} [field F] [field K] [algebra F K] (χ : K ≃ₐ[F] K) (E : Type u_3) [field E] [algebra F E] [algebra K E] [is_scalar_tower F K E] [normal F K] [normal F E] :
theorem alg_equiv.restrict_normal_hom_surjective {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] [normal F K] [normal F E] :
theorem is_solvable_of_is_scalar_tower (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] [normal F K] [h1 : is_solvable (K ≃ₐ[F] K)] [h2 : is_solvable (E ≃ₐ[K] E)] :