Normal field extensions #
In this file we define normal field extensions and prove that for a finite extension, being normal
is the same as being a splitting field (Normal.of_isSplittingField and
Normal.exists_isSplittingField).
Main Definitions #
Normal F KwhereKis a field extension ofF.
class
Normal
(F : Type u_1)
(K : Type u_2)
[Field F]
[Field K]
[Algebra F K]
extends
Algebra.IsAlgebraic
:
Typeclass for normal field extension: K is a normal extension of F iff the minimal
polynomial of every element x in K splits in K, i.e. every conjugate of x is in K.
- isAlgebraic : ∀ (x : K), IsAlgebraic F x
- splits' : ∀ (x : K), Polynomial.Splits (algebraMap F K) (minpoly F x)
theorem
Normal.splits'
{F : Type u_1}
{K : Type u_2}
:
∀ {inst : Field F} {inst_1 : Field K} {inst_2 : Algebra F K} [self : Normal F K] (x : K),
Polynomial.Splits (algebraMap F K) (minpoly F x)
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
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)
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)
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)
theorem
Normal.exists_isSplittingField
(F : Type u_1)
(K : Type u_2)
[Field F]
[Field K]
[Algebra F K]
[h : Normal F K]
[FiniteDimensional F K]
:
∃ (p : Polynomial F), Polynomial.IsSplittingField F K p
theorem
Normal.of_isSplittingField
{F : Type u_1}
[Field F]
{E : Type u_3}
[Field E]
[Algebra F E]
(p : Polynomial F)
[hFEp : Polynomial.IsSplittingField F E p]
:
Normal F E
instance
Polynomial.SplittingField.instNormal
{F : Type u_1}
[Field F]
(p : Polynomial F)
:
Normal F p.SplittingField
Equations
- ⋯ = ⋯
theorem
IntermediateField.splits_of_mem_adjoin
(F : Type u_1)
(K : Type u_2)
[Field F]
[Field K]
[Algebra F K]
{L : Type u_3}
[Field L]
[Algebra F L]
{S : Set K}
(splits : ∀ x ∈ S, IsIntegral F x ∧ Polynomial.Splits (algebraMap F L) (minpoly F x))
{x : K}
(hx : x ∈ IntermediateField.adjoin F S)
:
Polynomial.Splits (algebraMap F L) (minpoly F x)
If a set of algebraic elements in a field extension K/F have minimal polynomials that
split in another extension L/F, then all minimal polynomials in the intermediate field
generated by the set also split in L/F.
instance
IntermediateField.normal_sup
(F : Type u_1)
(K : Type u_2)
[Field F]
[Field K]
[Algebra F K]
(E : IntermediateField F K)
(E' : IntermediateField F K)
[Normal F ↥E]
[Normal F ↥E']
:
Equations
- ⋯ = ⋯
instance
IntermediateField.normal_inf
(F : Type u_1)
(K : Type u_2)
[Field F]
[Field K]
[Algebra F K]
(E : IntermediateField F K)
(E' : IntermediateField F K)
[Normal F ↥E]
[Normal F ↥E']
:
Equations
- ⋯ = ⋯
@[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 ↥(IntermediateField.restrictScalars F E) ↔ Normal F ↥E
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' := ⋯ }
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]
:
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₁))
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]
:
Restrict algebra homomorphism to normal subfield (AlgEquiv version)
Equations
- ϕ.restrictNormal' E = AlgEquiv.ofBijective (ϕ.restrictNormal E) ⋯
@[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)
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
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]
:
Restrict algebra isomorphism to a normal subfield
Equations
- χ.restrictNormal E = (↑χ).restrictNormal' E
@[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)
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)
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]
:
Restriction to a normal subfield as a group homomorphism
Equations
- AlgEquiv.restrictNormalHom E = MonoidHom.mk' (fun (χ : K₁ ≃ₐ[F] K₁) => χ.restrictNormal E) ⋯
@[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]
(σ : E ≃ₐ[F] E)
:
(Normal.algHomEquivAut F K₁ E).symm σ = (IsScalarTower.toAlgHom F E K₁).comp ↑σ
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]
:
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 (σ : E ≃ₐ[F] E) => (IsScalarTower.toAlgHom F E K₁).comp ↑σ, left_inv := ⋯, right_inv := ⋯ }
noncomputable def
AlgHom.liftNormal
{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 K₁ E]
[Algebra K₂ E]
[IsScalarTower F K₁ E]
[IsScalarTower F K₂ E]
[h : Normal F E]
:
If E/Kᵢ/F are towers of fields with E/F normal then we can lift
an algebra homomorphism ϕ : K₁ →ₐ[F] K₂ to ϕ.liftNormal E : E →ₐ[F] E.
Equations
- ϕ.liftNormal E = AlgHom.restrictScalars F ⋯.some
@[simp]
theorem
AlgHom.liftNormal_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 K₁ E]
[Algebra K₂ E]
[IsScalarTower F K₁ E]
[IsScalarTower F K₂ E]
[Normal F E]
(x : K₁)
:
(ϕ.liftNormal E) ((algebraMap K₁ E) x) = (algebraMap K₂ E) (ϕ x)
noncomputable def
AlgEquiv.liftNormal
{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 K₁ E]
[Algebra K₂ E]
[IsScalarTower F K₁ E]
[IsScalarTower F K₂ E]
[Normal F E]
:
If E/Kᵢ/F are towers of fields with E/F normal then we can lift
an algebra isomorphism ϕ : K₁ ≃ₐ[F] K₂ to ϕ.liftNormal E : E ≃ₐ[F] E.
Equations
- χ.liftNormal E = AlgEquiv.ofBijective ((↑χ).liftNormal E) ⋯
@[simp]
theorem
AlgEquiv.liftNormal_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 K₁ E]
[Algebra K₂ E]
[IsScalarTower F K₁ E]
[IsScalarTower F K₂ E]
[Normal F E]
(x : K₁)
:
(χ.liftNormal E) ((algebraMap K₁ E) x) = (algebraMap K₂ E) (χ x)
theorem
isSolvable_of_isScalarTower
(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 K₁ E]
[IsScalarTower F K₁ E]
[Normal F K₁]
[h1 : IsSolvable (K₁ ≃ₐ[F] K₁)]
[h2 : IsSolvable (E ≃ₐ[K₁] E)]
:
IsSolvable (E ≃ₐ[F] E)
theorem
minpoly.exists_algEquiv_of_root
{K : Type u_6}
{L : Type u_7}
[Field K]
[Field L]
[Algebra K L]
[Normal K L]
{x : L}
{y : L}
(hy : IsAlgebraic K y)
(h_ev : (Polynomial.aeval x) (minpoly K y) = 0)
:
If x : L is a root of minpoly K y, then we can find (σ : L ≃ₐ[K] L) with σ x = y.
That is, x and y are Galois conjugates.
theorem
minpoly.exists_algEquiv_of_root'
{K : Type u_6}
{L : Type u_7}
[Field K]
[Field L]
[Algebra K L]
[Normal K L]
{x : L}
{y : L}
(hy : IsAlgebraic K y)
(h_ev : (Polynomial.aeval x) (minpoly K y) = 0)
:
If x : L is a root of minpoly K y, then we can find (σ : L ≃ₐ[K] L) with σ y = x.
That is, x and y are Galois conjugates.