Normal closures

Main definitions

Given field extensions K/F and L/F, the predicate IsNormalClosure F K L says that the minimal polynomial of every element of K over F splits in L, and that L is generated by the roots of such minimal polynomials. These conditions uniquely characterize L/F up to F-algebra isomorphisms (IsNormalClosure.equiv).

The explicit construction normalClosure F K L of a field extension K/F inside another field extension L/F is the smallest intermediate field of L/F that contains the image of every F-algebra embedding K →ₐ[F] L. It satisfies the IsNormalClosure predicate if L/F satisfies the abovementioned splitting condition, in particular if L/K/F form a tower and L/F is normal.

class IsNormalClosure (F : Type u_1) (K : Type u_2) (L : Type u_3) [Field F] [Field K] [Field L] [Algebra F K] [Algebra F L] : Prop

L/F is a normal closure of K/F if the minimal polynomial of every element of K over F splits in L, and L is generated by roots of such minimal polynomials over F. (Since the minimal polynomial of a transcendental element is 0, the normal closure of K/F is the same as the normal closure over F of the algebraic closure of F in K.)

Stacks Tag 0BMF (Predicate version)

• splits (x : K) : Polynomial.Splits (algebraMap F L) (minpoly F x)
• adjoin_rootSet : ⨆ (x : K), IntermediateField.adjoin F ((minpoly F x).rootSet L) = ⊤

noncomputable def normalClosure (F : Type u_1) (K : Type u_2) (L : Type u_3) [Field F] [Field K] [Field L] [Algebra F K] [Algebra F L] : IntermediateField F L

The normal closure of K/F in L/F.

Stacks Tag 0BMF

Equations

• normalClosure F K L = ⨆ (f : K →ₐ[F] L), f.fieldRange

theorem normalClosure_def (F : Type u_1) (K : Type u_2) (L : Type u_3) [Field F] [Field K] [Field L] [Algebra F K] [Algebra F L] : normalClosure F K L = ⨆ (f : K →ₐ[F] L), f.fieldRange

theorem IsNormalClosure.normal {F : Type u_1} {K : Type u_2} {L : Type u_3} [Field F] [Field K] [Field L] [Algebra F K] [Algebra F L] [h : IsNormalClosure F K L] : Normal F L

A normal closure is always normal.

theorem normalClosure_le_iff {F : Type u_1} {K : Type u_2} {L : Type u_3} [Field F] [Field K] [Field L] [Algebra F K] [Algebra F L] {K' : IntermediateField F L} : normalClosure F K L ≤ K' ↔ ∀ (f : K →ₐ[F] L), f.fieldRange ≤ K'

theorem AlgHom.fieldRange_le_normalClosure {F : Type u_1} {K : Type u_2} {L : Type u_3} [Field F] [Field K] [Field L] [Algebra F K] [Algebra F L] (f : K →ₐ[F] L) : f.fieldRange ≤ normalClosure F K L

theorem Algebra.IsAlgebraic.normalClosure_le_iSup_adjoin {F : Type u_1} {K : Type u_2} {L : Type u_3} [Field F] [Field K] [Field L] [Algebra F K] [Algebra F L] [Algebra.IsAlgebraic F K] : normalClosure F K L ≤ ⨆ (x : K), IntermediateField.adjoin F ((minpoly F x).rootSet L)

theorem Algebra.IsAlgebraic.normalClosure_eq_iSup_adjoin_of_splits {F : Type u_1} {K : Type u_2} {L : Type u_3} [Field F] [Field K] [Field L] [Algebra F K] [Algebra F L] [Algebra.IsAlgebraic F K] (splits : ∀ (x : K), Polynomial.Splits (algebraMap F L) (minpoly F x)) : normalClosure F K L = ⨆ (x : K), IntermediateField.adjoin F ((minpoly F x).rootSet L)

theorem Algebra.IsAlgebraic.isNormalClosure_iff {F : Type u_1} {K : Type u_2} {L : Type u_3} [Field F] [Field K] [Field L] [Algebra F K] [Algebra F L] [Algebra.IsAlgebraic F K] : IsNormalClosure F K L ↔ (∀ (x : K), Polynomial.Splits (algebraMap F L) (minpoly F x)) ∧ normalClosure F K L = ⊤

If K/F is algebraic, the "generated by roots" condition in IsNormalClosure can be replaced by "generated by images of embeddings".

theorem Algebra.IsAlgebraic.isNormalClosure_normalClosure {F : Type u_1} {K : Type u_2} {L : Type u_3} [Field F] [Field K] [Field L] [Algebra F K] [Algebra F L] [Algebra.IsAlgebraic F K] (splits : ∀ (x : K), Polynomial.Splits (algebraMap F L) (minpoly F x)) : IsNormalClosure F K ↥(normalClosure F K L)

normalClosure F K L is a valid normal closure if K/F is algebraic and all minimal polynomials of K/F splits in L/F.

noncomputable def IsNormalClosure.lift {F : Type u_1} {K : Type u_2} {L : Type u_3} [Field F] [Field K] [Field L] [Algebra F K] [Algebra F L] [h : IsNormalClosure F K L] {L' : Type u_4} [Field L'] [Algebra F L'] (splits : ∀ (x : K), Polynomial.Splits (algebraMap F L') (minpoly F x)) : L →ₐ[F] L'

