Splitting fields

In this file we prove the existence and uniqueness of splitting fields.

Main definitions

• Polynomial.SplittingField f: A fixed splitting field of the polynomial f.

Main statements

• Polynomial.IsSplittingField.algEquiv: Every splitting field of a polynomial f is isomorphic to SplittingField f and thus, being a splitting field is unique up to isomorphism.

Implementation details

We construct a SplittingFieldAux without worrying about whether the instances satisfy nice definitional equalities. Then the actual SplittingField is defined to be a quotient of a MvPolynomial ring by the kernel of the obvious map into SplittingFieldAux. Because the actual SplittingField will be a quotient of a MvPolynomial, it has nice instances on it.

def Polynomial.factor {K : Type v} [Field K] (f : Polynomial K) : Polynomial K

Non-computably choose an irreducible factor from a polynomial.

theorem Polynomial.irreducible_factor {K : Type v} [Field K] (f : Polynomial K) : Irreducible (Polynomial.factor f)

theorem Polynomial.fact_irreducible_factor {K : Type v} [Field K] (f : Polynomial K) : Fact (Irreducible (Polynomial.factor f))

See note [fact non-instances].

theorem Polynomial.factor_dvd_of_not_isUnit {K : Type v} [Field K] {f : Polynomial K} (hf1 : ¬IsUnit f) : Polynomial.factor f ∣ f

theorem Polynomial.factor_dvd_of_degree_ne_zero {K : Type v} [Field K] {f : Polynomial K} (hf : Polynomial.degree f ≠ 0) : Polynomial.factor f ∣ f

theorem Polynomial.factor_dvd_of_natDegree_ne_zero {K : Type v} [Field K] {f : Polynomial K} (hf : Polynomial.natDegree f ≠ 0) : Polynomial.factor f ∣ f

def Polynomial.removeFactor {K : Type v} [Field K] (f : Polynomial K) : Polynomial (AdjoinRoot (Polynomial.factor f))

Divide a polynomial f by X - C r where r is a root of f in a bigger field extension.

theorem Polynomial.X_sub_C_mul_removeFactor {K : Type v} [Field K] (f : Polynomial K) (hf : Polynomial.natDegree f ≠ 0) : (Polynomial.X - ↑Polynomial.C (AdjoinRoot.root (Polynomial.factor f))) * Polynomial.removeFactor f = Polynomial.map (AdjoinRoot.of (Polynomial.factor f)) f

theorem Polynomial.natDegree_removeFactor {K : Type v} [Field K] (f : Polynomial K) : Polynomial.natDegree (Polynomial.removeFactor f) = Polynomial.natDegree f - 1

theorem Polynomial.natDegree_removeFactor' {K : Type v} [Field K] {f : Polynomial K} {n : ℕ} (hfn : Polynomial.natDegree f = n + 1) : Polynomial.natDegree (Polynomial.removeFactor f) = n

def Polynomial.SplittingFieldAuxAux (n : ℕ) {K : Type u} [Field K] : Polynomial K → (L : Type u) × (x : Field L) × Algebra K L

Auxiliary construction to a splitting field of a polynomial, which removes n (arbitrarily-chosen) factors.

It constructs the type, proves that is a field and algebra over the base field.

Uses recursion on the degree.

def Polynomial.SplittingFieldAux (n : ℕ) {K : Type u} [Field K] (f : Polynomial K) : Type u

Auxiliary construction to a splitting field of a polynomial, which removes n (arbitrarily-chosen) factors. It is the type constructed in SplittingFieldAuxAux.

instance Polynomial.SplittingFieldAux.field (n : ℕ) {K : Type u} [Field K] (f : Polynomial K) : Field (Polynomial.SplittingFieldAux n f)

instance Polynomial.instInhabitedSplittingFieldAux (n : ℕ) {K : Type u} [Field K] (f : Polynomial K) : Inhabited (Polynomial.SplittingFieldAux n f)

