Normal field extensions

In this file we define normal field extensions.

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 F K : Prop

Typeclass for normal field extensions: an algebraic extension of fields K/F is normal if the minimal polynomial of every element x in K splits in K, i.e. every F-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.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

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

Stacks Tag 09HN

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_equiv_equiv {F : Type u_1} [Field F] {E : Type u_3} [Field E] [Algebra F E] {M : Type u_5} {N : Type u_6} [Field N] [Field M] [Algebra M N] [Algebra.IsAlgebraic F E] [h : Normal F E] {f : F ≃+* M} {g : E ≃+* N} (hcomp : (algebraMap M N).comp ↑f = (↑g).comp (algebraMap F E)) : Normal M N

@[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 ↥(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

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) ⋯

theorem AlgEquiv.restrictNormalHom_apply {F : Type u_1} [Field F] {K₁ : Type u_3} [Field K₁] [Algebra F K₁] (L : IntermediateField F K₁) [Normal F ↥L] (σ : K₁ ≃ₐ[F] K₁) (x : ↥L) : ↑(((restrictNormalHom ↥L) σ) x) = σ ↑x

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 := ⋯ }

@[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₁) : (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) : (algHomEquivAut F K₁ E).symm σ = (IsScalarTower.toAlgHom F E K₁).comp ↑σ

@[simp]

theorem AlgEquiv.restrictNormalHom_id (F : Type u_6) (K : Type u_7) [Field F] [Field K] [Algebra F K] [Normal F K] : 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_6) (K₁ : Type u_7) (K₂ : Type u_8) (K₃ : Type u_9) [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_6) (K₂ : Type u_7) {F : Type u_8} {K₃ : Type u_9} [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)