# 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) [] [] [] [Algebra F K] [Algebra F L] :

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

Instances
theorem IsNormalClosure.splits {F : Type u_1} {K : Type u_2} {L : Type u_3} [] [] [] [Algebra F K] [Algebra F L] [self : ] (x : K) :
theorem IsNormalClosure.adjoin_rootSet {F : Type u_1} {K : Type u_2} {L : Type u_3} [] [] [] [Algebra F K] [Algebra F L] [self : ] :
⨆ (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) [] [] [] [Algebra F K] [Algebra F L] :

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

Equations
Instances For
theorem normalClosure_def (F : Type u_1) (K : Type u_2) (L : Type u_3) [] [] [] [Algebra F K] [Algebra F L] :
= ⨆ (f : K →ₐ[F] L), f.fieldRange
theorem IsNormalClosure.normal {F : Type u_1} {K : Type u_2} {L : Type u_3} [] [] [] [Algebra F K] [Algebra F L] [h : ] :
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} [] [] [] [Algebra F K] [Algebra F L] {K' : } :
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} [] [] [] [Algebra F K] [Algebra F L] (f : K →ₐ[F] L) :
f.fieldRange
theorem Algebra.IsAlgebraic.normalClosure_le_iSup_adjoin {F : Type u_1} {K : Type u_2} {L : Type u_3} [] [] [] [Algebra F K] [Algebra F 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} [] [] [] [Algebra F K] [Algebra F L] [] (splits : ∀ (x : K), Polynomial.Splits () (minpoly F x)) :
= ⨆ (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} [] [] [] [Algebra F K] [Algebra F L] [] :
(∀ (x : K), Polynomial.Splits () (minpoly F x)) =

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} [] [] [] [Algebra F K] [Algebra F L] [] (splits : ∀ (x : K), Polynomial.Splits () (minpoly F x)) :
IsNormalClosure F K ()

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} [] [] [] [Algebra F K] [Algebra F L] [h : ] {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
Instances For
noncomputable def IsNormalClosure.equiv {F : Type u_1} {K : Type u_2} {L : Type u_3} [] [] [] [Algebra F K] [Algebra F L] {L' : Type u_4} [Field L'] [Algebra F L'] [h : ] [h' : IsNormalClosure F K L'] :
L ≃ₐ[F] L'

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

Equations
• IsNormalClosure.equiv = let_fun this := ;
Instances For
instance isNormalClosure_normalClosure (F : Type u_1) (K : Type u_2) (L : Type u_3) [] [] [] [Algebra F K] [Algebra F L] [ne : Nonempty (K →ₐ[F] L)] [h : Normal F L] :
IsNormalClosure F K ()
Equations
• =
theorem normalClosure_eq_iSup_adjoin' (F : Type u_1) (K : Type u_2) (L : Type u_3) [] [] [] [Algebra F K] [Algebra F L] [ne : Nonempty (K →ₐ[F] L)] [h : Normal F 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) [] [] [] [Algebra F K] [Algebra F L] [Algebra K L] [] [Normal F 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) [] [] [] [Algebra F K] [Algebra F L] :
(K →ₐ[F] ()) (K →ₐ[F] L)

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

Equations
• = { toFun := ().val.comp, invFun := fun (f : K →ₐ[F] L) => f.codRestrict ().toSubalgebra , left_inv := , right_inv := }
Instances For
instance normalClosure.normal (F : Type u_1) (K : Type u_2) (L : Type u_3) [] [] [] [Algebra F K] [Algebra F L] [h : Normal F L] :
Normal F ()
Equations
• =
instance normalClosure.is_finiteDimensional (F : Type u_1) (K : Type u_2) (L : Type u_3) [] [] [] [Algebra F K] [Algebra F L] [] :
Equations
• =
noncomputable instance normalClosure.algebra (F : Type u_1) (K : Type u_2) (L : Type u_3) [] [] [] [Algebra F K] [Algebra F L] [Algebra K L] [] :
Algebra K ()
Equations
• = (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) [] [] [] [Algebra F K] [Algebra F L] [Algebra K L] [] :
IsScalarTower F K ()
Equations
• =
instance normalClosure.instIsScalarTowerSubtypeMemIntermediateField_1 (F : Type u_1) (K : Type u_2) (L : Type u_3) [] [] [] [Algebra F K] [Algebra F L] [Algebra K L] [] :
IsScalarTower K (()) L
Equations
• =
theorem normalClosure.restrictScalars_eq (F : Type u_1) (K : Type u_2) (L : Type u_3) [] [] [] [Algebra F K] [Algebra F L] [Algebra K L] [] :
noncomputable def Algebra.IsAlgebraic.algHomEmbeddingOfSplits {F : Type u_1} {K : Type u_2} {L : Type u_3} [] [] [] [Algebra F K] [Algebra F L] [] (h : ∀ (x : K), Polynomial.Splits () (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
• = let φ := .some; let φ' := φ.comp ; { toFun := φ'.comp ().symm, inj' := }
Instances For
theorem IntermediateField.le_normalClosure {F : Type u_1} {L : Type u_3} [] [] [Algebra F L] (K : ) :
K normalClosure F (K) L
theorem IntermediateField.normalClosure_of_normal {F : Type u_1} {L : Type u_3} [] [] [Algebra F L] (K : ) [Normal F K] :
normalClosure F (K) L = K
theorem IntermediateField.normalClosure_def' {F : Type u_1} {L : Type u_3} [] [] [Algebra F L] (K : ) [Normal F L] :
normalClosure F (K) L = ⨆ (f : L →ₐ[F] L),
theorem IntermediateField.normalClosure_def'' {F : Type u_1} {L : Type u_3} [] [] [Algebra F L] (K : ) [Normal F L] :
normalClosure F (K) L = ⨆ (f : L ≃ₐ[F] L),
theorem IntermediateField.normalClosure_mono {F : Type u_1} {L : Type u_3} [] [] [Algebra F L] (K : ) (K' : ) [Normal F L] (h : K K') :
normalClosure F (K) L normalClosure F (K') L
@[simp]
theorem IntermediateField.closureOperator_apply (F : Type u_1) (L : Type u_3) [] [] [Algebra F L] [Normal F L] (K : ) :
= normalClosure F (K) L
@[simp]
theorem IntermediateField.closureOperator_isClosed (F : Type u_1) (L : Type u_3) [] [] [Algebra F L] [Normal F L] (x : ) :
.IsClosed x = (normalClosure F (x) L = x)
noncomputable def IntermediateField.closureOperator (F : Type u_1) (L : Type u_3) [] [] [Algebra F L] [Normal F L] :

normalClosure as a ClosureOperator.

Equations
• One or more equations did not get rendered due to their size.
Instances For
theorem IntermediateField.normal_iff_normalClosure_eq {F : Type u_1} {L : Type u_3} [] [] [Algebra F L] [Normal F L] {K : } :
Normal F K normalClosure F (K) L = K
theorem IntermediateField.normal_iff_normalClosure_le {F : Type u_1} {L : Type u_3} [] [] [Algebra F L] [Normal F L] {K : } :
Normal F K normalClosure F (K) L K
theorem IntermediateField.normal_iff_forall_fieldRange_le {F : Type u_1} {L : Type u_3} [] [] [Algebra F L] [Normal F L] {K : } :
Normal F K ∀ (σ : K →ₐ[F] L), σ.fieldRange K
theorem IntermediateField.normal_iff_forall_map_le {F : Type u_1} {L : Type u_3} [] [] [Algebra F L] [Normal F L] {K : } :
Normal F K ∀ (σ : L →ₐ[F] L),
theorem IntermediateField.normal_iff_forall_map_le' {F : Type u_1} {L : Type u_3} [] [] [Algebra F L] [Normal F L] {K : } :
Normal F K ∀ (σ : L ≃ₐ[F] L), K
theorem IntermediateField.normal_iff_forall_fieldRange_eq {F : Type u_1} {L : Type u_3} [] [] [Algebra F L] [Normal F L] {K : } :
Normal F K ∀ (σ : K →ₐ[F] L), σ.fieldRange = K
theorem IntermediateField.normal_iff_forall_map_eq {F : Type u_1} {L : Type u_3} [] [] [Algebra F L] [Normal F L] {K : } :
Normal F K ∀ (σ : L →ₐ[F] L),
theorem IntermediateField.normal_iff_forall_map_eq' {F : Type u_1} {L : Type u_3} [] [] [Algebra F L] [Normal F L] {K : } :
Normal F K ∀ (σ : L ≃ₐ[F] L), = K