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]
:
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.)
- splits : ∀ (x : K), Polynomial.Splits (algebraMap F L) (minpoly F x)
- adjoin_rootSet : ⨆ (x : K), IntermediateField.adjoin F ((minpoly F x).rootSet L) = ⊤
Instances
theorem
IsNormalClosure.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]
[self : IsNormalClosure F K L]
(x : K)
:
Polynomial.Splits (algebraMap F L) (minpoly F x)
theorem
IsNormalClosure.adjoin_rootSet
{F : Type u_1}
{K : Type u_2}
{L : Type u_3}
[Field F]
[Field K]
[Field L]
[Algebra F K]
[Algebra F L]
[self : IsNormalClosure F K L]
:
⨆ (x : K), IntermediateField.adjoin F ((minpoly F x).rootSet 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))
:
A normal closure of K/F embeds into any L/F
where the minimal polynomials of K/F splits.
Equations
- IsNormalClosure.lift splits = let_fun this := ⋯; ⋯.some
Instances For
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']
:
Normal closures of K/F are unique up to F-algebra isomorphisms.
Equations
- IsNormalClosure.equiv = let_fun this := ⋯; AlgEquiv.ofBijective (IsNormalClosure.lift ⋯) ⋯
Instances For
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]
:
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 := ⋯ }
Instances For
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)
Equations
- ⋯ = ⋯
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)
Equations
- ⋯ = ⋯
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
Equations
- ⋯ = ⋯
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']
:
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' = let φ := ⋯.some; let φ' := φ.comp (IntermediateField.inclusion ⋯); { toFun := φ'.comp ∘ ⇑(normalClosure.algHomEquiv F K L').symm, inj' := ⋯ }
Instances For
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), IntermediateField.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), IntermediateField.map (↑f) K
theorem
IntermediateField.normalClosure_mono
{F : Type u_1}
{L : Type u_3}
[Field F]
[Field L]
[Algebra F L]
(K : IntermediateField F L)
(K' : IntermediateField F L)
[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)
[Field F]
[Field L]
[Algebra F L]
[Normal F L]
(K : IntermediateField F L)
:
(IntermediateField.closureOperator F L) K = normalClosure F (↥K) L
@[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)
:
(IntermediateField.closureOperator F L).IsClosed x = (normalClosure F (↥x) L = x)
noncomputable def
IntermediateField.closureOperator
(F : Type u_1)
(L : Type u_3)
[Field F]
[Field L]
[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}
[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_map_le
{F : Type u_1}
{L : Type u_3}
[Field F]
[Field L]
[Algebra F L]
[Normal F L]
{K : IntermediateField F L}
:
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}
:
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}
:
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}
: