Mathlib.Algebra.Polynomial.Splits

Polynomial.Splits definition

(f : K[X]) : Prop

Full source

/-- A polynomial `Splits` iff it is zero or all of its irreducible factors have `degree` 1. -/
def Splits (f : K[X]) : Prop :=
  f.map i = 0 ∨ ∀ {g : L[X]}, Irreducible g → g ∣ f.map i → degree g = 1

Splitting condition for polynomials over a field extension

Informal description

A polynomial $ f \in K[X] $ *splits* over a field extension $ L $ of $ K $ (via a ring homomorphism $ i : K \to L $) if either $ f $ is the zero polynomial or every irreducible factor $ g $ of $ f $ over $ L $ has degree $ 1 $.

Polynomial.splits_zero theorem

: Splits i (0 : K[X])

Full source

@[simp]
theorem splits_zero : Splits i (0 : K[X]) :=
  Or.inl (Polynomial.map_zero i)

Zero Polynomial Splits in Any Field Extension

Informal description

The zero polynomial $0 \in K[X]$ splits over any field extension $L$ of $K$ via the ring homomorphism $i : K \to L$.

Polynomial.splits_of_map_eq_C theorem

{f : K[X]} {a : L} (h : f.map i = C a) : Splits i f

Full source

theorem splits_of_map_eq_C {f : K[X]} {a : L} (h : f.map i = C a) : Splits i f :=
  letI := Classical.decEq L
  if ha : a = 0 then Or.inl (h.trans (ha.symm ▸ C_0))
  else
    Or.inr fun hg ⟨p, hp⟩ =>
      absurd hg.1 <|
        Classical.not_not.2 <|
          isUnit_iff_degree_eq_zero.2 <| by
            have := congr_arg degree hp
            rw [h, degree_C ha, degree_mul, @eq_comm (WithBot ℕ) 0,
                Nat.WithBot.add_eq_zero_iff] at this
            exact this.1

Constant Polynomials Split in Any Field Extension

Informal description

Let $K$ be a commutative ring and $L$ a field extension of $K$ via a ring homomorphism $i : K \to L$. For any polynomial $f \in K[X]$, if the polynomial $f$ under the map $i$ equals a constant polynomial $C(a)$ for some $a \in L$, then $f$ splits over $L$ via $i$.

Polynomial.splits_C theorem

(a : K) : Splits i (C a)

Full source

@[simp]
theorem splits_C (a : K) : Splits i (C a) :=
  splits_of_map_eq_C i (map_C i)

Constant Polynomials Split in Any Field Extension

Informal description

For any element $a$ in a commutative ring $K$ and any ring homomorphism $i : K \to L$ where $L$ is a field, the constant polynomial $C(a) \in K[X]$ splits over $L$ via $i$.

Polynomial.splits_of_map_degree_eq_one theorem

{f : K[X]} (hf : degree (f.map i) = 1) : Splits i f

Full source

theorem splits_of_map_degree_eq_one {f : K[X]} (hf : degree (f.map i) = 1) : Splits i f :=
  Or.inr fun hg ⟨p, hp⟩ => by
    have := congr_arg degree hp
    simp [Nat.WithBot.add_eq_one_iff, hf, @eq_comm (WithBot ℕ) 1,
        mt isUnit_iff_degree_eq_zero.2 hg.1] at this
    tauto

Polynomial Splitting Criterion for Degree-One Mapped Polynomials

Informal description

Let $K$ be a commutative ring and $L$ a field extension of $K$ via a ring homomorphism $i : K \to L$. For any polynomial $f \in K[X]$, if the degree of $f$ after applying the map $i$ is equal to 1 (i.e., $\deg(f \circ i) = 1$), then $f$ splits over $L$ via $i$.

Polynomial.splits_of_degree_le_one theorem

{f : K[X]} (hf : degree f ≤ 1) : Splits i f

Full source

theorem splits_of_degree_le_one {f : K[X]} (hf : degree f ≤ 1) : Splits i f :=
  if hif : degree (f.map i) ≤ 0 then splits_of_map_eq_C i (degree_le_zero_iff.mp hif)
  else by
    push_neg at hif
    rw [← Order.succ_le_iff, ← WithBot.coe_zero, WithBot.orderSucc_coe, Nat.succ_eq_succ] at hif
    exact splits_of_map_degree_eq_one i ((degree_map_le.trans hf).antisymm hif)

Polynomials of Degree at Most One Split in Any Field Extension

Informal description

Let $K$ be a commutative ring and $L$ a field extension of $K$ via a ring homomorphism $i : K \to L$. For any polynomial $f \in K[X]$, if the degree of $f$ is at most 1 (i.e., $\deg(f) \leq 1$), then $f$ splits over $L$ via $i$.

Polynomial.splits_of_degree_eq_one theorem

{f : K[X]} (hf : degree f = 1) : Splits i f

Full source

theorem splits_of_degree_eq_one {f : K[X]} (hf : degree f = 1) : Splits i f :=
  splits_of_degree_le_one i hf.le

Degree-One Polynomials Split in Any Field Extension

Informal description

Let $K$ be a commutative ring and $L$ a field extension of $K$ via a ring homomorphism $i : K \to L$. For any polynomial $f \in K[X]$, if the degree of $f$ is exactly 1 (i.e., $\deg(f) = 1$), then $f$ splits over $L$ via $i$.

Polynomial.splits_of_natDegree_le_one theorem

{f : K[X]} (hf : natDegree f ≤ 1) : Splits i f

Full source

theorem splits_of_natDegree_le_one {f : K[X]} (hf : natDegree f ≤ 1) : Splits i f :=
  splits_of_degree_le_one i (degree_le_of_natDegree_le hf)

Polynomials of Natural Degree at Most One Split in Any Field Extension

Informal description

Let $K$ be a commutative ring and $L$ a field extension of $K$ via a ring homomorphism $i : K \to L$. For any polynomial $f \in K[X]$, if the natural degree of $f$ is at most 1 (i.e., $\text{natDegree}(f) \leq 1$), then $f$ splits over $L$ via $i$.

Polynomial.splits_of_natDegree_eq_one theorem

{f : K[X]} (hf : natDegree f = 1) : Splits i f

Full source

theorem splits_of_natDegree_eq_one {f : K[X]} (hf : natDegree f = 1) : Splits i f :=
  splits_of_natDegree_le_one i (le_of_eq hf)

Polynomials of Natural Degree One Split in Any Field Extension

Informal description

Let $K$ be a commutative ring and $L$ a field extension of $K$ via a ring homomorphism $i : K \to L$. For any polynomial $f \in K[X]$, if the natural degree of $f$ is exactly 1 (i.e., $\text{natDegree}(f) = 1$), then $f$ splits over $L$ via $i$.

Polynomial.splits_mul theorem

{f g : K[X]} (hf : Splits i f) (hg : Splits i g) : Splits i (f * g)

Full source

theorem splits_mul {f g : K[X]} (hf : Splits i f) (hg : Splits i g) : Splits i (f * g) :=
  letI := Classical.decEq L
  if h : (f * g).map i = 0 then Or.inl h
  else
    Or.inr @fun p hp hpf =>
      ((irreducible_iff_prime.1 hp).2.2 _ _
            (show p ∣ map i f * map i g by convert hpf; rw [Polynomial.map_mul])).elim
        (hf.resolve_left (fun hf => by simp [hf] at h) hp)
        (hg.resolve_left (fun hg => by simp [hg] at h) hp)

Product of Splitting Polynomials Splits

Informal description

Let $K$ be a commutative ring and $L$ a field, with a ring homomorphism $i : K \to L$. For any polynomials $f, g \in K[X]$, if $f$ splits over $L$ via $i$ and $g$ splits over $L$ via $i$, then their product $f \cdot g$ also splits over $L$ via $i$.

Polynomial.splits_of_splits_mul' theorem

{f g : K[X]} (hfg : (f * g).map i ≠ 0) (h : Splits i (f * g)) : Splits i f ∧ Splits i g

Full source

theorem splits_of_splits_mul' {f g : K[X]} (hfg : (f * g).map i ≠ 0) (h : Splits i (f * g)) :
    SplitsSplits i f ∧ Splits i g :=
  ⟨Or.inr @fun g hgi hg =>
      Or.resolve_left h hfg hgi (by rw [Polynomial.map_mul]; exact hg.trans (dvd_mul_right _ _)),
    Or.inr @fun g hgi hg =>
      Or.resolve_left h hfg hgi (by rw [Polynomial.map_mul]; exact hg.trans (dvd_mul_left _ _))⟩

Splitting of Factors in Polynomial Multiplication over Field Extension

Informal description

Let $K$ be a commutative ring and $L$ a field, with a ring homomorphism $i : K \to L$. For any nonzero polynomials $f, g \in K[X]$ such that the product $f \cdot g$ splits over $L$ via $i$, both $f$ and $g$ split over $L$ via $i$. Here, a polynomial splits over $L$ if it is either zero or all its irreducible factors over $L$ have degree $1$.

Polynomial.splits_map_iff theorem

(j : L →+* F) {f : K[X]} : Splits j (f.map i) ↔ Splits (j.comp i) f

Full source

theorem splits_map_iff (j : L →+* F) {f : K[X]} : SplitsSplits j (f.map i) ↔ Splits (j.comp i) f := by
  simp [Splits, Polynomial.map_map]

Splitting Criterion via Composition of Field Homomorphisms: $f$ splits over $F$ via $j \circ i$ $\leftrightarrow$ $f \circ i$ splits over $F$ via $j$

Informal description

Let $K$, $L$, and $F$ be fields with ring homomorphisms $i \colon K \to L$ and $j \colon L \to F$. For any polynomial $f \in K[X]$, the following are equivalent: 1. The polynomial $f$ splits over $F$ via the homomorphism $j \circ i \colon K \to F$. 2. The polynomial $f$ splits over $F$ via the homomorphism $j \colon L \to F$ after being mapped by $i$ (i.e., $f \mapsto f \circ i$). In other words, $f$ splits over $F$ via the composition $j \circ i$ if and only if its image under $i$ splits over $F$ via $j$.

