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.
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)
Instances
The normal closure of K/F in L/F.
Equations
- normalClosure F K L = ⨆ (f : K →ₐ[F] L), f.fieldRange
If K/F is algebraic, the "generated by roots" condition in IsNormalClosure can be replaced
by "generated by images of embeddings".
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.
A normal closure of K/F embeds into any L/F
where the minimal polynomials of K/F splits.
Equations
- IsNormalClosure.lift splits = ⋯.some
Normal closures of K/F are unique up to F-algebra isomorphisms.
Equations
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 := ⋯ }
Stacks Tag 0BMG ((1) normality.)
Stacks Tag 0BMG (When L is normal over K, this agrees with 0BMG (1) finiteness.)
Equations
- normalClosure.algebra F K L = (let __src := ⨆ (f : K →ₐ[F] L), f.fieldRange; { toSubsemiring := __src.toSubsemiring, algebraMap_mem' := ⋯, inv_mem' := ⋯ }).algebra'
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' := ⋯ }
normalClosure as a ClosureOperator.
Equations
- One or more equations did not get rendered due to their size.
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)