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 K
whereK
is a field extension ofF
.
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' : Algebra.IsAlgebraic F K
- splits' : ∀ (x : K), Polynomial.Splits (algebraMap F K) (minpoly F x)
Instances
Equations
- ⋯ = ⋯
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
.
Equations
- ⋯ = ⋯
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' := ⋯ }
Instances For
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₁))
Instances For
Restrict algebra homomorphism to normal subfield (AlgEquiv
version)
Equations
- ϕ.restrictNormal' E = AlgEquiv.ofBijective (ϕ.restrictNormal E) ⋯
Instances For
Restrict algebra isomorphism to a normal subfield
Equations
- χ.restrictNormal E = (↑χ).restrictNormal' E
Instances For
Restriction to a normal subfield as a group homomorphism
Equations
- AlgEquiv.restrictNormalHom E = MonoidHom.mk' (fun (χ : K₁ ≃ₐ[F] K₁) => χ.restrictNormal E) ⋯
Instances For
If K₁/E/F
is a tower of fields with E/F
normal then AlgHom.restrictNormal'
is an
equivalence.
Equations
- One or more equations did not get rendered due to their size.
Instances For
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
Instances For
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) ⋯