# Normal field extensions #

In this file we define normal field extensions.

## Main Definitions #

- `Normal F K` where `K` is a field extension of `F`.

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

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

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

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.

Equations

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

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] :
Gal(E/F)

Restrict algebra homomorphism to normal subfield (`AlgEquiv` version)

Equations

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

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] :
Gal(E/F)

Restrict algebra isomorphism to a normal subfield

Equations

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

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] :
Gal(K₁/F) →* Gal(E/F)

Restriction to a normal subfield as a group homomorphism

Equations

- AlgEquiv.restrictNormalHom E = MonoidHom.mk' (fun (χ : Gal(K₁/F)) => χ.restrictNormal E) ⋯

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] (σ : Gal(K₁/F)) (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₁) ≃ Gal(E/F)

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 (σ : Gal(E/F)) => (IsScalarTower.toAlgHom F E K₁).comp ↑σ, left_inv := ⋯, right_inv := ⋯ }

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] (σ : Gal(E/F)) :
(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 Gal(K/F)

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 : Gal(K₃/F)) :
(AlgEquiv.restrictNormalHom K₁) f = (AlgEquiv.restrictNormalHom K₁) ((AlgEquiv.restrictNormalHom K₂) f)