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.

noncomputable 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 f.factor

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

See note [fact non-instances].

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

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

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

theorem Polynomial.isCoprime_iff_aeval_ne_zero {K : Type v} [Field K] (f g : Polynomial K) : IsCoprime f g ↔ ∀ {A : Type v} [inst : CommRing A] [IsDomain A] [inst_2 : Algebra K A] (a : A), (aeval a) f ≠ 0 ∨ (aeval a) g ≠ 0

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

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 : f.natDegree ≠ 0) : (X - C (AdjoinRoot.root f.factor)) * f.removeFactor = map (AdjoinRoot.of f.factor) f

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

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

noncomputable 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.

@[implicit_reducible]

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

@[implicit_reducible]

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

@[implicit_reducible]

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

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

@[implicit_reducible]

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

@[implicit_reducible]

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

@[implicit_reducible]

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

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

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

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

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

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

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

A splitting field of a polynomial.

@[implicit_reducible]

noncomputable instance Polynomial.instInhabitedSplittingField {K : Type u_1} [Field K] (f : Polynomial K) : Inhabited f.SplittingField

@[implicit_reducible]

noncomputable instance Polynomial.instCommRingSplittingField {K : Type u_1} [Field K] (f : Polynomial K) : CommRing f.SplittingField

@[implicit_reducible]

noncomputable instance Polynomial.instAlgebraSplittingField {K : Type u_1} [Field K] (f : Polynomial K) : Algebra K f.SplittingField

@[implicit_reducible]

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

@[implicit_reducible]

noncomputable instance Polynomial.SplittingField.instAlgebra {K : Type u_2} [Field K] (f : Polynomial K) {R : Type u_1} [CommSemiring R] [Algebra R K] : Algebra R f.SplittingField

@[implicit_reducible]

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

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

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

@[implicit_reducible]

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

@[implicit_reducible]

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

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

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

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

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

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

Stacks Tag 09HU (Splitting part)

noncomputable def Polynomial.SplittingField.lift {K : Type v} {L : Type w} [Field K] [Field L] (f : Polynomial K) [Algebra K L] (hb : (map (algebraMap K L) f).Splits) : f.SplittingField →ₐ[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 (f.rootSet f.SplittingField) = ⊤

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

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

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

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

Any splitting field is isomorphic to SplittingFieldAux f.