Polynomial.splits_one theorem

: Splits i 1

Full source

theorem splits_one : Splits i 1 :=
  splits_C i 1

Splitting of the Unit Polynomial

Informal description

The constant polynomial $1 \in K[X]$ splits over any field extension $L$ of $K$ via the ring homomorphism $i \colon K \to L$.

Polynomial.splits_of_isUnit theorem

[IsDomain K] {u : K[X]} (hu : IsUnit u) : u.Splits i

Full source

theorem splits_of_isUnit [IsDomain K] {u : K[X]} (hu : IsUnit u) : u.Splits i :=
  (isUnit_iff.mp hu).choose_spec.2 ▸ splits_C _ _

Units in Polynomial Ring Split over Any Field Extension

Informal description

Let $K$ be a commutative ring that is a domain, and let $L$ be a field. For any unit $u$ in the polynomial ring $K[X]$, the polynomial $u$ splits over $L$ via any ring homomorphism $i \colon K \to L$.

Polynomial.splits_X_sub_C theorem

{x : K} : (X - C x).Splits i

Full source

theorem splits_X_sub_C {x : K} : (X - C x).Splits i :=
  splits_of_degree_le_one _ <| degree_X_sub_C_le _

Linear Polynomials Split in Any Field Extension

Informal description

For any element $x$ in a commutative ring $K$ and any ring homomorphism $i : K \to L$ to a field $L$, the linear polynomial $X - x$ splits over $L$ via $i$.

Polynomial.splits_X theorem

: X.Splits i

Full source

theorem splits_X : X.Splits i :=
  splits_of_degree_le_one _ degree_X_le

Splitting of the Polynomial Variable $X$

Informal description

The polynomial variable $X$ splits over any field extension $L$ of $K$ via the ring homomorphism $i : K \to L$. That is, the polynomial $X$ is either zero or all of its irreducible factors over $L$ have degree $1$.

Polynomial.splits_prod theorem

{ι : Type u} {s : ι → K[X]} {t : Finset ι} : (∀ j ∈ t, (s j).Splits i) → (∏ x ∈ t, s x).Splits i

Full source

theorem splits_prod {ι : Type u} {s : ι → K[X]} {t : Finset ι} :
    (∀ j ∈ t, (s j).Splits i) → (∏ x ∈ t, s x).Splits i := by
  classical
  refine Finset.induction_on t (fun _ => splits_one i) fun a t hat ih ht => ?_
  rw [Finset.forall_mem_insert] at ht; rw [Finset.prod_insert hat]
  exact splits_mul i ht.1 (ih ht.2)

Product of Splitting Polynomials Splits Over Field Extension

Informal description

Let $K$ be a commutative ring, $L$ a field, and $i \colon K \to L$ a ring homomorphism. Given a finite set $t$ of indices and a family of polynomials $(s_j)_{j \in t}$ in $K[X]$, if each polynomial $s_j$ splits over $L$ via $i$, then their product $\prod_{j \in t} s_j$ also splits over $L$ via $i$.

Polynomial.splits_pow theorem

{f : K[X]} (hf : f.Splits i) (n : ℕ) : (f ^ n).Splits i

Full source

theorem splits_pow {f : K[X]} (hf : f.Splits i) (n : ℕ) : (f ^ n).Splits i := by
  rw [← Finset.card_range n, ← Finset.prod_const]
  exact splits_prod i fun j _ => hf

Powers of Splitting Polynomials Split Over Field Extension

Informal description

Let $K$ be a commutative ring, $L$ a field, and $i \colon K \to L$ a ring homomorphism. For any polynomial $f \in K[X]$ that splits over $L$ via $i$ and any natural number $n$, the polynomial $f^n$ also splits over $L$ via $i$.

Polynomial.splits_X_pow theorem

(n : ℕ) : (X ^ n).Splits i

Full source

theorem splits_X_pow (n : ℕ) : (X ^ n).Splits i :=
  splits_pow i (splits_X i) n

Splitting of $X^n$ over Field Extension via Ring Homomorphism

Informal description

For any natural number $n$, the polynomial $X^n$ splits over the field extension $L$ of $K$ via the ring homomorphism $i \colon K \to L$. That is, either $X^n$ is zero or all of its irreducible factors over $L$ have degree $1$.

Polynomial.splits_id_iff_splits theorem

{f : K[X]} : (f.map i).Splits (RingHom.id L) ↔ f.Splits i

Full source

theorem splits_id_iff_splits {f : K[X]} : (f.map i).Splits (RingHom.id L) ↔ f.Splits i := by
  rw [splits_map_iff, RingHom.id_comp]

Splitting Criterion via Identity Homomorphism: $f$ splits over $L$ via $i$ $\leftrightarrow$ $f \circ i$ splits over $L$ via $\text{id}_L$

Informal description

Let $K$ and $L$ be fields with a ring homomorphism $i \colon K \to L$. For any polynomial $f \in K[X]$, the following are equivalent: 1. The polynomial $f$ splits over $L$ via $i$. 2. The polynomial $f \circ i$ splits over $L$ via the identity homomorphism $\text{id}_L \colon L \to L$. In other words, $f$ splits over $L$ via $i$ if and only if its image under $i$ splits over $L$ via the identity map.

Polynomial.Splits.comp_of_map_degree_le_one theorem

{f : K[X]} {p : K[X]} (hd : (p.map i).degree ≤ 1) (h : f.Splits i) : (f.comp p).Splits i

Full source

theorem Splits.comp_of_map_degree_le_one {f : K[X]} {p : K[X]} (hd : (p.map i).degree ≤ 1)
    (h : f.Splits i) : (f.comp p).Splits i := by
  by_cases hzero : map i (f.comp p) = 0
  · exact Or.inl hzero
  cases h with
  | inl h0 =>
    exact Or.inl <| map_comp i _ _ ▸ h0.symm ▸ zero_comp
  | inr h =>
    right
    intro g irr dvd
    rw [map_comp] at dvd hzero
    cases lt_or_eq_of_le hd with
    | inl hd =>
      rw [eq_C_of_degree_le_zero (Nat.WithBot.lt_one_iff_le_zero.mp hd), comp_C] at dvd hzero
      refine False.elim (irr.1 (isUnit_of_dvd_unit dvd ?_))
      simpa using hzero
    | inr hd =>
      let _ := invertibleOfNonzero (leadingCoeff_ne_zero.mpr
          (ne_zero_of_degree_gt (n := ⊥) (by rw [hd]; decide)))
      rw [eq_X_add_C_of_degree_eq_one hd, dvd_comp_C_mul_X_add_C_iff _ _] at dvd
      have := h (irr.map (algEquivCMulXAddC _ _).symm) dvd
      rw [degree_eq_natDegree irr.ne_zero]
      rwa [algEquivCMulXAddC_symm_apply, ← comp_eq_aeval,
        degree_eq_natDegree (fun h => WithBot.bot_ne_one (h ▸ this)),
        natDegree_comp, natDegree_C_mul (invertibleInvOf.ne_zero),
        natDegree_X_sub_C, mul_one] at this

Splitting Preservation under Composition with Degree $\leq$ 1 Polynomial

Informal description

Let $K$ and $L$ be fields with a ring homomorphism $i \colon K \to L$. For any polynomial $f \in K[X]$, if: 1. The degree of $p \circ i$ is at most 1 (i.e., $\deg(p \circ i) \leq 1$), and 2. $f$ splits over $L$ via $i$, then the composition $f \circ p$ also splits over $L$ via $i$.

Polynomial.splits_iff_comp_splits_of_degree_eq_one theorem

{f : K[X]} {p : K[X]} (hd : (p.map i).degree = 1) : f.Splits i ↔ (f.comp p).Splits i

Full source

theorem splits_iff_comp_splits_of_degree_eq_one {f : K[X]} {p : K[X]} (hd : (p.map i).degree = 1) :
    f.Splits i ↔ (f.comp p).Splits i := by
  rw [← splits_id_iff_splits, ← splits_id_iff_splits (f := f.comp p), map_comp]
  refine ⟨fun h => Splits.comp_of_map_degree_le_one
    (le_of_eq (map_id (R := L) ▸ hd)) h, fun h => ?_⟩
  let _ := invertibleOfNonzero (leadingCoeff_ne_zero.mpr
      (ne_zero_of_degree_gt (n := ⊥) (by rw [hd]; decide)))
  have : (map i f) = ((map i f).comp (map i p)).comp ((C ⅟ (map i p).leadingCoeff *
      (X - C ((map i p).coeff 0)))) := by
    rw [comp_assoc]
    nth_rw 1 [eq_X_add_C_of_degree_eq_one hd]
    simp only [coeff_map, invOf_eq_inv, mul_sub, ← C_mul, add_comp, mul_comp, C_comp, X_comp,
      ← mul_assoc]
    simp
  refine this ▸ Splits.comp_of_map_degree_le_one ?_ h
  simp [degree_C (inv_ne_zero (Invertible.ne_zero (a := (map i p).leadingCoeff)))]

Splitting Equivalence for Composition with Degree 1 Polynomial: $f$ splits $\leftrightarrow$ $f \circ p$ splits when $\deg(p \circ i) = 1$

Informal description

Let $K$ and $L$ be fields with a ring homomorphism $i \colon K \to L$. For any polynomials $f, p \in K[X]$, if the degree of $p \circ i$ equals 1 (i.e., $\deg(p \circ i) = 1$), then $f$ splits over $L$ via $i$ if and only if the composition $f \circ p$ splits over $L$ via $i$.

Polynomial.Splits.comp_of_degree_le_one theorem

{f : K[X]} {p : K[X]} (hd : p.degree ≤ 1) (h : f.Splits i) : (f.comp p).Splits i

Full source

