Mathlib.FieldTheory.SplittingField.Construction

Polynomial.factor definition

(f : K[X]) : K[X]

Full source

/-- Non-computably choose an irreducible factor from a polynomial. -/
def factor (f : K[X]) : K[X] :=
  if H : ∃ g, Irreducible g ∧ g ∣ f then Classical.choose H else X

Irreducible factor of a polynomial

Informal description

Given a polynomial $ f $ over a field $ K $, the function returns an irreducible factor of $ f $ if one exists, otherwise it returns the polynomial $ X $.

Polynomial.irreducible_factor theorem

(f : K[X]) : Irreducible (factor f)

Full source

theorem irreducible_factor (f : K[X]) : Irreducible (factor f) := by
  rw [factor]
  split_ifs with H
  · exact (Classical.choose_spec H).1
  · exact irreducible_X

Irreducibility of the Factor Polynomial

Informal description

For any polynomial $f$ over a field $K$, the polynomial $\text{factor}(f)$ is irreducible in $K[X]$.

Polynomial.fact_irreducible_factor theorem

(f : K[X]) : Fact (Irreducible (factor f))

Full source

/-- See note [fact non-instances]. -/
theorem fact_irreducible_factor (f : K[X]) : Fact (Irreducible (factor f)) :=
  ⟨irreducible_factor f⟩

Irreducibility of Polynomial Factor as Type Class Instance

Informal description

For any polynomial $f$ over a field $K$, the polynomial $\text{factor}(f)$ is irreducible in $K[X]$, and this property is registered as a type class instance via the `Fact` wrapper.

Polynomial.factor_dvd_of_not_isUnit theorem

{f : K[X]} (hf1 : ¬IsUnit f) : factor f ∣ f

Full source

theorem factor_dvd_of_not_isUnit {f : K[X]} (hf1 : ¬IsUnit f) : factorfactor f ∣ f := by
  by_cases hf2 : f = 0; · rw [hf2]; exact dvd_zero _
  rw [factor, dif_pos (WfDvdMonoid.exists_irreducible_factor hf1 hf2)]
  exact (Classical.choose_spec <| WfDvdMonoid.exists_irreducible_factor hf1 hf2).2

Irreducible Factor Divides Non-Unit Polynomial

Informal description

For any polynomial $f$ over a field $K$, if $f$ is not a unit, then the irreducible factor $\text{factor}(f)$ divides $f$.

Polynomial.factor_dvd_of_degree_ne_zero theorem

{f : K[X]} (hf : f.degree ≠ 0) : factor f ∣ f

Full source

theorem factor_dvd_of_degree_ne_zero {f : K[X]} (hf : f.degree ≠ 0) : factorfactor f ∣ f :=
  factor_dvd_of_not_isUnit (mt degree_eq_zero_of_isUnit hf)

Irreducible Factor Divides Non-Constant Polynomial

Informal description

For any polynomial $f$ over a field $K$, if the degree of $f$ is not zero, then the irreducible factor $\text{factor}(f)$ divides $f$.

Polynomial.factor_dvd_of_natDegree_ne_zero theorem

{f : K[X]} (hf : f.natDegree ≠ 0) : factor f ∣ f

Full source

theorem factor_dvd_of_natDegree_ne_zero {f : K[X]} (hf : f.natDegree ≠ 0) : factorfactor f ∣ f :=
  factor_dvd_of_degree_ne_zero (mt natDegree_eq_of_degree_eq_some hf)

Irreducible Factor Divides Non-Zero Degree Polynomial

Informal description

For any polynomial $f$ over a field $K$, if the natural degree of $f$ is not zero, then the irreducible factor $\text{factor}(f)$ divides $f$.

Polynomial.isCoprime_iff_aeval_ne_zero theorem

 (f g : K[X]) :
  IsCoprime f g ↔ ∀ {A : Type v} [CommRing A] [IsDomain A] [Algebra K A] (a : A), aeval a f ≠ 0 ∨ aeval a g ≠ 0

Full source

lemma isCoprime_iff_aeval_ne_zero (f g : K[X]) : IsCoprimeIsCoprime f g ↔ ∀ {A : Type v} [CommRing A]
    [IsDomain A] [Algebra K A] (a : A), aeval a f ≠ 0 ∨ aeval a g ≠ 0 := by
  refine ⟨fun h => aeval_ne_zero_of_isCoprime h, fun h => isCoprime_of_dvd _ _ ?_ fun x hx _ => ?_⟩
  · replace h := @h K _ _ _ 0
    contrapose! h
    rw [h.left, h.right, map_zero, and_self]
  · rintro ⟨_, rfl⟩ ⟨_, rfl⟩
    replace h := not_and_or.mpr <| h <| AdjoinRoot.root x.factor
    simp only [AdjoinRoot.aeval_eq, AdjoinRoot.mk_eq_zero,
      dvd_mul_of_dvd_left <| factor_dvd_of_not_isUnit hx, true_and, not_true] at h

