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 :

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)

Instances

source

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

source

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)

source

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)

source

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)

source

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

Normal F F

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] [IsScalarTower F K E] [h : Normal F E] :

Normal K E

Stacks Tag 09HN

source

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 ⇑ϕ

source

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'

source

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'

source

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

source

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

Instances For

source

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.

Stacks Tag 0BME (Part 1)

Equations

Instances For

source

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

Instances For

source

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

source

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

source

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

Instances For

source

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

source

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)

source

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

Instances For

source

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

source

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.

Stacks Tag 0BR4

Equations

Instances For

source

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

source

@[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 ↑σ

source

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

source

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₁

source

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)

Documentation

Mathlib.FieldTheory.Normal.Defs

Normal field extensions #

Main Definitions #