/--
This is a weaker variant of `Splits.comp_of_map_degree_le_one`,
but its conditions are easier to check.
-/
theorem Splits.comp_of_degree_le_one {f : K[X]} {p : K[X]} (hd : p.degree ≤ 1)
    (h : f.Splits i) : (f.comp p).Splits i :=
  Splits.comp_of_map_degree_le_one (degree_map_le.trans hd) h

Splitting Preservation under Composition with Degree $\leq$ 1 Polynomial (Simplified Conditions)

Informal description

Let $K$ and $L$ be fields with a ring homomorphism $i \colon K \to L$. For any polynomial $f \in K[X]$, if: 1. The degree of $p$ is at most 1 (i.e., $\deg(p) \leq 1$), and 2. $f$ splits over $L$ via $i$, then the composition $f \circ p$ also splits over $L$ via $i$.

Polynomial.Splits.comp_X_sub_C theorem

(a : K) {f : K[X]} (h : f.Splits i) : (f.comp (X - C a)).Splits i

Full source

theorem Splits.comp_X_sub_C (a : K) {f : K[X]}
    (h : f.Splits i) : (f.comp (X - C a)).Splits i :=
  Splits.comp_of_degree_le_one (degree_X_sub_C_le _) h

Splitting Preservation under Composition with $X - a$

Informal description

Let $K$ and $L$ be fields with a ring homomorphism $i \colon K \to L$. For any element $a \in K$ and any polynomial $f \in K[X]$, if $f$ splits over $L$ via $i$, then the composition $f(X - a)$ also splits over $L$ via $i$.

Polynomial.Splits.comp_X_add_C theorem

(a : K) {f : K[X]} (h : f.Splits i) : (f.comp (X + C a)).Splits i

Full source

theorem Splits.comp_X_add_C (a : K) {f : K[X]}
    (h : f.Splits i) : (f.comp (X + C a)).Splits i :=
  Splits.comp_of_degree_le_one (by simpa using degree_X_sub_C_le (-a)) h

Splitting Preservation under Composition with $X + a$

Informal description

Let $K$ and $L$ be fields with a ring homomorphism $i \colon K \to L$. For any polynomial $f \in K[X]$ that splits over $L$ via $i$, and for any element $a \in K$, the composition $f \circ (X + a)$ also splits over $L$ via $i$.

Polynomial.Splits.comp_neg_X theorem

{f : K[X]} (h : f.Splits i) : (f.comp (-X)).Splits i

Full source

theorem Splits.comp_neg_X {f : K[X]} (h : f.Splits i) : (f.comp (-X)).Splits i :=
  Splits.comp_of_degree_le_one (by simpa using degree_X_sub_C_le (0 : K)) h

Splitting Preservation under Composition with $-X$

Informal description

Let $K$ be a commutative ring and $L$ a field extension of $K$ via a ring homomorphism $i \colon K \to L$. For any polynomial $f \in K[X]$ that splits over $L$ via $i$, the composition $f \circ (-X)$ also splits over $L$ via $i$.

Polynomial.exists_root_of_splits' theorem

{f : K[X]} (hs : Splits i f) (hf0 : degree (f.map i) ≠ 0) : ∃ x, eval₂ i x f = 0

Full source