Coprimality of Polynomials via Non-Vanishing Evaluations

Informal description

Two polynomials $f$ and $g$ over a field $K$ are coprime if and only if for every commutative domain $A$ with a $K$-algebra structure and every element $a \in A$, at least one of the evaluations $\text{aeval}(a, f)$ or $\text{aeval}(a, g)$ is nonzero.

Polynomial.removeFactor definition

(f : K[X]) : Polynomial (AdjoinRoot <| factor f)

Full source

/-- Divide a polynomial f by `X - C r` where `r` is a root of `f` in a bigger field extension. -/
def removeFactor (f : K[X]) : Polynomial (AdjoinRoot <| factor f) :=
  mapmap (AdjoinRoot.of f.factor) f /ₘ (X - C (AdjoinRoot.root f.factor))

Polynomial with factor removed in field extension

Informal description

Given a polynomial $ f $ over a field $ K $, the function `removeFactor` returns a polynomial over the field extension $ K[X]/(\text{factor}(f)) $ obtained by: 1. Mapping $ f $ into the extension field via the natural embedding $ \text{AdjoinRoot.of} $ 2. Dividing the result by the linear polynomial $ (X - r) $ where $ r $ is the adjoined root of $ \text{factor}(f) $

Polynomial.X_sub_C_mul_removeFactor theorem

 (f : K[X]) (hf : f.natDegree ≠ 0) :
  (X - C (AdjoinRoot.root f.factor)) * f.removeFactor = map (AdjoinRoot.of f.factor) f

Full source

theorem X_sub_C_mul_removeFactor (f : K[X]) (hf : f.natDegree ≠ 0) :
    (X - C (AdjoinRoot.root f.factor)) * f.removeFactor = map (AdjoinRoot.of f.factor) f := by
  let ⟨g, hg⟩ := factor_dvd_of_natDegree_ne_zero hf
  apply (mul_divByMonic_eq_iff_isRoot
    (R := AdjoinRoot f.factor) (a := AdjoinRoot.root f.factor)).mpr
  rw [IsRoot.def, eval_map, hg, eval₂_mul, ← hg, AdjoinRoot.eval₂_root, zero_mul]

Factorization Identity in Field Extension: $(X-r)\cdot\text{removeFactor}(f) = \text{map}(\text{of}, f)$

Informal description

Let $K$ be a field and $f \in K[X]$ be a polynomial with $\deg(f) \neq 0$. Then in the field extension $K[X]/(\text{factor}(f))$, we have the equality: $$(X - r) \cdot \text{removeFactor}(f) = \text{map}(\text{of}, f)$$ where: - $r$ is the adjoined root of $\text{factor}(f)$ in $K[X]/(\text{factor}(f))$ - $\text{removeFactor}(f)$ is the polynomial obtained by removing the linear factor $(X - r)$ from $f$ in the extension field - $\text{of}$ is the canonical embedding $K \to K[X]/(\text{factor}(f))$ - $\text{map}(\text{of}, f)$ is the image of $f$ under the extension of $\text{of}$ to polynomial rings.

Polynomial.natDegree_removeFactor theorem

(f : K[X]) : f.removeFactor.natDegree = f.natDegree - 1

Full source

theorem natDegree_removeFactor (f : K[X]) : f.removeFactor.natDegree = f.natDegree - 1 := by
  rw [removeFactor, natDegree_divByMonic _ (monic_X_sub_C _), natDegree_map, natDegree_X_sub_C]

Degree Reduction by Factor Removal: $\deg(\text{removeFactor}(f)) = \deg(f) - 1$

Informal description

For any polynomial $f$ over a field $K$, the degree of the polynomial obtained by removing a factor (via `removeFactor`) is one less than the degree of $f$, i.e., $\deg(\text{removeFactor}(f)) = \deg(f) - 1$.

Polynomial.natDegree_removeFactor' theorem

{f : K[X]} {n : ℕ} (hfn : f.natDegree = n + 1) : f.removeFactor.natDegree = n

Full source

theorem natDegree_removeFactor' {f : K[X]} {n : ℕ} (hfn : f.natDegree = n + 1) :
    f.removeFactor.natDegree = n := by rw [natDegree_removeFactor, hfn, n.add_sub_cancel]

Degree Reduction by Factor Removal: $\deg(\text{removeFactor}(f)) = \deg(f) - 1$ for $\deg(f) = n + 1$

Informal description

For any polynomial $f$ over a field $K$ with $\deg(f) = n + 1$, the degree of the polynomial obtained by removing a factor is $n$, i.e., $\deg(\text{removeFactor}(f)) = n$.