instance Polynomial.SplittingFieldAux.algebra (n : ℕ) {K : Type u} [Field K] (f : Polynomial K) : Algebra K (Polynomial.SplittingFieldAux n f)

theorem Polynomial.SplittingFieldAux.succ {K : Type v} [Field K] (n : ℕ) (f : Polynomial K) : Polynomial.SplittingFieldAux (n + 1) f = Polynomial.SplittingFieldAux n (Polynomial.removeFactor f)

instance Polynomial.SplittingFieldAux.algebra''' {K : Type v} [Field K] {n : ℕ} {f : Polynomial K} : Algebra (AdjoinRoot (Polynomial.factor f)) (Polynomial.SplittingFieldAux n (Polynomial.removeFactor f))

instance Polynomial.SplittingFieldAux.algebra' {K : Type v} [Field K] {n : ℕ} {f : Polynomial K} : Algebra (AdjoinRoot (Polynomial.factor f)) (Polynomial.SplittingFieldAux (Nat.succ n) f)

instance Polynomial.SplittingFieldAux.algebra'' {K : Type v} [Field K] {n : ℕ} {f : Polynomial K} : Algebra K (Polynomial.SplittingFieldAux n (Polynomial.removeFactor f))

instance Polynomial.SplittingFieldAux.scalar_tower' {K : Type v} [Field K] {n : ℕ} {f : Polynomial K} : IsScalarTower K (AdjoinRoot (Polynomial.factor f)) (Polynomial.SplittingFieldAux n (Polynomial.removeFactor f))

theorem Polynomial.SplittingFieldAux.algebraMap_succ {K : Type v} [Field K] (n : ℕ) (f : Polynomial K) : algebraMap K (Polynomial.SplittingFieldAux (n + 1) f) = RingHom.comp (algebraMap (AdjoinRoot (Polynomial.factor f)) (Polynomial.SplittingFieldAux n (Polynomial.removeFactor f))) (AdjoinRoot.of (Polynomial.factor f))

theorem Polynomial.SplittingFieldAux.splits (n : ℕ) {K : Type u} [Field K] (f : Polynomial K) (_hfn : Polynomial.natDegree f = n) : Polynomial.Splits (algebraMap K (Polynomial.SplittingFieldAux n f)) f

theorem Polynomial.SplittingFieldAux.adjoin_rootSet (n : ℕ) {K : Type u} [Field K] (f : Polynomial K) (_hfn : Polynomial.natDegree f = n) : Algebra.adjoin K (Polynomial.rootSet f (Polynomial.SplittingFieldAux n f)) = ⊤

instance Polynomial.SplittingFieldAux.instIsSplittingFieldSplittingFieldAuxNatDegreeToSemiringToDivisionSemiringToSemifieldFieldAlgebra {K : Type v} [Field K] (f : Polynomial K) : Polynomial.IsSplittingField K (Polynomial.SplittingFieldAux (Polynomial.natDegree f) f) f

def Polynomial.SplittingField {K : Type v} [Field K] (f : Polynomial K) : Type v

A splitting field of a polynomial.

instance Polynomial.SplittingField.commRing {K : Type v} [Field K] (f : Polynomial K) : CommRing (Polynomial.SplittingField f)

instance Polynomial.SplittingField.inhabited {K : Type v} [Field K] (f : Polynomial K) : Inhabited (Polynomial.SplittingField f)

instance Polynomial.SplittingField.instSMulSplittingField {K : Type v} [Field K] (f : Polynomial K) {S : Type u_1} [DistribSMul S K] [IsScalarTower S K K] : SMul S (Polynomial.SplittingField f)

instance Polynomial.SplittingField.algebra {K : Type v} [Field K] (f : Polynomial K) : Algebra K (Polynomial.SplittingField f)

instance Polynomial.SplittingField.algebra' {K : Type v} [Field K] (f : Polynomial K) {R : Type u_1} [CommSemiring R] [Algebra R K] : Algebra R (Polynomial.SplittingField f)

instance Polynomial.SplittingField.isScalarTower {K : Type v} [Field K] (f : Polynomial K) {R : Type u_1} [CommSemiring R] [Algebra R K] : IsScalarTower R K (Polynomial.SplittingField f)

def Polynomial.SplittingField.algEquivSplittingFieldAux {K : Type v} [Field K] (f : Polynomial K) : Polynomial.SplittingField f ≃ₐ[K] Polynomial.SplittingFieldAux (Polynomial.natDegree f) f

The algebra equivalence with SplittingFieldAux, which we will use to construct the field structure.

instance Polynomial.SplittingField.instFieldSplittingField {K : Type v} [Field K] (f : Polynomial K) : Field (Polynomial.SplittingField f)

instance Polynomial.SplittingField.instCharZero {K : Type v} [Field K] (f : Polynomial K) [CharZero K] : CharZero (Polynomial.SplittingField f)

instance Polynomial.SplittingField.instCharP {K : Type v} [Field K] (f : Polynomial K) (p : ℕ) [CharP K p] : CharP (Polynomial.SplittingField f) p

instance Polynomial.IsSplittingField.splittingField {K : Type v} [Field K] (f : Polynomial K) : Polynomial.IsSplittingField K (Polynomial.SplittingField f) f

theorem Polynomial.SplittingField.splits {K : Type v} [Field K] (f : Polynomial K) : Polynomial.Splits (algebraMap K (Polynomial.SplittingField f)) f

def Polynomial.SplittingField.lift {K : Type v} {L : Type w} [Field K] [Field L] (f : Polynomial K) [Algebra K L] (hb : Polynomial.Splits (algebraMap K L) f) : Polynomial.SplittingField f →ₐ[K] L

Embeds the splitting field into any other field that splits the polynomial.

theorem Polynomial.SplittingField.adjoin_rootSet {K : Type v} [Field K] (f : Polynomial K) : Algebra.adjoin K (Polynomial.rootSet f (Polynomial.SplittingField f)) = ⊤

instance Polynomial.IsSplittingField.instFiniteDimensionalSplittingFieldToDivisionRingToAddCommGroupToRingInstFieldSplittingFieldToModuleToCommSemiringToSemifieldToSemiringToDivisionSemiringAlgebra'Id {K : Type v} [Field K] (f : Polynomial K) : FiniteDimensional K (Polynomial.SplittingField f)

instance Polynomial.IsSplittingField.instFintypeSplittingField {K : Type v} [Field K] [Fintype K] (f : Polynomial K) : Fintype (Polynomial.SplittingField f)

instance Polynomial.IsSplittingField.instNoZeroSMulDivisorsSplittingFieldToZeroToCommMonoidWithZeroToCommGroupWithZeroToSemifieldInstFieldSplittingFieldInstSMulSplittingFieldToDistribSMulToMonoidToMonoidWithZeroToSemiringToDivisionSemiringToAddMonoidToAddMonoidWithOneToAddGroupWithOneToRingToDivisionRingToDistribMulActionToAddCommMonoidToNonUnitalNonAssocSemiringToNonUnitalNonAssocRingToNonAssocRingToModuleRightToCommSemiringToSemiringId {K : Type v} [Field K] (f : Polynomial K) : NoZeroSMulDivisors K (Polynomial.SplittingField f)

def Polynomial.IsSplittingField.algEquiv {K : Type v} (L : Type w) [Field K] [Field L] [Algebra K L] (f : Polynomial K) [Polynomial.IsSplittingField K L f] : L ≃ₐ[K] Polynomial.SplittingField f

Any splitting field is isomorphic to SplittingFieldAux f.

instance Polynomial.SplittingField.instNormal {F : Type u} [Field F] (p : Polynomial F) : Normal F (Polynomial.SplittingField p)