A normal closure of K/F embeds into any L/F where the minimal polynomials of K/F splits.

Equations

• IsNormalClosure.lift splits = ⋯.some

noncomputable def IsNormalClosure.equiv {F : Type u_1} {K : Type u_2} {L : Type u_3} [Field F] [Field K] [Field L] [Algebra F K] [Algebra F L] {L' : Type u_4} [Field L'] [Algebra F L'] [h : IsNormalClosure F K L] [h' : IsNormalClosure F K L'] : L ≃ₐ[F] L'

Normal closures of K/F are unique up to F-algebra isomorphisms.

Equations

• IsNormalClosure.equiv = AlgEquiv.ofBijective (IsNormalClosure.lift ⋯) ⋯

instance isNormalClosure_normalClosure (F : Type u_1) (K : Type u_2) (L : Type u_3) [Field F] [Field K] [Field L] [Algebra F K] [Algebra F L] [ne : Nonempty (K →ₐ[F] L)] [h : Normal F L] : IsNormalClosure F K ↥(normalClosure F K L)

theorem normalClosure_eq_iSup_adjoin' (F : Type u_1) (K : Type u_2) (L : Type u_3) [Field F] [Field K] [Field L] [Algebra F K] [Algebra F L] [ne : Nonempty (K →ₐ[F] L)] [h : Normal F L] : normalClosure F K L = ⨆ (x : K), IntermediateField.adjoin F ((minpoly F x).rootSet L)

theorem normalClosure_eq_iSup_adjoin (F : Type u_1) (K : Type u_2) (L : Type u_3) [Field F] [Field K] [Field L] [Algebra F K] [Algebra F L] [Algebra K L] [IsScalarTower F K L] [Normal F L] : normalClosure F K L = ⨆ (x : K), IntermediateField.adjoin F ((minpoly F x).rootSet L)

noncomputable def normalClosure.algHomEquiv (F : Type u_1) (K : Type u_2) (L : Type u_3) [Field F] [Field K] [Field L] [Algebra F K] [Algebra F L] : (K →ₐ[F] ↥(normalClosure F K L)) ≃ (K →ₐ[F] L)

All F-AlgHoms from K to L factor through the normal closure of K/F in L/F.

Equations

• normalClosure.algHomEquiv F K L = { toFun := (normalClosure F K L).val.comp, invFun := fun (f : K →ₐ[F] L) => f.codRestrict (normalClosure F K L).toSubalgebra ⋯, left_inv := ⋯, right_inv := ⋯ }

instance normalClosure.normal (F : Type u_1) (K : Type u_2) (L : Type u_3) [Field F] [Field K] [Field L] [Algebra F K] [Algebra F L] [h : Normal F L] : Normal F ↥(normalClosure F K L)

Stacks Tag 0BMG ((1) normality.)

instance normalClosure.is_finiteDimensional (F : Type u_1) (K : Type u_2) (L : Type u_3) [Field F] [Field K] [Field L] [Algebra F K] [Algebra F L] [FiniteDimensional F K] : FiniteDimensional F ↥(normalClosure F K L)

Stacks Tag 0BMG (When L is normal over K, this agrees with 0BMG (1) finiteness.)

noncomputable instance normalClosure.algebra (F : Type u_1) (K : Type u_2) (L : Type u_3) [Field F] [Field K] [Field L] [Algebra F K] [Algebra F L] [Algebra K L] [IsScalarTower F K L] : Algebra K ↥(normalClosure F K L)

Equations

• normalClosure.algebra F K L = (let __src := ⨆ (f : K →ₐ[F] L), f.fieldRange; { toSubsemiring := __src.toSubsemiring, algebraMap_mem' := ⋯, inv_mem' := ⋯ }).algebra'

instance normalClosure.instIsScalarTowerSubtypeMemIntermediateField (F : Type u_1) (K : Type u_2) (L : Type u_3) [Field F] [Field K] [Field L] [Algebra F K] [Algebra F L] [Algebra K L] [IsScalarTower F K L] : IsScalarTower F K ↥(normalClosure F K L)

instance normalClosure.instIsScalarTowerSubtypeMemIntermediateField_1 (F : Type u_1) (K : Type u_2) (L : Type u_3) [Field F] [Field K] [Field L] [Algebra F K] [Algebra F L] [Algebra K L] [IsScalarTower F K L] : IsScalarTower K (↥(normalClosure F K L)) L

theorem normalClosure.restrictScalars_eq (F : Type u_1) (K : Type u_2) (L : Type u_3) [Field F] [Field K] [Field L] [Algebra F K] [Algebra F L] [Algebra K L] [IsScalarTower F K L] : IntermediateField.restrictScalars F (IsScalarTower.toAlgHom K (↥(normalClosure F K L)) L).fieldRange = normalClosure F K L

noncomputable def Algebra.IsAlgebraic.algHomEmbeddingOfSplits {F : Type u_1} {K : Type u_2} {L : Type u_3} [Field F] [Field K] [Field L] [Algebra F K] [Algebra F L] [Algebra.IsAlgebraic F K] (h : ∀ (x : K), Polynomial.Splits (algebraMap F L) (minpoly F x)) (L' : Type u_4) [Field L'] [Algebra F L'] : (K →ₐ[F] L') ↪ K →ₐ[F] L

An extension L/F in which every minimal polynomial of K/F splits is maximal with respect to F-embeddings of K, in the sense that K →ₐ[F] L achieves maximal cardinality. We construct an explicit injective function from an arbitrary K →ₐ[F] L' into K →ₐ[F] L, using an embedding of normalClosure F K L' into L.

Equations

• Algebra.IsAlgebraic.algHomEmbeddingOfSplits h L' = { toFun := (⋯.some.comp (IntermediateField.inclusion ⋯)).comp ∘ ⇑(normalClosure.algHomEquiv F K L').symm, inj' := ⋯ }