Polynomial.SplittingFieldAuxAux definition

(n : ℕ) : ∀ {K : Type u} [Field K], K[X] → Σ (L : Type u) (_ : Field L), Algebra K L

Full source

/-- 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 SplittingFieldAuxAux (n : ℕ) : ∀ {K : Type u} [Field K], K[X] →
    Σ (L : Type u) (_ : Field L), Algebra K L :=
  -- Porting note: added motive
  Nat.recOn (motive := fun (_x : ℕ) => ∀ {K : Type u} [_inst_4 : Field K], K[X] →
      Σ (L : Type u) (_ : Field L), Algebra K L) n
    (fun {K} _ _ => ⟨K, inferInstance, inferInstance⟩)
    fun _ ih _ _ f =>
      let ⟨L, fL, _⟩ := ih f.removeFactor
      ⟨L, fL, (RingHom.comp (algebraMap _ _) (AdjoinRoot.of f.factor)).toAlgebra⟩

Recursive construction of field extension by removing polynomial factors

Informal description

Given a natural number `n` and a polynomial `f` over a field `K`, the function constructs a field extension `L` of `K` by recursively removing `n` factors from `f`. Specifically: 1. For `n = 0`, it returns `K` itself. 2. For `n > 0`, it first removes one factor of `f` (using `removeFactor`), then recursively constructs the field extension for the remaining `n-1` factors. The result is a dependent pair consisting of: - The field extension `L` - A proof that `L` is a field - An algebra structure showing `L` is an extension of `K`

Polynomial.SplittingFieldAux definition

(n : ℕ) {K : Type u} [Field K] (f : K[X]) : Type u

Full source

/-- Auxiliary construction to a splitting field of a polynomial, which removes
`n` (arbitrarily-chosen) factors. It is the type constructed in `SplittingFieldAuxAux`.
-/
def SplittingFieldAux (n : ℕ) {K : Type u} [Field K] (f : K[X]) : Type u :=
  (SplittingFieldAuxAux n f).1

Auxiliary splitting field construction by removing polynomial factors

Informal description

Given a natural number `n`, a field `K`, and a polynomial `f` over `K`, the type `SplittingFieldAux n f` represents an auxiliary field extension of `K` constructed by removing `n` factors from `f`. This is obtained as the first component of the dependent pair constructed by `SplittingFieldAuxAux n f`.

Polynomial.SplittingFieldAux.field instance

(n : ℕ) {K : Type u} [Field K] (f : K[X]) : Field (SplittingFieldAux n f)

Full source

instance SplittingFieldAux.field (n : ℕ) {K : Type u} [Field K] (f : K[X]) :
    Field (SplittingFieldAux n f) :=
  (SplittingFieldAuxAux n f).2.1

Field Structure on Auxiliary Splitting Field Construction

Informal description

For any natural number $n$, field $K$, and polynomial $f$ over $K$, the auxiliary splitting field construction $\text{SplittingFieldAux}\,n\,f$ is a field.

Polynomial.instInhabitedSplittingFieldAux instance

(n : ℕ) {K : Type u} [Field K] (f : K[X]) : Inhabited (SplittingFieldAux n f)

Full source

instance (n : ℕ) {K : Type u} [Field K] (f : K[X]) : Inhabited (SplittingFieldAux n f) :=
  ⟨0⟩

Inhabitedness of Auxiliary Splitting Fields

Informal description

For any natural number $n$, field $K$, and polynomial $f \in K[X]$, the auxiliary splitting field construction $\text{SplittingFieldAux}\,n\,f$ is inhabited.

Polynomial.SplittingFieldAux.algebra instance

(n : ℕ) {K : Type u} [Field K] (f : K[X]) : Algebra K (SplittingFieldAux n f)

Full source

instance SplittingFieldAux.algebra (n : ℕ) {K : Type u} [Field K] (f : K[X]) :
    Algebra K (SplittingFieldAux n f) :=
  (SplittingFieldAuxAux n f).2.2

Algebra Structure on Auxiliary Splitting Field Construction

Informal description

For any natural number $n$, field $K$, and polynomial $f$ over $K$, the auxiliary splitting field construction $\text{SplittingFieldAux}\,n\,f$ is equipped with a canonical $K$-algebra structure.

Polynomial.SplittingFieldAux.succ theorem

(n : ℕ) (f : K[X]) : SplittingFieldAux (n + 1) f = SplittingFieldAux n f.removeFactor

Full source

theorem succ (n : ℕ) (f : K[X]) :
    SplittingFieldAux (n + 1) f = SplittingFieldAux n f.removeFactor :=
  rfl

Recursive Construction of Splitting Field: $S_{n+1}(f) = S_n(f/\text{factor})$

Informal description