theorem exists_root_of_splits' {f : K[X]} (hs : Splits i f) (hf0 : degreedegree (f.map i) ≠ 0) :
    ∃ x, eval₂ i x f = 0 :=
  letI := Classical.decEq L
  if hf0' : f.map i = 0 then by simp [eval₂_eq_eval_map, hf0']
  else
    let ⟨g, hg⟩ :=
      WfDvdMonoid.exists_irreducible_factor
        (show ¬IsUnit (f.map i) from mt isUnit_iff_degree_eq_zero.1 hf0) hf0'
    let ⟨x, hx⟩ := exists_root_of_degree_eq_one (hs.resolve_left hf0' hg.1 hg.2)
    let ⟨i, hi⟩ := hg.2
    ⟨x, by rw [← eval_map, hi, eval_mul, show _ = _ from hx, zero_mul]⟩

Existence of Roots for Splitting Polynomials over Field Extensions

Informal description

Let $K$ be a commutative ring and $L$ a field extension of $K$ via a ring homomorphism $i : K \to L$. For any polynomial $f \in K[X]$ that splits over $L$ (i.e., either $f = 0$ or all irreducible factors of $f$ over $L$ have degree 1), if the degree of $f$ under the extension $i$ is nonzero, then there exists an element $x \in L$ such that evaluating $f$ at $x$ via $i$ yields zero, i.e., $\text{eval}_2(i, x, f) = 0$.

Polynomial.roots_ne_zero_of_splits' theorem

{f : K[X]} (hs : Splits i f) (hf0 : natDegree (f.map i) ≠ 0) : (f.map i).roots ≠ 0

Full source

theorem roots_ne_zero_of_splits' {f : K[X]} (hs : Splits i f) (hf0 : natDegreenatDegree (f.map i) ≠ 0) :
    (f.map i).roots ≠ 0 :=
  let ⟨x, hx⟩ := exists_root_of_splits' i hs fun h => hf0 <| natDegree_eq_of_degree_eq_some h
  fun h => by
  rw [← eval_map] at hx
  have : f.map i ≠ 0 := by intro; simp_all
  cases h.subst ((mem_roots this).2 hx)

Nonempty Roots for Splitting Polynomials with Nonzero Degree

Informal description

Let $K$ be a commutative ring and $L$ a field extension of $K$ via a ring homomorphism $i : K \to L$. For any polynomial $f \in K[X]$ that splits over $L$ (i.e., either $f = 0$ or all irreducible factors of $f$ over $L$ have degree 1), if the natural degree of $f$ under the extension $i$ is nonzero, then the multiset of roots of $f$ in $L$ is nonempty.

Polynomial.rootOfSplits' definition

{f : K[X]} (hf : f.Splits i) (hfd : (f.map i).degree ≠ 0) : L

Full source

/-- Pick a root of a polynomial that splits. See `rootOfSplits` for polynomials over a field
which has simpler assumptions. -/
def rootOfSplits' {f : K[X]} (hf : f.Splits i) (hfd : (f.map i).degree ≠ 0) : L :=
  Classical.choose <| exists_root_of_splits' i hf hfd

Root of a splitting polynomial over a field extension

Informal description

Given a polynomial $ f \in K[X] $ that splits over a field extension $ L $ of $ K $ via a ring homomorphism $ i : K \to L $, and assuming the degree of $ f $ under the extension $ i $ is nonzero, the function returns a root of $ f $ in $ L $. Specifically, it picks a root $ x \in L $ such that evaluating $ f $ at $ x $ via $ i $ yields zero, i.e., $ \text{eval}_2(i, x, f) = 0 $.

Polynomial.map_rootOfSplits' theorem

{f : K[X]} (hf : f.Splits i) (hfd) : f.eval₂ i (rootOfSplits' i hf hfd) = 0

Full source

theorem map_rootOfSplits' {f : K[X]} (hf : f.Splits i) (hfd) :
    f.eval₂ i (rootOfSplits' i hf hfd) = 0 :=
  Classical.choose_spec <| exists_root_of_splits' i hf hfd

Evaluation of Splitting Polynomial at Root is Zero

Informal description

Let $K$ be a commutative ring and $L$ a field extension of $K$ via a ring homomorphism $i : K \to L$. For any polynomial $f \in K[X]$ that splits over $L$ (i.e., either $f = 0$ or all irreducible factors of $f$ over $L$ have degree 1), and assuming the degree of $f$ under the extension $i$ is nonzero, the evaluation of $f$ at the root $\text{rootOfSplits'}(i, hf, hfd) \in L$ via $i$ equals zero, i.e., $$ \text{eval}_2(i, \text{rootOfSplits'}(i, hf, hfd), f) = 0. $$

Polynomial.natDegree_eq_card_roots' theorem

{p : K[X]} {i : K →+* L} (hsplit : Splits i p) : (p.map i).natDegree = Multiset.card (p.map i).roots

Full source

theorem natDegree_eq_card_roots' {p : K[X]} {i : K →+* L} (hsplit : Splits i p) :
    (p.map i).natDegree = Multiset.card (p.map i).roots := by
  by_cases hp : p.map i = 0
  · rw [hp, natDegree_zero, roots_zero, Multiset.card_zero]
  obtain ⟨q, he, hd, hr⟩ := exists_prod_multiset_X_sub_C_mul (p.map i)
  rw [← splits_id_iff_splits, ← he] at hsplit
  rw [← he] at hp
  have hq : q ≠ 0 := fun h => hp (by rw [h, mul_zero])
  rw [← hd, add_eq_left]
  by_contra h
  have h' : (map (RingHom.id L) q).natDegree ≠ 0 := by simp [h]
  have := roots_ne_zero_of_splits' (RingHom.id L) (splits_of_splits_mul' _ ?_ hsplit).2 h'
  · rw [map_id] at this
    exact this hr
  · rw [map_id]
    exact mul_ne_zero (monic_multisetProd_X_sub_C _).ne_zero hq

Natural Degree Equals Root Count for Splitting Polynomials

Informal description

Let $K$ be a commutative ring and $L$ a field, with a ring homomorphism $i \colon K \to L$. For any polynomial $p \in K[X]$ that splits over $L$ via $i$ (i.e., either $p = 0$ or all irreducible factors of $p$ over $L$ have degree 1), the natural degree of $p$ under the extension $i$ equals the number of roots (counting multiplicities) of $p$ in $L$, i.e., \[ \text{natDegree}(p \circ i) = |\text{roots}(p \circ i)|. \]

Polynomial.degree_eq_card_roots' theorem

 {p : K[X]} {i : K →+* L} (p_ne_zero : p.map i ≠ 0) (hsplit : Splits i p) :
  (p.map i).degree = Multiset.card (p.map i).roots

Full source

theorem degree_eq_card_roots' {p : K[X]} {i : K →+* L} (p_ne_zero : p.map i ≠ 0)
    (hsplit : Splits i p) : (p.map i).degree = Multiset.card (p.map i).roots := by
  simp [degree_eq_natDegree p_ne_zero, natDegree_eq_card_roots' hsplit]

Degree Equals Root Count for Splitting Polynomials

Informal description

Let $K$ be a commutative ring and $L$ a field, with a ring homomorphism $i \colon K \to L$. For any nonzero polynomial $p \in K[X]$ that splits over $L$ via $i$ (i.e., all irreducible factors of $p$ over $L$ have degree 1), the degree of $p$ under the extension $i$ equals the number of roots (counting multiplicities) of $p$ in $L$, i.e., \[ \deg(p \circ i) = |\text{roots}(p \circ i)|. \]

Polynomial.aeval_root_of_mapAlg_eq_multiset_prod_X_sub_C theorem

 [CommSemiring R] [CommRing L] [Algebra R L] (s : Multiset L) {x : L} (hx : x ∈ s) {p : R[X]}
  (hp : mapAlg R L p = (Multiset.map (fun a : L ↦ X - C a) s).prod) : aeval x p = 0

Full source

theorem aeval_root_of_mapAlg_eq_multiset_prod_X_sub_C [CommSemiring R] [CommRing L] [Algebra R L]
    (s : Multiset L) {x : L} (hx : x ∈ s) {p : R[X]}
    (hp : mapAlg R L p = (Multiset.map (fun a : L ↦ X - C a) s).prod) : aeval x p = 0 := by
  rw [← aeval_map_algebraMap L, ← mapAlg_eq_map, hp, map_multiset_prod, Multiset.prod_eq_zero]
  rw [Multiset.map_map, Multiset.mem_map]
  exact ⟨x, hx, by simp⟩

Root Evaluation for Polynomials Factored as Product of Linear Terms

Informal description

Let $R$ be a commutative semiring, $L$ a commutative ring with an $R$-algebra structure, and $s$ a multiset of elements in $L$. For any element $x \in s$ and any polynomial $p \in R[X]$, if the algebra homomorphism $\text{mapAlg}_{R \to L}$ applied to $p$ equals the product $\prod_{a \in s} (X - a)$ in $L[X]$, then the evaluation of $p$ at $x$ is zero, i.e., $p(x) = 0$.

Polynomial.splits_iff theorem

(f : K[X]) : Splits i f ↔ f = 0 ∨ ∀ {g : L[X]}, Irreducible g → g ∣ f.map i → degree g = 1

Full source

/-- This lemma is for polynomials over a field. -/
theorem splits_iff (f : K[X]) :
    SplitsSplits i f ↔ f = 0 ∨ ∀ {g : L[X]}, Irreducible g → g ∣ f.map i → degree g = 1 := by
  rw [Splits, Polynomial.map_eq_zero]

Characterization of Polynomial Splitting over Field Extension

Informal description

Let $K$ be a field and $L$ be a field extension of $K$ via a ring homomorphism $i: K \to L$. A polynomial $f \in K[X]$ splits over $L$ if and only if either $f = 0$ or every irreducible factor $g$ of $f$ over $L$ (i.e., $g \mid f \circ i$ and $g$ is irreducible in $L[X]$) has degree $1$.

Polynomial.Splits.def theorem

 {i : K →+* L} {f : K[X]} (h : Splits i f) : f = 0 ∨ ∀ {g : L[X]}, Irreducible g → g ∣ f.map i → degree g = 1

Full source

/-- This lemma is for polynomials over a field. -/
theorem Splits.def {i : K →+* L} {f : K[X]} (h : Splits i f) :
    f = 0 ∨ ∀ {g : L[X]}, Irreducible g → g ∣ f.map i → degree g = 1 :=
  (splits_iff i f).mp h

Characterization of Splitting Polynomials via Irreducible Factors of Degree 1

Informal description

Let $K$ be a field, $L$ a field extension of $K$, and $i: K \to L$ a ring homomorphism. If a polynomial $f \in K[X]$ splits over $L$ via $i$, then either $f = 0$ or every irreducible factor $g$ of $f$ over $L$ (i.e., $g$ divides $f \circ i$ and $g$ is irreducible in $L[X]$) has degree $1$.

Polynomial.splits_of_splits_mul theorem

{f g : K[X]} (hfg : f * g ≠ 0) (h : Splits i (f * g)) : Splits i f ∧ Splits i g

Full source

theorem splits_of_splits_mul {f g : K[X]} (hfg : f * g ≠ 0) (h : Splits i (f * g)) :
    SplitsSplits i f ∧ Splits i g :=
  splits_of_splits_mul' i (map_ne_zero hfg) h

Splitting of Factors in Polynomial Multiplication over Field Extension

Informal description

Let $K$ be a commutative ring, $L$ a field, and $i \colon K \to L$ a ring homomorphism. For any nonzero polynomials $f, g \in K[X]$ such that $f \cdot g$ splits over $L$ via $i$, both $f$ and $g$ split over $L$ via $i$. Here, a polynomial splits over $L$ if it is either zero or all its irreducible factors over $L$ have degree $1$.

Polynomial.splits_of_splits_of_dvd theorem

{f g : K[X]} (hf0 : f ≠ 0) (hf : Splits i f) (hgf : g ∣ f) : Splits i g

Full source

theorem splits_of_splits_of_dvd {f g : K[X]} (hf0 : f ≠ 0) (hf : Splits i f) (hgf : g ∣ f) :
    Splits i g := by
  obtain ⟨f, rfl⟩ := hgf
  exact (splits_of_splits_mul i hf0 hf).1

Divisibility Preserves Splitting Condition for Polynomials over Field Extension

Informal description

Let $K$ be a commutative ring, $L$ a field, and $i \colon K \to L$ a ring homomorphism. For any nonzero polynomial $f \in K[X]$ that splits over $L$ via $i$, and any polynomial $g \in K[X]$ that divides $f$, the polynomial $g$ also splits over $L$ via $i$. Here, a polynomial splits over $L$ if it is either zero or all its irreducible factors over $L$ have degree $1$.

Polynomial.splits_of_splits_gcd_left theorem

[DecidableEq K] {f g : K[X]} (hf0 : f ≠ 0) (hf : Splits i f) : Splits i (EuclideanDomain.gcd f g)

Full source

theorem splits_of_splits_gcd_left [DecidableEq K] {f g : K[X]} (hf0 : f ≠ 0) (hf : Splits i f) :
    Splits i (EuclideanDomain.gcd f g) :=
  Polynomial.splits_of_splits_of_dvd i hf0 hf (EuclideanDomain.gcd_dvd_left f g)

Splitting of GCD with Left Factor in Polynomial Ring over Field Extension

Informal description

Let $K$ be a field with decidable equality, $L$ a field, and $i \colon K \to L$ a ring homomorphism. For any nonzero polynomial $f \in K[X]$ that splits over $L$ via $i$, the greatest common divisor $\gcd(f, g)$ also splits over $L$ via $i$ for any polynomial $g \in K[X]$. Here, a polynomial splits over $L$ if it is either zero or all its irreducible factors over $L$ have degree $1$.

Polynomial.splits_of_splits_gcd_right theorem

[DecidableEq K] {f g : K[X]} (hg0 : g ≠ 0) (hg : Splits i g) : Splits i (EuclideanDomain.gcd f g)

Full source

theorem splits_of_splits_gcd_right [DecidableEq K] {f g : K[X]} (hg0 : g ≠ 0) (hg : Splits i g) :
    Splits i (EuclideanDomain.gcd f g) :=
  Polynomial.splits_of_splits_of_dvd i hg0 hg (EuclideanDomain.gcd_dvd_right f g)

Splitting condition for GCD of polynomials: right version

Informal description

Let $K$ be a field with decidable equality, $L$ a field, and $i \colon K \to L$ a ring homomorphism. For any nonzero polynomial $g \in K[X]$ that splits over $L$ via $i$, and any polynomial $f \in K[X]$, the greatest common divisor $\gcd(f, g)$ also splits over $L$ via $i$. Here, a polynomial splits over $L$ if it is either zero or all its irreducible factors over $L$ have degree $1$.

Polynomial.splits_mul_iff theorem

{f g : K[X]} (hf : f ≠ 0) (hg : g ≠ 0) : (f * g).Splits i ↔ f.Splits i ∧ g.Splits i

Full source

theorem splits_mul_iff {f g : K[X]} (hf : f ≠ 0) (hg : g ≠ 0) :
    (f * g).Splits i ↔ f.Splits i ∧ g.Splits i :=
  ⟨splits_of_splits_mul i (mul_ne_zero hf hg), fun ⟨hfs, hgs⟩ => splits_mul i hfs hgs⟩

Splitting Criterion for Product of Nonzero Polynomials over Field Extension

Informal description

Let $K$ be a commutative ring, $L$ a field, and $i \colon K \to L$ a ring homomorphism. For any nonzero polynomials $f, g \in K[X]$, the product $f \cdot g$ splits over $L$ via $i$ if and only if both $f$ and $g$ split over $L$ via $i$. Here, a polynomial splits over $L$ if it is either zero or all its irreducible factors over $L$ have degree $1$.

Polynomial.splits_prod_iff theorem

 {ι : Type u} {s : ι → K[X]} {t : Finset ι} : (∀ j ∈ t, s j ≠ 0) → ((∏ x ∈ t, s x).Splits i ↔ ∀ j ∈ t, (s j).Splits i)

Full source

theorem splits_prod_iff {ι : Type u} {s : ι → K[X]} {t : Finset ι} :
    (∀ j ∈ t, s j ≠ 0) → ((∏ x ∈ t, s x).Splits i ↔ ∀ j ∈ t, (s j).Splits i) := by
  classical
  refine
    Finset.induction_on t (fun _ =>
        ⟨fun _ _ h => by simp only [Finset.not_mem_empty] at h, fun _ => splits_one i⟩)
      fun a t hat ih ht => ?_
  rw [Finset.forall_mem_insert] at ht ⊢
  rw [Finset.prod_insert hat, splits_mul_iff i ht.1 (Finset.prod_ne_zero_iff.2 ht.2), ih ht.2]

Splitting Criterion for Finite Product of Nonzero Polynomials over Field Extension

Informal description

Let $K$ be a commutative ring, $L$ a field, and $i \colon K \to L$ a ring homomorphism. Given a finite set $t$ and a family of nonzero polynomials $(s_j)_{j \in t}$ in $K[X]$, the product $\prod_{j \in t} s_j$ splits over $L$ via $i$ if and only if each $s_j$ splits over $L$ via $i$. Here, a polynomial splits over $L$ if it is either zero or all its irreducible factors over $L$ have degree $1$.

Polynomial.degree_eq_one_of_irreducible_of_splits theorem

{p : K[X]} (hp : Irreducible p) (hp_splits : Splits (RingHom.id K) p) : p.degree = 1

Full source

theorem degree_eq_one_of_irreducible_of_splits {p : K[X]} (hp : Irreducible p)
    (hp_splits : Splits (RingHom.id K) p) : p.degree = 1 := by
  rcases hp_splits with ⟨⟩ | hp_splits
  · exfalso
    simp_all
  · apply hp_splits hp
    simp

Irreducible polynomials splitting over their base field have degree one

Informal description

Let $K$ be a field and $p \in K[X]$ be an irreducible polynomial. If $p$ splits over $K$ (via the identity homomorphism), then $p$ has degree $1$.

Polynomial.exists_root_of_splits theorem

{f : K[X]} (hs : Splits i f) (hf0 : degree f ≠ 0) : ∃ x, eval₂ i x f = 0

Full source

theorem exists_root_of_splits {f : K[X]} (hs : Splits i f) (hf0 : degreedegree f ≠ 0) :
    ∃ x, eval₂ i x f = 0 :=
  exists_root_of_splits' i hs ((f.degree_map i).symm ▸ hf0)

Existence of Roots for Splitting Polynomials over Field Extensions

Informal description

Let $K$ be a commutative ring and $L$ a field extension of $K$ via a ring homomorphism $i : K \to L$. For any polynomial $f \in K[X]$ that splits over $L$ (i.e., either $f = 0$ or all irreducible factors of $f$ over $L$ have degree 1), if the degree of $f$ is nonzero, then there exists an element $x \in L$ such that evaluating $f$ at $x$ via $i$ yields zero, i.e., $\text{eval}_2(i, x, f) = 0$.

Polynomial.roots_ne_zero_of_splits theorem

{f : K[X]} (hs : Splits i f) (hf0 : natDegree f ≠ 0) : (f.map i).roots ≠ 0

Full source

theorem roots_ne_zero_of_splits {f : K[X]} (hs : Splits i f) (hf0 : natDegreenatDegree f ≠ 0) :
    (f.map i).roots ≠ 0 :=
  roots_ne_zero_of_splits' i hs (ne_of_eq_of_ne (natDegree_map i) hf0)

Nonempty Roots for Splitting Polynomials with Nonzero Natural Degree

Informal description

Let $K$ be a commutative ring and $L$ a field extension of $K$ via a ring homomorphism $i : K \to L$. For any polynomial $f \in K[X]$ that splits over $L$ (i.e., either $f = 0$ or all irreducible factors of $f$ over $L$ have degree 1), if the natural degree of $f$ is nonzero, then the multiset of roots of $f$ in $L$ is nonempty.

Polynomial.rootOfSplits definition

{f : K[X]} (hf : f.Splits i) (hfd : f.degree ≠ 0) : L

Full source

/-- Pick a root of a polynomial that splits. This version is for polynomials over a field and has
simpler assumptions. -/
def rootOfSplits {f : K[X]} (hf : f.Splits i) (hfd : f.degree ≠ 0) : L :=
  rootOfSplits' i hf ((f.degree_map i).symm ▸ hfd)

Root of a splitting polynomial over a field extension

Informal description

Given a polynomial $ f \in K[X] $ that splits over a field extension $ L $ of $ K $ via a ring homomorphism $ i : K \to L $, and assuming the degree of $ f $ is nonzero, the function returns a root of $ f $ in $ L $. Specifically, it picks a root $ x \in L $ such that evaluating $ f $ at $ x $ via $ i $ yields zero, i.e., $ \text{eval}_2(i, x, f) = 0 $.

Polynomial.rootOfSplits'_eq_rootOfSplits theorem

{f : K[X]} (hf : f.Splits i) (hfd) : rootOfSplits' i hf hfd = rootOfSplits i hf (f.degree_map i ▸ hfd)

Full source

/-- `rootOfSplits'` is definitionally equal to `rootOfSplits`. -/
theorem rootOfSplits'_eq_rootOfSplits {f : K[X]} (hf : f.Splits i) (hfd) :
    rootOfSplits' i hf hfd = rootOfSplits i hf (f.degree_map i ▸ hfd) :=
  rfl

Equality of Roots from Splitting Polynomial Variants

Informal description

Let $K$ be a commutative ring and $L$ a field extension of $K$ via a ring homomorphism $i : K \to L$. For any polynomial $f \in K[X]$ that splits over $L$ (i.e., either $f = 0$ or all irreducible factors of $f$ over $L$ have degree 1), and assuming the degree of $f$ under the extension $i$ is nonzero, the root obtained from `rootOfSplits'` is equal to the root obtained from `rootOfSplits` when considering the degree of the mapped polynomial.

Polynomial.map_rootOfSplits theorem

{f : K[X]} (hf : f.Splits i) (hfd) : f.eval₂ i (rootOfSplits i hf hfd) = 0

Full source

theorem map_rootOfSplits {f : K[X]} (hf : f.Splits i) (hfd) :
    f.eval₂ i (rootOfSplits i hf hfd) = 0 :=
  map_rootOfSplits' i hf (ne_of_eq_of_ne (degree_map f i) hfd)

Evaluation of Splitting Polynomial at Root is Zero

Informal description

Let $K$ be a commutative ring and $L$ a field extension of $K$ via a ring homomorphism $i : K \to L$. For any polynomial $f \in K[X]$ that splits over $L$ (i.e., either $f = 0$ or all irreducible factors of $f$ over $L$ have degree 1), and assuming the degree of $f$ under the extension $i$ is nonzero, the evaluation of $f$ at the root $\text{rootOfSplits}(i, hf, hfd) \in L$ via $i$ equals zero, i.e., $$ \text{eval}_2(i, \text{rootOfSplits}(i, hf, hfd), f) = 0. $$

Polynomial.natDegree_eq_card_roots theorem

{p : K[X]} {i : K →+* L} (hsplit : Splits i p) : p.natDegree = Multiset.card (p.map i).roots

Full source

theorem natDegree_eq_card_roots {p : K[X]} {i : K →+* L} (hsplit : Splits i p) :
    p.natDegree = Multiset.card (p.map i).roots :=
  (natDegree_map i).symm.trans <| natDegree_eq_card_roots' hsplit

Natural Degree Equals Root Count for Splitting Polynomials

Informal description

Let $K$ be a commutative ring and $L$ a field, with a ring homomorphism $i \colon K \to L$. For any polynomial $p \in K[X]$ that splits over $L$ via $i$ (i.e., either $p = 0$ or all irreducible factors of $p$ over $L$ have degree 1), the natural degree of $p$ equals the number of roots (counting multiplicities) of $p$ in $L$ under the extension $i$, i.e., \[ \deg p = |\text{roots}(p \circ i)|. \]

Polynomial.degree_eq_card_roots theorem

{p : K[X]} {i : K →+* L} (p_ne_zero : p ≠ 0) (hsplit : Splits i p) : p.degree = Multiset.card (p.map i).roots

Full source

theorem degree_eq_card_roots {p : K[X]} {i : K →+* L} (p_ne_zero : p ≠ 0) (hsplit : Splits i p) :
    p.degree = Multiset.card (p.map i).roots := by
  rw [degree_eq_natDegree p_ne_zero, natDegree_eq_card_roots hsplit]

Degree Equals Root Count for Nonzero Splitting Polynomials

Informal description

Let $K$ be a commutative ring and $L$ a field, with a ring homomorphism $i \colon K \to L$. For any nonzero polynomial $p \in K[X]$ that splits over $L$ via $i$ (i.e., all irreducible factors of $p$ over $L$ have degree 1), the degree of $p$ equals the number of roots (counting multiplicities) of $p$ in $L$ under the extension $i$, i.e., \[ \deg p = |\text{roots}(p \circ i)|. \]

Polynomial.roots_map theorem

{f : K[X]} (hf : f.Splits <| RingHom.id K) : (f.map i).roots = f.roots.map i

Full source

theorem roots_map {f : K[X]} (hf : f.Splits <| RingHom.id K) : (f.map i).roots = f.roots.map i :=
  (roots_map_of_injective_of_card_eq_natDegree i.injective <| by
      convert (natDegree_eq_card_roots hf).symm
      rw [map_id]).symm

Roots of Polynomial Image under Field Extension

Informal description

Let $K$ be a field and $L$ be a field extension of $K$ with a ring homomorphism $i \colon K \to L$. For any polynomial $f \in K[X]$ that splits over $K$ (i.e., either $f = 0$ or all irreducible factors of $f$ over $K$ have degree 1), the multiset of roots of $f \circ i$ in $L$ is equal to the image under $i$ of the multiset of roots of $f$ in $K$. That is, \[ \text{roots}(f \circ i) = i(\text{roots}(f)). \]

Polynomial.Splits.mem_subfield_of_isRoot theorem

 (F : Subfield K) {f : F[X]} (hnz : f ≠ 0) (hf : Splits (RingHom.id F) f) {x : K} (hx : (f.map F.subtype).IsRoot x) :
  x ∈ F

Full source

theorem Splits.mem_subfield_of_isRoot (F : Subfield K) {f : F[X]} (hnz : f ≠ 0)
    (hf : Splits (RingHom.id F) f) {x : K} (hx : (f.map F.subtype).IsRoot x) :
    x ∈ F := by
  obtain ⟨x, _, rfl⟩ := Multiset.mem_map.mp
    (roots_map F.subtype hf ▸ mem_roots'.mpr ⟨Polynomial.map_ne_zero hnz, hx⟩)
  exact x.2

Roots of Splitting Polynomials over Subfields Belong to the Subfield

Informal description

Let $K$ be a field and $F$ a subfield of $K$. For any nonzero polynomial $f \in F[X]$ that splits over $F$ (i.e., either $f = 0$ or all irreducible factors of $f$ over $F$ have degree 1), if $x \in K$ is a root of the polynomial $f$ viewed in $K$ via the inclusion map $F \hookrightarrow K$, then $x$ belongs to $F$.

Polynomial.image_rootSet theorem

 [Algebra R K] [Algebra R L] {p : R[X]} (h : p.Splits (algebraMap R K)) (f : K →ₐ[R] L) : f '' p.rootSet K = p.rootSet L

Full source

theorem image_rootSet [Algebra R K] [Algebra R L] {p : R[X]} (h : p.Splits (algebraMap R K))
    (f : K →ₐ[R] L) : f '' p.rootSet K = p.rootSet L := by
  classical
    rw [rootSet, ← Finset.coe_image, ← Multiset.toFinset_map, ← f.coe_toRingHom,
      ← roots_map _ ((splits_id_iff_splits (algebraMap R K)).mpr h), map_map, f.comp_algebraMap,
      ← rootSet]

Image of Root Set under Algebra Homomorphism Equals Target Root Set for Splitting Polynomials

Informal description

Let $R$, $K$, and $L$ be commutative rings with $K$ and $L$ being $R$-algebras. For any polynomial $p \in R[X]$ that splits over $K$ via the algebra map $R \to K$, and any $R$-algebra homomorphism $f \colon K \to L$, the image of the root set of $p$ in $K$ under $f$ equals the root set of $p$ in $L$. That is, \[ f(p.\text{rootSet}(K)) = p.\text{rootSet}(L). \]

Polynomial.adjoin_rootSet_eq_range theorem

 [Algebra R K] [Algebra R L] {p : R[X]} (h : p.Splits (algebraMap R K)) (f : K →ₐ[R] L) :
  Algebra.adjoin R (p.rootSet L) = f.range ↔ Algebra.adjoin R (p.rootSet K) = ⊤

Full source

theorem adjoin_rootSet_eq_range [Algebra R K] [Algebra R L] {p : R[X]}
    (h : p.Splits (algebraMap R K)) (f : K →ₐ[R] L) :
    Algebra.adjoinAlgebra.adjoin R (p.rootSet L) = f.range ↔ Algebra.adjoin R (p.rootSet K) = ⊤ := by
  rw [← image_rootSet h f, Algebra.adjoin_image, ← Algebra.map_top]
  exact (Subalgebra.map_injective f.toRingHom.injective).eq_iff

Equivalence of Adjoining Roots and Range of Algebra Homomorphism for Splitting Polynomials

Informal description

Let $R$, $K$, and $L$ be commutative rings with $K$ and $L$ being $R$-algebras. For a polynomial $p \in R[X]$ that splits over $K$ via the algebra map $R \to K$, and an $R$-algebra homomorphism $f \colon K \to L$, the following are equivalent: 1. The algebra generated by $R$ and the roots of $p$ in $L$ equals the range of $f$. 2. The algebra generated by $R$ and the roots of $p$ in $K$ is the entire ring $K$.

Polynomial.Splits.dvd_of_roots_le_roots theorem

{p q : K[X]} (hp : p.Splits (RingHom.id _)) (hp0 : p ≠ 0) (hq : p.roots ≤ q.roots) : p ∣ q

Full source

theorem Splits.dvd_of_roots_le_roots {p q : K[X]} (hp : p.Splits (RingHom.id _)) (hp0 : p ≠ 0)
    (hq : p.roots ≤ q.roots) : p ∣ q := by
  rw [eq_prod_roots_of_splits_id hp, C_mul_dvd (leadingCoeff_ne_zero.2 hp0)]
  exact dvd_trans
    (Multiset.prod_dvd_prod_of_le (Multiset.map_le_map hq))
    (prod_multiset_X_sub_C_dvd _)

Divisibility of Polynomials via Root Inclusion for Split Polynomials

Informal description

Let $K$ be a field and let $p, q \in K[X]$ be nonzero polynomials. If $p$ splits over $K$ (i.e., all irreducible factors of $p$ over $K$ have degree 1) and the multiset of roots of $p$ is a submultiset of the multiset of roots of $q$, then $p$ divides $q$.

Polynomial.Splits.dvd_iff_roots_le_roots theorem

{p q : K[X]} (hp : p.Splits (RingHom.id _)) (hp0 : p ≠ 0) (hq0 : q ≠ 0) : p ∣ q ↔ p.roots ≤ q.roots

Full source

theorem Splits.dvd_iff_roots_le_roots {p q : K[X]}
    (hp : p.Splits (RingHom.id _)) (hp0 : p ≠ 0) (hq0 : q ≠ 0) :
    p ∣ qp ∣ q ↔ p.roots ≤ q.roots :=
  ⟨Polynomial.roots.le_of_dvd hq0, hp.dvd_of_roots_le_roots hp0⟩

Divisibility Criterion for Split Polynomials via Root Inclusion

Informal description

Let $K$ be a field and let $p, q \in K[X]$ be nonzero polynomials such that $p$ splits over $K$ (i.e., all irreducible factors of $p$ over $K$ have degree 1). Then $p$ divides $q$ if and only if the multiset of roots of $p$ is a submultiset of the multiset of roots of $q$.

Polynomial.aeval_eq_prod_aroots_sub_of_splits theorem

 [Algebra K L] {p : K[X]} (hsplit : Splits (algebraMap K L) p) (v : L) :
  aeval v p = algebraMap K L p.leadingCoeff * ((p.aroots L).map fun a ↦ v - a).prod

Full source

theorem aeval_eq_prod_aroots_sub_of_splits [Algebra K L] {p : K[X]}
    (hsplit : Splits (algebraMap K L) p) (v : L) :
    aeval v p = algebraMap K L p.leadingCoeff * ((p.aroots L).map fun a ↦ v - a).prod := by
  rw [← eval_map_algebraMap, eq_prod_roots_of_splits hsplit]
  simp [eval_multiset_prod]

Evaluation of Split Polynomials via Roots and Leading Coefficient

Informal description

Let $K$ be a field and $L$ be a field extension of $K$ via an algebra structure $[Algebra K L]$. For any polynomial $p \in K[X]$ that splits over $L$ (i.e., all irreducible factors of $p$ over $L$ have degree 1) and any element $v \in L$, the evaluation of $p$ at $v$ via the algebra homomorphism is equal to the product of the leading coefficient of $p$ (mapped to $L$) and the product of $(v - a)$ for all roots $a$ of $p$ in $L$. That is, \[ \text{aeval}_L(v, p) = (\text{algebraMap}_{K \to L})(p.\text{leadingCoeff}) \cdot \prod_{a \in p.\text{aroots}(L)} (v - a). \]

Polynomial.eval_eq_prod_roots_sub_of_splits_id theorem

{p : K[X]} (hsplit : Splits (RingHom.id K) p) (v : K) : eval v p = p.leadingCoeff * (p.roots.map fun a ↦ v - a).prod

Full source

theorem eval_eq_prod_roots_sub_of_splits_id {p : K[X]}
    (hsplit : Splits (RingHom.id K) p) (v : K) :
    eval v p = p.leadingCoeff * (p.roots.map fun a ↦ v - a).prod := by
  convert aeval_eq_prod_aroots_sub_of_splits hsplit v
  rw [Algebra.id.map_eq_id, map_id]

Evaluation of Split Polynomials via Roots and Leading Coefficient over Base Field

Informal description

Let $K$ be a field and $p \in K[X]$ be a polynomial that splits over $K$ (i.e., all irreducible factors of $p$ over $K$ have degree 1). Then for any element $v \in K$, the evaluation of $p$ at $v$ is equal to the product of the leading coefficient of $p$ and the product of $(v - a)$ for all roots $a$ of $p$ in $K$. That is, \[ \text{eval}(v, p) = p.\text{leadingCoeff} \cdot \prod_{a \in p.\text{roots}} (v - a). \]

Polynomial.aeval_eq_prod_aroots_sub_of_monic_of_splits theorem

 [Algebra K L] {p : K[X]} (m : Monic p) (hsplit : Splits (algebraMap K L) p) (v : L) :
  aeval v p = ((p.aroots L).map fun a ↦ v - a).prod

Full source

theorem aeval_eq_prod_aroots_sub_of_monic_of_splits [Algebra K L] {p : K[X]} (m : Monic p)
    (hsplit : Splits (algebraMap K L) p) (v : L) :
    aeval v p = ((p.aroots L).map fun a ↦ v - a).prod := by
  simp [aeval_eq_prod_aroots_sub_of_splits hsplit, m]

Evaluation of Monic Split Polynomials via Roots

Informal description

Let $K$ be a field and $L$ be a field extension of $K$ via an algebra structure. For any monic polynomial $p \in K[X]$ that splits over $L$ (i.e., all irreducible factors of $p$ over $L$ have degree 1) and any element $v \in L$, the evaluation of $p$ at $v$ via the algebra homomorphism is equal to the product of $(v - a)$ for all roots $a$ of $p$ in $L$. That is, \[ \text{aeval}_L(v, p) = \prod_{a \in p.\text{aroots}(L)} (v - a). \]

Polynomial.eval_eq_prod_roots_sub_of_monic_of_splits_id theorem

{p : K[X]} (m : Monic p) (hsplit : Splits (RingHom.id K) p) (v : K) : eval v p = (p.roots.map fun a ↦ v - a).prod

Full source

theorem eval_eq_prod_roots_sub_of_monic_of_splits_id {p : K[X]} (m : Monic p)
    (hsplit : Splits (RingHom.id K) p) (v : K) :
    eval v p = (p.roots.map fun a ↦ v - a).prod := by
  simp [eval_eq_prod_roots_sub_of_splits_id hsplit, m]

Evaluation of Monic Split Polynomials via Roots over Base Field

Informal description

Let $K$ be a field and $p \in K[X]$ be a monic polynomial that splits over $K$ (i.e., all irreducible factors of $p$ over $K$ have degree 1). Then for any element $v \in K$, the evaluation of $p$ at $v$ is equal to the product of $(v - a)$ for all roots $a$ of $p$ in $K$. That is, \[ p(v) = \prod_{a \in \text{roots}(p)} (v - a). \]

Polynomial.mem_lift_of_splits_of_roots_mem_range theorem

 [Algebra R K] {f : K[X]} (hs : f.Splits (RingHom.id K)) (hm : f.Monic)
  (hr : ∀ a ∈ f.roots, a ∈ (algebraMap R K).range) : f ∈ Polynomial.lifts (algebraMap R K)

Full source

theorem mem_lift_of_splits_of_roots_mem_range [Algebra R K] {f : K[X]}
    (hs : f.Splits (RingHom.id K)) (hm : f.Monic) (hr : ∀ a ∈ f.roots, a ∈ (algebraMap R K).range) :
    f ∈ Polynomial.lifts (algebraMap R K) := by
  rw [eq_prod_roots_of_monic_of_splits_id hm hs, lifts_iff_liftsRing]
  refine Subring.multiset_prod_mem _ _ fun P hP => ?_
  obtain ⟨b, hb, rfl⟩ := Multiset.mem_map.1 hP
  exact Subring.sub_mem _ (X_mem_lifts _) (C'_mem_lifts (hr _ hb))

Liftability of Monic Splitting Polynomials with Roots in Base Ring

Informal description

Let $R$ and $K$ be commutative rings with $K$ a field extension of $R$ via an algebra map $\text{algebraMap} \colon R \to K$. For a monic polynomial $f \in K[X]$ that splits over $K$ (i.e., all irreducible factors of $f$ over $K$ have degree 1), and such that every root of $f$ lies in the range of $\text{algebraMap}$, then $f$ can be lifted to a polynomial in $R[X]$ via $\text{algebraMap}$.

Polynomial.splits_of_natDegree_eq_two theorem

{f : Polynomial K} {x : L} (h₁ : f.natDegree = 2) (h₂ : eval₂ i x f = 0) : Splits i f

Full source

/--
A polynomial of degree `2` with a root splits.
-/
theorem splits_of_natDegree_eq_two {f : Polynomial K} {x : L} (h₁ : f.natDegree = 2)
    (h₂ : eval₂ i x f = 0) : Splits i f := by
  have hf₀ : f ≠ 0 := ne_zero_of_natDegree_gt (h₁ ▸ zero_lt_two)
  have h : (mapmap i f /ₘ (X - C x)).natDegree = 1 := by
    rw [natDegree_divByMonic _ (monic_X_sub_C x), natDegree_map, h₁, natDegree_X_sub_C]
  replace h₂ := (mem_roots'.mp <| (mem_roots_map_of_injective i.injective hf₀).mpr h₂).2
  rw [← splits_id_iff_splits, ← mul_divByMonic_eq_iff_isRoot.mpr h₂]
  exact (splits_mul_iff _ (X_sub_C_ne_zero x) (by simp [ne_zero_of_natDegree_gt, h])).mpr
    ⟨splits_X_sub_C  _, splits_of_natDegree_le_one (RingHom.id L) (by rw [h])⟩

Quadratic Polynomials with Roots Split over Field Extensions

Informal description

Let $K$ be a commutative ring and $L$ a field with a ring homomorphism $i \colon K \to L$. For any polynomial $f \in K[X]$ of natural degree $2$ (i.e., $\deg f = 2$) and any element $x \in L$ such that $f(x) = 0$ (where $f(x)$ is evaluated via $i$), the polynomial $f$ splits over $L$ via $i$.

Polynomial.splits_of_degree_eq_two theorem

{f : Polynomial K} {x : L} (h₁ : f.degree = 2) (h₂ : eval₂ i x f = 0) : Splits i f

Full source

theorem splits_of_degree_eq_two {f : Polynomial K} {x : L} (h₁ : f.degree = 2)
    (h₂ : eval₂ i x f = 0) : Splits i f :=
  splits_of_natDegree_eq_two i (natDegree_eq_of_degree_eq_some h₁) h₂

Quadratic Polynomials with Roots Split over Field Extensions

Informal description

Let $K$ be a commutative ring and $L$ a field with a ring homomorphism $i \colon K \to L$. For any polynomial $f \in K[X]$ of degree $2$ and any element $x \in L$ such that $f(x) = 0$ (where $f(x)$ is evaluated via $i$), the polynomial $f$ splits over $L$ via $i$.

Polynomial.splits_of_exists_multiset theorem

{f : K[X]} {s : Multiset L} (hs : f.map i = C (i f.leadingCoeff) * (s.map fun a : L => X - C a).prod) : Splits i f

Full source

theorem splits_of_exists_multiset {f : K[X]} {s : Multiset L}
    (hs : f.map i = C (i f.leadingCoeff) * (s.map fun a : L => X - C a).prod) : Splits i f :=
  letI := Classical.decEq K
  if hf0 : f = 0 then hf0.symm ▸ splits_zero i
  else
    Or.inr @fun p hp hdp => by
      rw [irreducible_iff_prime] at hp
      rw [hs, ← Multiset.prod_toList] at hdp
      obtain hd | hd := hp.2.2 _ _ hdp
      · refine (hp.2.1 <| isUnit_of_dvd_unit hd ?_).elim
        exact isUnit_C.2 ((leadingCoeff_ne_zero.2 hf0).isUnit.map i)
      · obtain ⟨q, hq, hd⟩ := hp.dvd_prod_iff.1 hd
        obtain ⟨a, _, rfl⟩ := Multiset.mem_map.1 (Multiset.mem_toList.1 hq)
        rw [degree_eq_degree_of_associated ((hp.dvd_prime_iff_associated <| prime_X_sub_C a).1 hd)]
        exact degree_X_sub_C a

Factorization into Linear Factors Implies Splitting of Polynomial

Informal description

Let $K$ be a commutative ring and $L$ a field extension of $K$ via a ring homomorphism $i : K \to L$. For any polynomial $f \in K[X]$, if there exists a multiset $s$ of elements in $L$ such that the polynomial $f$ mapped via $i$ can be expressed as: \[ f \circ i = C(i(f.\text{leadingCoeff})) \cdot \prod_{a \in s} (X - C(a)), \] then $f$ splits over $L$ via $i$, meaning either $f$ is zero or all its irreducible factors over $L$ have degree 1.

Polynomial.splits_of_splits_id theorem

{f : K[X]} : Splits (RingHom.id K) f → Splits i f

Full source

theorem splits_of_splits_id {f : K[X]} : Splits (RingHom.id K) f → Splits i f :=
  UniqueFactorizationMonoid.induction_on_prime f (fun _ => splits_zero _)
    (fun _ hu _ => splits_of_degree_le_one _ ((isUnit_iff_degree_eq_zero.1 hu).symm ▸ by decide))
    fun _ p ha0 hp ih hfi =>
    splits_mul _
      (splits_of_degree_eq_one _
        ((splits_of_splits_mul _ (mul_ne_zero hp.1 ha0) hfi).1.def.resolve_left hp.1 hp.irreducible
          (by rw [map_id])))
      (ih (splits_of_splits_mul _ (mul_ne_zero hp.1 ha0) hfi).2)

Splitting over Base Field Implies Splitting over Extension

Informal description

Let $K$ be a field, $L$ a field extension of $K$, and $i \colon K \to L$ a ring homomorphism. For any polynomial $f \in K[X]$, if $f$ splits over $K$ via the identity homomorphism $\text{id}_K$, then $f$ splits over $L$ via $i$.

Polynomial.splits_iff_exists_multiset theorem

{f : K[X]} : Splits i f ↔ ∃ s : Multiset L, f.map i = C (i f.leadingCoeff) * (s.map fun a : L => X - C a).prod

Full source

theorem splits_iff_exists_multiset {f : K[X]} :
    SplitsSplits i f ↔
      ∃ s : Multiset L, f.map i = C (i f.leadingCoeff) * (s.map fun a : L => X - C a).prod :=
  ⟨fun hf => ⟨(f.map i).roots, eq_prod_roots_of_splits hf⟩, fun ⟨_, hs⟩ =>
    splits_of_exists_multiset i hs⟩

Characterization of Polynomial Splitting via Linear Factorization

Informal description

Let $K$ be a commutative ring, $L$ a field extension of $K$ via a ring homomorphism $i \colon K \to L$, and $f \in K[X]$ a polynomial. Then $f$ splits over $L$ via $i$ if and only if there exists a multiset $s$ of elements in $L$ such that the polynomial $f$ mapped via $i$ can be expressed as: \[ f \circ i = C(i(f.\text{leadingCoeff})) \cdot \prod_{a \in s} (X - C(a)), \] where $C$ denotes the constant polynomial embedding and $X$ is the polynomial variable.

Polynomial.splits_of_comp theorem

 (j : L →+* F) {f : K[X]} (h : Splits (j.comp i) f) (roots_mem_range : ∀ a ∈ (f.map (j.comp i)).roots, a ∈ j.range) :
  Splits i f

Full source

theorem splits_of_comp (j : L →+* F) {f : K[X]} (h : Splits (j.comp i) f)
    (roots_mem_range : ∀ a ∈ (f.map (j.comp i)).roots, a ∈ j.range) : Splits i f := by
  choose lift lift_eq using roots_mem_range
  rw [splits_iff_exists_multiset]
  refine ⟨(f.map (j.comp i)).roots.pmap lift fun _ ↦ id, map_injective _ j.injective ?_⟩
  conv_lhs => rw [Polynomial.map_map, eq_prod_roots_of_splits h]
  simp_rw [Polynomial.map_mul, Polynomial.map_multiset_prod, Multiset.map_pmap, Polynomial.map_sub,
    map_C, map_X, lift_eq, Multiset.pmap_eq_map]
  rfl

Splitting over Composition of Field Extensions Implies Splitting over Intermediate Extension

Informal description

Let $K$ be a commutative ring, $L$ and $F$ be field extensions of $K$ via ring homomorphisms $i \colon K \to L$ and $j \colon L \to F$. For any polynomial $f \in K[X]$, if $f$ splits over $F$ via the composition $j \circ i$ and every root of $f$ under this composition lies in the image of $j$, then $f$ splits over $L$ via $i$.

Polynomial.splits_id_of_splits theorem

{f : K[X]} (h : Splits i f) (roots_mem_range : ∀ a ∈ (f.map i).roots, a ∈ i.range) : Splits (RingHom.id K) f

Full source

theorem splits_id_of_splits {f : K[X]} (h : Splits i f)
    (roots_mem_range : ∀ a ∈ (f.map i).roots, a ∈ i.range) : Splits (RingHom.id K) f :=
  splits_of_comp (RingHom.id K) i h roots_mem_range

Splitting over Field Extension Implies Splitting over Base Field via Identity

Informal description

Let $K$ be a commutative ring, $L$ a field extension of $K$ via a ring homomorphism $i \colon K \to L$, and $f \in K[X]$ a polynomial. If $f$ splits over $L$ via $i$ and every root of $f$ under this extension lies in the image of $i$, then $f$ splits over $K$ via the identity homomorphism $\text{id}_K$.

Polynomial.splits_comp_of_splits theorem

(i : R →+* K) (j : K →+* L) {f : R[X]} (h : Splits i f) : Splits (j.comp i) f

Full source

theorem splits_comp_of_splits (i : R →+* K) (j : K →+* L) {f : R[X]} (h : Splits i f) :
    Splits (j.comp i) f :=
  (splits_map_iff i j).mp (splits_of_splits_id _ <| (splits_map_iff i <| .id K).mpr h)

Splitting Preservation under Composition of Field Homomorphisms

Informal description

Let $R$, $K$, and $L$ be commutative rings with $K$ and $L$ being fields. Given ring homomorphisms $i \colon R \to K$ and $j \colon K \to L$, and a polynomial $f \in R[X]$, if $f$ splits over $K$ via $i$, then $f$ splits over $L$ via the composition $j \circ i$.

Polynomial.splits_of_algHom theorem

{f : R[X]} (h : Splits (algebraMap R K) f) (e : K →ₐ[R] L) : Splits (algebraMap R L) f

Full source

theorem splits_of_algHom {f : R[X]} (h : Splits (algebraMap R K) f) (e : K →ₐ[R] L) :
    Splits (algebraMap R L) f := by
  rw [← e.comp_algebraMap_of_tower R]; exact splits_comp_of_splits _ _ h

Splitting Preservation under Algebra Homomorphisms

Informal description

Let $R$, $K$, and $L$ be commutative rings with $K$ and $L$ being fields, and let $f \in R[X]$ be a polynomial. If $f$ splits over $K$ via the algebra map $\text{algebraMap} \colon R \to K$, then for any $R$-algebra homomorphism $e \colon K \to L$, the polynomial $f$ also splits over $L$ via the algebra map $\text{algebraMap} \colon R \to L$.

Polynomial.splits_of_isScalarTower theorem

{f : R[X]} [Algebra K L] [IsScalarTower R K L] (h : Splits (algebraMap R K) f) : Splits (algebraMap R L) f

Full source

theorem splits_of_isScalarTower {f : R[X]} [Algebra K L] [IsScalarTower R K L]
    (h : Splits (algebraMap R K) f) : Splits (algebraMap R L) f :=
  splits_of_algHom h (IsScalarTower.toAlgHom R K L)

Splitting Preservation under Scalar Multiplication Tower Condition

Informal description

Let $R$, $K$, and $L$ be commutative rings with $K$ and $L$ fields, and let $f \in R[X]$ be a polynomial. Suppose there is an algebra structure $K \to L$ such that the scalar multiplication tower property holds for $R$, $K$, and $L$. If $f$ splits over $K$ via the algebra map $R \to K$, then $f$ also splits over $L$ via the algebra map $R \to L$.

Polynomial.splits_iff_card_roots theorem

{p : K[X]} : Splits (RingHom.id K) p ↔ Multiset.card p.roots = p.natDegree

Full source

/-- A polynomial splits if and only if it has as many roots as its degree. -/
theorem splits_iff_card_roots {p : K[X]} :
    SplitsSplits (RingHom.id K) p ↔ Multiset.card p.roots = p.natDegree := by
  constructor
  · intro H
    rw [natDegree_eq_card_roots H, map_id]
  · intro hroots
    rw [splits_iff_exists_multiset (RingHom.id K)]
    use p.roots
    simp only [RingHom.id_apply, map_id]
    exact (C_leadingCoeff_mul_prod_multiset_X_sub_C hroots).symm

Splitting Criterion: $\text{Splits}(p) \leftrightarrow |\text{roots}(p)| = \deg p$

Informal description

Let $K$ be a field and $p \in K[X]$ a polynomial. Then $p$ splits over $K$ (i.e., either $p = 0$ or all irreducible factors of $p$ over $K$ have degree 1) if and only if the number of roots of $p$ in $K$ (counting multiplicities) equals the degree of $p$.

Polynomial.aeval_root_derivative_of_splits theorem

 [Algebra K L] [DecidableEq L] {P : K[X]} (hmo : P.Monic) (hP : P.Splits (algebraMap K L)) {r : L}
  (hr : r ∈ P.aroots L) : aeval r (Polynomial.derivative P) = (((P.aroots L).erase r).map fun a => r - a).prod

Full source

theorem aeval_root_derivative_of_splits [Algebra K L] [DecidableEq L] {P : K[X]} (hmo : P.Monic)
    (hP : P.Splits (algebraMap K L)) {r : L} (hr : r ∈ P.aroots L) :
    aeval r (Polynomial.derivative P) =
    (((P.aroots L).erase r).map fun a => r - a).prod := by
  replace hmo := hmo.map (algebraMap K L)
  replace hP := (splits_id_iff_splits (algebraMap K L)).2 hP
  rw [aeval_def, ← eval_map, ← derivative_map]
  nth_rw 1 [eq_prod_roots_of_monic_of_splits_id hmo hP]
  rw [eval_multiset_prod_X_sub_C_derivative hr]

Evaluation of Derivative at Root Equals Product of Root Differences for Splitting Polynomials

Informal description

Let $K$ and $L$ be fields with $L$ an algebra over $K$, and let $P \in K[X]$ be a monic polynomial that splits over $L$ via the algebra map $K \to L$. For any root $r \in L$ of $P$, the evaluation of the derivative $P'$ at $r$ equals the product of $(r - a)$ for all other roots $a$ of $P$ in $L$ (counted with multiplicity).

Polynomial.prod_roots_eq_coeff_zero_of_monic_of_splits theorem

{P : K[X]} (hmo : P.Monic) (hP : P.Splits (RingHom.id K)) : coeff P 0 = (-1) ^ P.natDegree * P.roots.prod

Full source

/-- If `P` is a monic polynomial that splits, then `coeff P 0` equals the product of the roots. -/
theorem prod_roots_eq_coeff_zero_of_monic_of_splits {P : K[X]} (hmo : P.Monic)
    (hP : P.Splits (RingHom.id K)) : coeff P 0 = (-1) ^ P.natDegree * P.roots.prod := by
  nth_rw 1 [eq_prod_roots_of_monic_of_splits_id hmo hP]
  rw [coeff_zero_eq_eval_zero, eval_multiset_prod, Multiset.map_map]
  simp_rw [Function.comp_apply, eval_sub, eval_X, zero_sub, eval_C]
  conv_lhs =>
    congr
    congr
    ext
    rw [neg_eq_neg_one_mul]
  simp only [splits_iff_card_roots.1 hP, neg_mul, one_mul, Multiset.prod_map_neg]

Constant Term of Splitting Monic Polynomial Equals Signed Product of Roots: $P(0) = (-1)^{\deg P} \prod r$

Informal description

Let $P \in K[X]$ be a monic polynomial that splits over $K$ (i.e., either $P = 0$ or all irreducible factors of $P$ over $K$ have degree 1). Then the constant term of $P$ is equal to $(-1)^{\deg P}$ times the product of the roots of $P$ (counted with multiplicity), i.e., \[ P(0) = (-1)^{\deg P} \prod_{r \in \text{roots}(P)} r. \]

Polynomial.sum_roots_eq_nextCoeff_of_monic_of_split theorem

{P : K[X]} (hmo : P.Monic) (hP : P.Splits (RingHom.id K)) : P.nextCoeff = -P.roots.sum

Full source

/-- If `P` is a monic polynomial that splits, then `P.nextCoeff` equals the sum of the roots. -/
theorem sum_roots_eq_nextCoeff_of_monic_of_split {P : K[X]} (hmo : P.Monic)
    (hP : P.Splits (RingHom.id K)) : P.nextCoeff = -P.roots.sum := by
  nth_rw 1 [eq_prod_roots_of_monic_of_splits_id hmo hP]
  rw [Monic.nextCoeff_multiset_prod _ _ fun a ha => _]
  · simp_rw [nextCoeff_X_sub_C, Multiset.sum_map_neg']
  · simp only [monic_X_sub_C, implies_true]

Next Coefficient Equals Negative Sum of Roots for Splitting Monic Polynomials

Informal description

Let $P \in K[X]$ be a monic polynomial that splits over $K$ (i.e., all its irreducible factors over $K$ have degree 1). Then the next coefficient of $P$ is equal to the negative of the sum of its roots, i.e., \[ \text{nextCoeff}(P) = -\sum_{r \in \text{roots}(P)} r. \]

Main definitions