theorem IntermediateField.le_normalClosure {F : Type u_1} {L : Type u_3} [Field F] [Field L] [Algebra F L] (K : IntermediateField F L) : K ≤ normalClosure F (↥K) L

theorem IntermediateField.normalClosure_of_normal {F : Type u_1} {L : Type u_3} [Field F] [Field L] [Algebra F L] (K : IntermediateField F L) [Normal F ↥K] : normalClosure F (↥K) L = K

theorem IntermediateField.normalClosure_def' {F : Type u_1} {L : Type u_3} [Field F] [Field L] [Algebra F L] (K : IntermediateField F L) [Normal F L] : normalClosure F (↥K) L = ⨆ (f : L →ₐ[F] L), map f K

theorem IntermediateField.normalClosure_def'' {F : Type u_1} {L : Type u_3} [Field F] [Field L] [Algebra F L] (K : IntermediateField F L) [Normal F L] : normalClosure F (↥K) L = ⨆ (f : L ≃ₐ[F] L), map (↑f) K

theorem IntermediateField.normalClosure_mono {F : Type u_1} {L : Type u_3} [Field F] [Field L] [Algebra F L] (K K' : IntermediateField F L) [Normal F L] (h : K ≤ K') : normalClosure F (↥K) L ≤ normalClosure F (↥K') L

noncomputable def IntermediateField.closureOperator (F : Type u_1) (L : Type u_3) [Field F] [Field L] [Algebra F L] [Normal F L] : ClosureOperator (IntermediateField F L)

normalClosure as a ClosureOperator.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem IntermediateField.closureOperator_isClosed (F : Type u_1) (L : Type u_3) [Field F] [Field L] [Algebra F L] [Normal F L] (x : IntermediateField F L) : (closureOperator F L).IsClosed x = (normalClosure F (↥x) L = x)

@[simp]

theorem IntermediateField.closureOperator_apply (F : Type u_1) (L : Type u_3) [Field F] [Field L] [Algebra F L] [Normal F L] (K : IntermediateField F L) : (closureOperator F L) K = normalClosure F (↥K) L

theorem IntermediateField.normal_iff_normalClosure_eq {F : Type u_1} {L : Type u_3} [Field F] [Field L] [Algebra F L] [Normal F L] {K : IntermediateField F L} : Normal F ↥K ↔ normalClosure F (↥K) L = K

theorem IntermediateField.normal_iff_normalClosure_le {F : Type u_1} {L : Type u_3} [Field F] [Field L] [Algebra F L] [Normal F L] {K : IntermediateField F L} : Normal F ↥K ↔ normalClosure F (↥K) L ≤ K

theorem IntermediateField.normal_iff_forall_fieldRange_le {F : Type u_1} {L : Type u_3} [Field F] [Field L] [Algebra F L] [Normal F L] {K : IntermediateField F L} : Normal F ↥K ↔ ∀ (σ : ↥K →ₐ[F] L), σ.fieldRange ≤ K

theorem IntermediateField.normal_iff_forall_map_le {F : Type u_1} {L : Type u_3} [Field F] [Field L] [Algebra F L] [Normal F L] {K : IntermediateField F L} : Normal F ↥K ↔ ∀ (σ : L →ₐ[F] L), map σ K ≤ K

theorem IntermediateField.normal_iff_forall_map_le' {F : Type u_1} {L : Type u_3} [Field F] [Field L] [Algebra F L] [Normal F L] {K : IntermediateField F L} : Normal F ↥K ↔ ∀ (σ : L ≃ₐ[F] L), map (↑σ) K ≤ K

theorem IntermediateField.normal_iff_forall_fieldRange_eq {F : Type u_1} {L : Type u_3} [Field F] [Field L] [Algebra F L] [Normal F L] {K : IntermediateField F L} : Normal F ↥K ↔ ∀ (σ : ↥K →ₐ[F] L), σ.fieldRange = K

If L/K/F is a field tower where L/F is normal, then K is normal over F if and only if σ(K) = K for every σ ∈ K →ₐ[F] L.

Stacks Tag 09HQ (stronger version replacing an algebraic closure by a normal extension)

theorem IntermediateField.normal_iff_forall_map_eq {F : Type u_1} {L : Type u_3} [Field F] [Field L] [Algebra F L] [Normal F L] {K : IntermediateField F L} : Normal F ↥K ↔ ∀ (σ : L →ₐ[F] L), map σ K = K

theorem IntermediateField.normal_iff_forall_map_eq' {F : Type u_1} {L : Type u_3} [Field F] [Field L] [Algebra F L] [Normal F L] {K : IntermediateField F L} : Normal F ↥K ↔ ∀ (σ : L ≃ₐ[F] L), map (↑σ) K = K

@[simp]

theorem IntermediateField.normalClosure_map_eq {F : Type u_1} {L : Type u_3} [Field F] [Field L] [Algebra F L] [Normal F L] (K : IntermediateField F L) (σ : L →ₐ[F] L) : normalClosure F (↥(map σ K)) L = normalClosure F (↥K) L

@[simp]

theorem IntermediateField.normalClosure_le_iff_of_normal {F : Type u_1} {L : Type u_3} [Field F] [Field L] [Algebra F L] [Normal F L] {K₁ K₂ : IntermediateField F L} [Normal F ↥K₂] : normalClosure F (↥K₁) L ≤ K₂ ↔ K₁ ≤ K₂