For any natural number $n$ and polynomial $f$ over a field $K$, the splitting field auxiliary construction at stage $n+1$ is equal to the splitting field auxiliary construction at stage $n$ applied to the polynomial obtained by removing a factor of $f$ in the field extension $K[X]/(\text{factor}(f))$.

Polynomial.SplittingFieldAux.algebra''' instance

{n : ℕ} {f : K[X]} : Algebra (AdjoinRoot f.factor) (SplittingFieldAux n f.removeFactor)

Full source

instance algebra''' {n : ℕ} {f : K[X]} :
    Algebra (AdjoinRoot f.factor) (SplittingFieldAux n f.removeFactor) :=
  SplittingFieldAux.algebra n _

Algebra Structure on Splitting Field Auxiliary Construction After Factor Removal

Informal description

For any natural number $n$ and polynomial $f$ over a field $K$, the auxiliary splitting field construction $\text{SplittingFieldAux}\,n\,f.\text{removeFactor}$ is equipped with a canonical algebra structure over the field extension $K[X]/(f.\text{factor})$.

Polynomial.SplittingFieldAux.algebra' instance

{n : ℕ} {f : K[X]} : Algebra (AdjoinRoot f.factor) (SplittingFieldAux n.succ f)

Full source

instance algebra' {n : ℕ} {f : K[X]} : Algebra (AdjoinRoot f.factor) (SplittingFieldAux n.succ f) :=
  SplittingFieldAux.algebra'''

Algebra Structure on Successor Stage of Splitting Field Construction

Informal description

For any natural number $n$ and polynomial $f$ over a field $K$, the auxiliary splitting field construction $\text{SplittingFieldAux}\,(n+1)\,f$ is equipped with a canonical algebra structure over the field extension $K[X]/(f.\text{factor})$.

Polynomial.SplittingFieldAux.algebra'' instance

{n : ℕ} {f : K[X]} : Algebra K (SplittingFieldAux n f.removeFactor)

Full source

instance algebra'' {n : ℕ} {f : K[X]} : Algebra K (SplittingFieldAux n f.removeFactor) :=
  RingHom.toAlgebra (RingHom.comp (algebraMap _ _) (AdjoinRoot.of f.factor))

Algebra Structure on Auxiliary Splitting Field Construction over Base Field

Informal description

For any natural number $n$ and polynomial $f$ over a field $K$, the auxiliary splitting field construction $\text{SplittingFieldAux}\,n\,f.\text{removeFactor}$ is equipped with a canonical algebra structure over $K$.

Polynomial.SplittingFieldAux.scalar_tower' instance

{n : ℕ} {f : K[X]} : IsScalarTower K (AdjoinRoot f.factor) (SplittingFieldAux n f.removeFactor)

Full source

instance scalar_tower' {n : ℕ} {f : K[X]} :
    IsScalarTower K (AdjoinRoot f.factor) (SplittingFieldAux n f.removeFactor) :=
  IsScalarTower.of_algebraMap_eq fun _ => rfl

Scalar Tower Property for Auxiliary Splitting Field Construction

Informal description

For any natural number $n$ and polynomial $f$ over a field $K$, the scalar multiplication operations on the auxiliary splitting field construction $\text{SplittingFieldAux}\,n\,f.\text{removeFactor}$ form a scalar tower over $K$ and the field extension $K[X]/(f.\text{factor})$. This means that for any scalar $k \in K$, element $a \in K[X]/(f.\text{factor})$, and element $x \in \text{SplittingFieldAux}\,n\,f.\text{removeFactor}$, we have $k \cdot (a \cdot x) = (k \cdot a) \cdot x$.

Polynomial.SplittingFieldAux.algebraMap_succ theorem

 (n : ℕ) (f : K[X]) :
  algebraMap K (SplittingFieldAux (n + 1) f) =
    (algebraMap (AdjoinRoot f.factor) (SplittingFieldAux n f.removeFactor)).comp (AdjoinRoot.of f.factor)

Full source

theorem algebraMap_succ (n : ℕ) (f : K[X]) :
    algebraMap K (SplittingFieldAux (n + 1) f) =
      (algebraMap (AdjoinRoot f.factor) (SplittingFieldAux n f.removeFactor)).comp
        (AdjoinRoot.of f.factor) :=
  rfl

Recursive Construction of Algebra Map for Splitting Fields

Informal description

For any natural number $n$ and polynomial $f$ over a field $K$, the algebra map from $K$ to the splitting field $\text{SplittingFieldAux}\,(n+1)\,f$ is equal to the composition of the algebra map from $\text{AdjoinRoot}\,f.\text{factor}$ to $\text{SplittingFieldAux}\,n\,f.\text{removeFactor}$ with the natural embedding $\text{AdjoinRoot.of}\,f.\text{factor}$ from $K$ to $\text{AdjoinRoot}\,f.\text{factor}$.

Polynomial.SplittingFieldAux.splits theorem

 (n : ℕ) :
  ∀ {K : Type u} [Field K], ∀ (f : K[X]) (_hfn : f.natDegree = n), Splits (algebraMap K <| SplittingFieldAux n f) f

Full source

protected theorem splits (n : ℕ) :
    ∀ {K : Type u} [Field K],
      ∀ (f : K[X]) (_hfn : f.natDegree = n), Splits (algebraMap K <| SplittingFieldAux n f) f :=
  Nat.recOn (motive := fun n => ∀ {K : Type u} [Field K],
      ∀ (f : K[X]) (_hfn : f.natDegree = n), Splits (algebraMap K <| SplittingFieldAux n f) f) n
    (fun {_} _ _ hf =>
      splits_of_degree_le_one _
        (le_trans degree_le_natDegree <| hf.symm ▸ WithBot.coe_le_coe.2 zero_le_one))
    fun n ih {K} _ f hf => by
    rw [← splits_id_iff_splits, algebraMap_succ, ← map_map, splits_id_iff_splits,
      ← X_sub_C_mul_removeFactor f fun h => by rw [h] at hf; cases hf]
    exact splits_mul _ (splits_X_sub_C _) (ih _ (natDegree_removeFactor' hf))

Splitting Property of Auxiliary Splitting Field Construction: $f$ splits in $\text{SplittingFieldAux}\,n\,f$ when $\deg(f) = n$

Informal description

For any natural number $n$, field $K$, and polynomial $f \in K[X]$ with $\deg(f) = n$, the polynomial $f$ splits completely in the field extension $\text{SplittingFieldAux}\,n\,f$ via the canonical algebra map $K \to \text{SplittingFieldAux}\,n\,f$.

Polynomial.SplittingFieldAux.adjoin_rootSet theorem

 (n : ℕ) :
  ∀ {K : Type u} [Field K],
    ∀ (f : K[X]) (_hfn : f.natDegree = n), Algebra.adjoin K (f.rootSet (SplittingFieldAux n f)) = ⊤

Full source

theorem adjoin_rootSet (n : ℕ) :
    ∀ {K : Type u} [Field K],
      ∀ (f : K[X]) (_hfn : f.natDegree = n),
        Algebra.adjoin K (f.rootSet (SplittingFieldAux n f)) = ⊤ :=
  Nat.recOn (motive := fun n =>
    ∀ {K : Type u} [Field K],
      ∀ (f : K[X]) (_hfn : f.natDegree = n),
        Algebra.adjoin K (f.rootSet (SplittingFieldAux n f)) = ⊤)
    n (fun {_} _ _ _hf => Algebra.eq_top_iff.2 fun x => Subalgebra.range_le _ ⟨x, rfl⟩)
    fun n ih {K} _ f hfn => by
    have hndf : f.natDegree ≠ 0 := by intro h; rw [h] at hfn; cases hfn
    have hfn0 : f ≠ 0 := by intro h; rw [h] at hndf; exact hndf rfl
    have hmf0 : mapmap (algebraMap K (SplittingFieldAux n.succ f)) f ≠ 0 := map_ne_zero hfn0
    classical
    rw [rootSet_def, aroots_def]
    rw [algebraMap_succ, ← map_map, ← X_sub_C_mul_removeFactor _ hndf, Polynomial.map_mul] at hmf0 ⊢
    -- This used to be `rw`, but we need `erw` after https://github.com/leanprover/lean4/pull/2644
    rw [roots_mul hmf0, Polynomial.map_sub, map_X, map_C, roots_X_sub_C, Multiset.toFinset_add,
      Finset.coe_union, Multiset.toFinset_singleton, Finset.coe_singleton,
      Algebra.adjoin_union_eq_adjoin_adjoin, ← Set.image_singleton]
    erw [Algebra.adjoin_algebraMap K (SplittingFieldAux n f.removeFactor)]
    rw [AdjoinRoot.adjoinRoot_eq_top, Algebra.map_top]
    /- Porting note: was `rw [IsScalarTower.adjoin_range_toAlgHom K (AdjoinRoot f.factor)
        (SplittingFieldAux n f.removeFactor)]` -/
    have := IsScalarTower.adjoin_range_toAlgHom K (AdjoinRoot f.factor)
        (SplittingFieldAux n f.removeFactor)
        (f.removeFactor.rootSet (SplittingFieldAux n f.removeFactor))
    refine this.trans ?_
    rw [ih _ (natDegree_removeFactor' hfn), Subalgebra.restrictScalars_top]

Root Set Generates Splitting Field in Degree-Matching Case

Informal description

For any natural number $n$, field $K$, and polynomial $f \in K[X]$ with $\deg(f) = n$, the $K$-subalgebra generated by the roots of $f$ in the auxiliary splitting field $\text{SplittingFieldAux}\,n\,f$ is equal to the entire field. In other words, $\text{adjoin}_K(f.\text{rootSet}(\text{SplittingFieldAux}\,n\,f)) = \text{SplittingFieldAux}\,n\,f$.

Polynomial.SplittingFieldAux.instIsSplittingFieldNatDegree instance

(f : K[X]) : IsSplittingField K (SplittingFieldAux f.natDegree f) f

Full source

instance (f : K[X]) : IsSplittingField K (SplittingFieldAux f.natDegree f) f :=
  ⟨SplittingFieldAux.splits _ _ rfl, SplittingFieldAux.adjoin_rootSet _ _ rfl⟩

Auxiliary Splitting Field Construction is a Splitting Field

Informal description

For any polynomial $f$ over a field $K$, the auxiliary splitting field construction $\text{SplittingFieldAux}\,(\deg f)\,f$ is a splitting field of $f$ over $K$. This means that $f$ splits completely into linear factors in this field extension, and the extension is generated by the roots of $f$.

Polynomial.SplittingField definition

(f : K[X])

Full source

/-- A splitting field of a polynomial. -/
@[stacks 09HV "The construction of the splitting field."]
def SplittingField (f : K[X]) :=
  MvPolynomialMvPolynomial (SplittingFieldAux f.natDegree f) K ⧸
    RingHom.ker (MvPolynomial.aeval (R := K) id).toRingHom

Splitting field of a polynomial

Informal description

Given a polynomial $f$ over a field $K$, the splitting field of $f$ is defined as the quotient of the polynomial ring in variables indexed by the auxiliary splitting field construction $\text{SplittingFieldAux}\,(\text{natDegree}\,f)\,f$ by the kernel of the evaluation map (as a ring homomorphism) that substitutes each variable with itself.

Polynomial.SplittingField.commRing instance

: CommRing (SplittingField f)

Full source

instance commRing : CommRing (SplittingField f) :=
  Ideal.Quotient.commRing _

Commutative Ring Structure on Splitting Fields

Informal description

The splitting field of a polynomial $f$ over a field $K$ is a commutative ring.

Polynomial.SplittingField.inhabited instance

: Inhabited (SplittingField f)

Full source

instance inhabited : Inhabited (SplittingField f) :=
  ⟨37⟩

Nonemptiness of Splitting Fields

Informal description

The splitting field of a polynomial $f$ over a field $K$ is nonempty.

Polynomial.SplittingField.instSMulOfIsScalarTower instance

{S : Type*} [DistribSMul S K] [IsScalarTower S K K] : SMul S (SplittingField f)

Full source

instance {S : Type*} [DistribSMul S K] [IsScalarTower S K K] : SMul S (SplittingField f) :=
  Submodule.Quotient.instSMul' _

Scalar Multiplication on Splitting Fields via Scalar Tower Condition

Informal description

For any type $S$ with a distributive scalar multiplication action on a field $K$ and satisfying the scalar tower condition for $K$, the splitting field $\text{SplittingField}\,f$ of a polynomial $f$ over $K$ inherits a scalar multiplication operation from $S$.

Polynomial.SplittingField.algebra instance

: Algebra K (SplittingField f)

Full source

instance algebra : Algebra K (SplittingField f) :=
  Ideal.Quotient.algebra _

Algebra Structure on Splitting Fields

Informal description

For any field $K$ and polynomial $f$ over $K$, the splitting field $\text{SplittingField}\,f$ is equipped with a canonical $K$-algebra structure.

Polynomial.SplittingField.algebra' instance

{R : Type*} [CommSemiring R] [Algebra R K] : Algebra R (SplittingField f)

Full source

instance algebra' {R : Type*} [CommSemiring R] [Algebra R K] : Algebra R (SplittingField f) :=
  Ideal.Quotient.algebra _

Algebra Structure on Splitting Fields via Base Ring Extension

Informal description

For any commutative semiring $R$ with an algebra structure over a field $K$, the splitting field $\text{SplittingField}\,f$ of a polynomial $f$ over $K$ inherits an $R$-algebra structure.

Polynomial.SplittingField.isScalarTower instance

{R : Type*} [CommSemiring R] [Algebra R K] : IsScalarTower R K (SplittingField f)

Full source

instance isScalarTower {R : Type*} [CommSemiring R] [Algebra R K] :
    IsScalarTower R K (SplittingField f) :=
  Ideal.Quotient.isScalarTower _ _ _

Scalar Tower Condition for Splitting Fields

Informal description

For any commutative semiring $R$ with an algebra structure over a field $K$, the splitting field $\text{SplittingField}\,f$ of a polynomial $f$ over $K$ satisfies the scalar tower condition for the scalar multiplication from $R$ to $K$.

Polynomial.SplittingField.algEquivSplittingFieldAux definition

(f : K[X]) : SplittingField f ≃ₐ[K] SplittingFieldAux f.natDegree f

Full source

/-- The algebra equivalence with `SplittingFieldAux`,
which we will use to construct the field structure. -/
def algEquivSplittingFieldAux (f : K[X]) : SplittingFieldSplittingField f ≃ₐ[K] SplittingFieldAux f.natDegree f :=
  Ideal.quotientKerAlgEquivOfSurjective fun x => ⟨MvPolynomial.X x, by simp⟩

Isomorphism between Splitting Field and Auxiliary Construction

Informal description

For any polynomial $ f $ over a field $ K $, there is a $ K $-algebra isomorphism between the splitting field $ \text{SplittingField}\,f $ and the auxiliary splitting field construction $ \text{SplittingFieldAux}\,(\text{natDegree}\,f)\,f $. This isomorphism is constructed using the first isomorphism theorem for algebras, applied to the evaluation map that substitutes each variable with itself in the polynomial ring.

Polynomial.SplittingField.instGroupWithZero instance

: GroupWithZero (SplittingField f)

Full source

instance instGroupWithZero : GroupWithZero (SplittingField f) :=
  let e := algEquivSplittingFieldAux f
  { inv := fun a ↦ e.symm (e a)⁻¹
    inv_zero := by simp
    mul_inv_cancel := fun a ha ↦ e.injective <| by simp [EmbeddingLike.map_ne_zero_iff.2 ha]
    __ := e.surjective.nontrivial }

Splitting Fields are Groups with Zero

Informal description

The splitting field of a polynomial $f$ over a field $K$ is a group with zero.

Polynomial.SplittingField.instField instance

: Field (SplittingField f)

Full source

instance instField : Field (SplittingField f) where
  __ := commRing _
  __ := instGroupWithZero _
  nnratCast q := algebraMap K _ q
  ratCast q := algebraMap K _ q
  nnqsmul := (· • ·)
  qsmul := (· • ·)
  nnratCast_def q := by change algebraMap K _ _ = _; simp_rw [NNRat.cast_def, map_div₀, map_natCast]
  ratCast_def q := by
    change algebraMap K _ _ = _; rw [Rat.cast_def, map_div₀, map_intCast, map_natCast]
  nnqsmul_def q x := Quotient.inductionOn x fun p ↦ congr_arg Quotient.mk'' <| by
    ext; simp [MvPolynomial.algebraMap_eq, NNRat.smul_def]
  qsmul_def q x := Quotient.inductionOn x fun p ↦ congr_arg Quotient.mk'' <| by
    ext; simp [MvPolynomial.algebraMap_eq, Rat.smul_def]

Splitting Fields are Fields

Informal description

The splitting field of a polynomial $f$ over a field $K$ is itself a field.

Polynomial.SplittingField.instCharZero instance

[CharZero K] : CharZero (SplittingField f)

Full source

instance instCharZero [CharZero K] : CharZero (SplittingField f) :=
  charZero_of_injective_algebraMap (algebraMap K _).injective

Splitting Fields Preserve Characteristic Zero

Informal description

For any field $K$ of characteristic zero, the splitting field of a polynomial $f$ over $K$ also has characteristic zero.

Polynomial.SplittingField.instCharP instance

(p : ℕ) [CharP K p] : CharP (SplittingField f) p

Full source

instance instCharP (p : ℕ) [CharP K p] : CharP (SplittingField f) p :=
  charP_of_injective_algebraMap (algebraMap K _).injective p

Characteristic of Splitting Fields Preserves Base Field Characteristic

Informal description

For any prime $p$ and any field $K$ of characteristic $p$, the splitting field of a polynomial $f$ over $K$ also has characteristic $p$.

Polynomial.SplittingField.instExpChar instance

(p : ℕ) [ExpChar K p] : ExpChar (SplittingField f) p

Full source

instance instExpChar (p : ℕ) [ExpChar K p] : ExpChar (SplittingField f) p :=
  expChar_of_injective_algebraMap (algebraMap K _).injective p

Splitting Fields Preserve Exponential Characteristic

Informal description

For any prime power $p$ and any field $K$ of exponential characteristic $p$, the splitting field of a polynomial $f$ over $K$ also has exponential characteristic $p$.

Polynomial.IsSplittingField.splittingField instance

(f : K[X]) : IsSplittingField K (SplittingField f) f

Full source

instance _root_.Polynomial.IsSplittingField.splittingField (f : K[X]) :
    IsSplittingField K (SplittingField f) f :=
  IsSplittingField.of_algEquiv _ f (algEquivSplittingFieldAux f).symm

Splitting Field Property of $\text{SplittingField}\,f$

Informal description

For any polynomial $f$ over a field $K$, the splitting field $\text{SplittingField}\,f$ is indeed a splitting field of $f$ over $K$. This means that $f$ splits completely into linear factors in $\text{SplittingField}\,f$ and this field extension is minimal with this property.

Polynomial.SplittingField.splits theorem

: Splits (algebraMap K (SplittingField f)) f

Full source

@[stacks 09HU "Splitting part"]
protected theorem splits : Splits (algebraMap K (SplittingField f)) f :=
  IsSplittingField.splits f.SplittingField f

Polynomial Splits in its Splitting Field

Informal description

The polynomial $f$ splits completely in its splitting field over $K$, i.e., the canonical algebra homomorphism from $K$ to $\text{SplittingField}\,f$ maps $f$ to a product of linear factors in $\text{SplittingField}\,f$.

Polynomial.SplittingField.lift definition

: SplittingField f →ₐ[K] L

Full source

/-- Embeds the splitting field into any other field that splits the polynomial. -/
def lift : SplittingFieldSplittingField f →ₐ[K] L :=
  IsSplittingField.lift f.SplittingField f hb

Embedding of splitting field into a field where the polynomial splits

Informal description

Given a polynomial $ f $ over a field $ K $ and a field $ L $ where $ f $ splits, there exists an algebra homomorphism from the splitting field of $ f $ over $ K $ to $ L $ that commutes with the embeddings of $ K $.

Polynomial.SplittingField.adjoin_rootSet theorem

: Algebra.adjoin K (f.rootSet (SplittingField f)) = ⊤

Full source

theorem adjoin_rootSet : Algebra.adjoin K (f.rootSet (SplittingField f)) = ⊤ :=
  Polynomial.IsSplittingField.adjoin_rootSet _ f

Splitting Field Generated by Roots of Polynomial

Informal description

For a polynomial $f$ over a field $K$, the smallest subalgebra of the splitting field $\text{SplittingField}\,f$ containing $K$ and all roots of $f$ in $\text{SplittingField}\,f$ is equal to the entire splitting field. In other words, $\text{SplittingField}\,f$ is generated over $K$ by the roots of $f$.

Polynomial.IsSplittingField.instFiniteDimensionalSplittingField instance

(f : K[X]) : FiniteDimensional K f.SplittingField

Full source

instance (f : K[X]) : FiniteDimensional K f.SplittingField :=
  finiteDimensional f.SplittingField f

Finite-Dimensionality of Splitting Fields

Informal description

For any polynomial $f$ over a field $K$, the splitting field of $f$ is a finite-dimensional vector space over $K$.

Polynomial.IsSplittingField.instFiniteSplittingField instance

[Finite K] (f : K[X]) : Finite f.SplittingField

Full source

instance [Finite K] (f : K[X]) : Finite f.SplittingField :=
  Module.finite_of_finite K

Finiteness of Splitting Fields over Finite Fields

Informal description

For any finite field $K$ and polynomial $f$ over $K$, the splitting field of $f$ is also finite.

Polynomial.IsSplittingField.instNoZeroSMulDivisorsSplittingField instance

(f : K[X]) : NoZeroSMulDivisors K f.SplittingField

Full source

instance (f : K[X]) : NoZeroSMulDivisors K f.SplittingField :=
  inferInstance

No Zero Divisors in Scalar Multiplication for Splitting Fields

Informal description

For any polynomial $f$ over a field $K$, the splitting field of $f$ has no zero divisors under scalar multiplication by elements of $K$. That is, for any $k \in K$ and $x$ in the splitting field of $f$, if $k \cdot x = 0$, then either $k = 0$ or $x = 0$.

Polynomial.IsSplittingField.algEquiv definition

(f : K[X]) [h : IsSplittingField K L f] : L ≃ₐ[K] SplittingField f

Full source

/-- Any splitting field is isomorphic to `SplittingFieldAux f`. -/
def algEquiv (f : K[X]) [h : IsSplittingField K L f] : L ≃ₐ[K] SplittingField f :=
  AlgEquiv.ofBijective (lift L f <| splits (SplittingField f) f) <|
    have := finiteDimensional L f
    ((Algebra.IsAlgebraic.of_finite K L).algHom_bijective₂ _ <| lift _ f h.1).1

Isomorphism between Splitting Fields

Informal description

Given a polynomial $ f $ over a field $ K $ and a field extension $ L $ of $ K $ that is a splitting field for $ f $, there exists an algebra isomorphism $ L \simeq_K \text{SplittingField}\,f $ between $ L $ and the splitting field of $ f $. This isomorphism is constructed using the universal property of splitting fields.

Mathlib.FieldTheory.SplittingField.Construction

Main definitions

Main statements

Implementation details