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.

Equations

• f.factor = if H : ∃ (g : Polynomial K), Irreducible g ∧ g ∣ f then Classical.choose H else Polynomial.X

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 : Polynomial K) (g : Polynomial K) : IsCoprime f g ↔ ∀ {A : Type v} [inst : CommRing A] [inst_1 : IsDomain A] [inst_2 : Algebra K A] (a : A), (Polynomial.aeval a) f ≠ 0 ∨ (Polynomial.aeval a) g ≠ 0

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.

Equations

• f.removeFactor = Polynomial.map (AdjoinRoot.of f.factor) f /ₘ (Polynomial.X - Polynomial.C (AdjoinRoot.root f.factor))

theorem Polynomial.X_sub_C_mul_removeFactor {K : Type v} [Field K] (f : Polynomial K) (hf : f.natDegree ≠ 0) : (Polynomial.X - Polynomial.C (AdjoinRoot.root f.factor)) * f.removeFactor = Polynomial.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

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.

Equations

• One or more equations did not get rendered due to their size.

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.

Equations

• Polynomial.SplittingFieldAux n f = (Polynomial.SplittingFieldAuxAux n f).fst

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

Equations

• Polynomial.SplittingFieldAux.field n f = (Polynomial.SplittingFieldAuxAux n f).snd.fst

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

Equations

• Polynomial.instInhabitedSplittingFieldAux n f = { default := 0 }

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

Equations

• Polynomial.SplittingFieldAux.algebra n f = (Polynomial.SplittingFieldAuxAux n f).snd.snd

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

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

Equations

• Polynomial.SplittingFieldAux.algebra''' = Polynomial.SplittingFieldAux.algebra n f.removeFactor

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

Equations

• Polynomial.SplittingFieldAux.algebra' = Polynomial.SplittingFieldAux.algebra'''

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

Equations

• Polynomial.SplittingFieldAux.algebra'' = ((algebraMap (AdjoinRoot f.factor) (Polynomial.SplittingFieldAux n f.removeFactor)).comp (AdjoinRoot.of f.factor)).toAlgebra

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

Equations

• ⋯ = ⋯

theorem Polynomial.SplittingFieldAux.algebraMap_succ {K : Type v} [Field K] (n : ℕ) (f : Polynomial K) : algebraMap K (Polynomial.SplittingFieldAux (n + 1) f) = (algebraMap (AdjoinRoot f.factor) (Polynomial.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) : Polynomial.Splits (algebraMap K (Polynomial.SplittingFieldAux n f)) f

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

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

Equations

• ⋯ = ⋯

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

A splitting field of a polynomial.

Equations

• f.SplittingField = (MvPolynomial (Polynomial.SplittingFieldAux f.natDegree f) K ⧸ RingHom.ker (MvPolynomial.aeval id).toRingHom)

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

Equations

• Polynomial.SplittingField.commRing f = Ideal.Quotient.commRing (RingHom.ker (MvPolynomial.aeval id).toRingHom)

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

Equations

• Polynomial.SplittingField.inhabited f = { default := 37 }

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

Equations

• Polynomial.SplittingField.instSMulOfIsScalarTower f = Submodule.Quotient.instSMul' (RingHom.ker (MvPolynomial.aeval id).toRingHom)

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

Equations

• Polynomial.SplittingField.algebra f = Ideal.Quotient.algebra K

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

Equations

• Polynomial.SplittingField.algebra' f = Ideal.Quotient.algebra R

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

Equations

• ⋯ = ⋯

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

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

Equations

• Polynomial.SplittingField.algEquivSplittingFieldAux f = Ideal.quotientKerAlgEquivOfSurjective ⋯

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

Equations

• Polynomial.SplittingField.instGroupWithZero f = GroupWithZero.mk ⋯ zpowRec ⋯ ⋯ ⋯ ⋯ ⋯

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

Equations

• Polynomial.SplittingField.instField f = Field.mk ⋯ GroupWithZero.zpow ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ (fun (x1 : ℚ≥0) (x2 : f.SplittingField) => x1 • x2) ⋯ ⋯ (fun (x1 : ℚ) (x2 : f.SplittingField) => x1 • x2) ⋯

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

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯

theorem Polynomial.SplittingField.splits {K : Type v} [Field K] (f : Polynomial K) : Polynomial.Splits (algebraMap K f.SplittingField) 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) : f.SplittingField →ₐ[K] L

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

Equations

• Polynomial.SplittingField.lift f hb = Polynomial.IsSplittingField.lift f.SplittingField f hb

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

Equations

• ⋯ = ⋯

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

Equations

• Polynomial.IsSplittingField.instFintypeSplittingField f = FiniteDimensional.fintypeOfFintype K f.SplittingField

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

Equations

• ⋯ = ⋯

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

Any splitting field is isomorphic to SplittingFieldAux f.

Equations

• Polynomial.IsSplittingField.algEquiv L f = AlgEquiv.ofBijective (Polynomial.IsSplittingField.lift L f ⋯) ⋯