Split polynomials

A polynomial f : K[X] splits over a field extension L of K if it is zero or all of its irreducible factors over L have degree 1.

Main definitions

• Polynomial.Splits i f: A predicate on a homomorphism i : K →+* L from a commutative ring to a field and a polynomial f saying that f.map i is zero or all of its irreducible factors over L have degree 1.

Main statements

• lift_of_splits: If K and L are field extensions of a field F and for some finite subset S of K, the minimal polynomial of every x ∈ K splits as a polynomial with coefficients in L, then Algebra.adjoin F S embeds into L.

def Polynomial.Splits {K : Type v} {L : Type w} [CommRing K] [Field L] (i : K →+* L) (f : Polynomial K) : Prop

A polynomial Splits iff it is zero or all of its irreducible factors have degree 1.

Equations

• Polynomial.Splits i f = (Polynomial.map i f = 0 ∨ ∀ {g : Polynomial L}, Irreducible g → g ∣ Polynomial.map i f → Polynomial.degree g = 1)

@[simp]

theorem Polynomial.splits_zero {K : Type v} {L : Type w} [CommRing K] [Field L] (i : K →+* L) : Polynomial.Splits i 0

theorem Polynomial.splits_of_map_eq_C {K : Type v} {L : Type w} [CommRing K] [Field L] (i : K →+* L) {f : Polynomial K} {a : L} (h : Polynomial.map i f = ↑Polynomial.C a) : Polynomial.Splits i f

@[simp]

theorem Polynomial.splits_C {K : Type v} {L : Type w} [CommRing K] [Field L] (i : K →+* L) (a : K) : Polynomial.Splits i (↑Polynomial.C a)

theorem Polynomial.splits_of_map_degree_eq_one {K : Type v} {L : Type w} [CommRing K] [Field L] (i : K →+* L) {f : Polynomial K} (hf : Polynomial.degree (Polynomial.map i f) = 1) : Polynomial.Splits i f

theorem Polynomial.splits_of_degree_le_one {K : Type v} {L : Type w} [CommRing K] [Field L] (i : K →+* L) {f : Polynomial K} (hf : Polynomial.degree f ≤ 1) : Polynomial.Splits i f

theorem Polynomial.splits_of_degree_eq_one {K : Type v} {L : Type w} [CommRing K] [Field L] (i : K →+* L) {f : Polynomial K} (hf : Polynomial.degree f = 1) : Polynomial.Splits i f

theorem Polynomial.splits_of_natDegree_le_one {K : Type v} {L : Type w} [CommRing K] [Field L] (i : K →+* L) {f : Polynomial K} (hf : Polynomial.natDegree f ≤ 1) : Polynomial.Splits i f

theorem Polynomial.splits_of_natDegree_eq_one {K : Type v} {L : Type w} [CommRing K] [Field L] (i : K →+* L) {f : Polynomial K} (hf : Polynomial.natDegree f = 1) : Polynomial.Splits i f

theorem Polynomial.splits_mul {K : Type v} {L : Type w} [CommRing K] [Field L] (i : K →+* L) {f : Polynomial K} {g : Polynomial K} (hf : Polynomial.Splits i f) (hg : Polynomial.Splits i g) : Polynomial.Splits i (f * g)

theorem Polynomial.splits_of_splits_mul' {K : Type v} {L : Type w} [CommRing K] [Field L] (i : K →+* L) {f : Polynomial K} {g : Polynomial K} (hfg : Polynomial.map i (f * g) ≠ 0) (h : Polynomial.Splits i (f * g)) : Polynomial.Splits i f ∧ Polynomial.Splits i g

theorem Polynomial.splits_map_iff {F : Type u} {K : Type v} {L : Type w} [CommRing K] [Field L] [Field F] (i : K →+* L) (j : L →+* F) {f : Polynomial K} : Polynomial.Splits j (Polynomial.map i f) ↔ Polynomial.Splits (RingHom.comp j i) f

theorem Polynomial.splits_one {K : Type v} {L : Type w} [CommRing K] [Field L] (i : K →+* L) : Polynomial.Splits i 1

theorem Polynomial.splits_of_isUnit {K : Type v} {L : Type w} [CommRing K] [Field L] (i : K →+* L) [IsDomain K] {u : Polynomial K} (hu : IsUnit u) : Polynomial.Splits i u

theorem Polynomial.splits_X_sub_C {K : Type v} {L : Type w} [CommRing K] [Field L] (i : K →+* L) {x : K} : Polynomial.Splits i (Polynomial.X - ↑Polynomial.C x)

theorem Polynomial.splits_X {K : Type v} {L : Type w} [CommRing K] [Field L] (i : K →+* L) : Polynomial.Splits i Polynomial.X

theorem Polynomial.splits_prod {K : Type v} {L : Type w} [CommRing K] [Field L] (i : K →+* L) {ι : Type u} {s : ι → Polynomial K} {t : Finset ι} : (∀ (j : ι), j ∈ t → Polynomial.Splits i (s j)) → Polynomial.Splits i (Finset.prod t fun x => s x)

theorem Polynomial.splits_pow {K : Type v} {L : Type w} [CommRing K] [Field L] (i : K →+* L) {f : Polynomial K} (hf : Polynomial.Splits i f) (n : ℕ) : Polynomial.Splits i (f ^ n)

theorem Polynomial.splits_X_pow {K : Type v} {L : Type w} [CommRing K] [Field L] (i : K →+* L) (n : ℕ) : Polynomial.Splits i (Polynomial.X ^ n)

theorem Polynomial.splits_id_iff_splits {K : Type v} {L : Type w} [CommRing K] [Field L] (i : K →+* L) {f : Polynomial K} : Polynomial.Splits (RingHom.id L) (Polynomial.map i f) ↔ Polynomial.Splits i f

theorem Polynomial.exists_root_of_splits' {K : Type v} {L : Type w} [CommRing K] [Field L] (i : K →+* L) {f : Polynomial K} (hs : Polynomial.Splits i f) (hf0 : Polynomial.degree (Polynomial.map i f) ≠ 0) : ∃ x, Polynomial.eval₂ i x f = 0

theorem Polynomial.roots_ne_zero_of_splits' {K : Type v} {L : Type w} [CommRing K] [Field L] (i : K →+* L) {f : Polynomial K} (hs : Polynomial.Splits i f) (hf0 : Polynomial.natDegree (Polynomial.map i f) ≠ 0) : Polynomial.roots (Polynomial.map i f) ≠ 0

def Polynomial.rootOfSplits' {K : Type v} {L : Type w} [CommRing K] [Field L] (i : K →+* L) {f : Polynomial K} (hf : Polynomial.Splits i f) (hfd : Polynomial.degree (Polynomial.map i f) ≠ 0) : L

Pick a root of a polynomial that splits. See rootOfSplits for polynomials over a field which has simpler assumptions.

Equations

• Polynomial.rootOfSplits' i hf hfd = Classical.choose (_ : ∃ x, Polynomial.eval₂ i x f = 0)

theorem Polynomial.map_rootOfSplits' {K : Type v} {L : Type w} [CommRing K] [Field L] (i : K →+* L) {f : Polynomial K} (hf : Polynomial.Splits i f) (hfd : Polynomial.degree (Polynomial.map i f) ≠ 0) : Polynomial.eval₂ i (Polynomial.rootOfSplits' i hf hfd) f = 0

theorem Polynomial.natDegree_eq_card_roots' {K : Type v} {L : Type w} [CommRing K] [Field L] {p : Polynomial K} {i : K →+* L} (hsplit : Polynomial.Splits i p) : Polynomial.natDegree (Polynomial.map i p) = ↑Multiset.card (Polynomial.roots (Polynomial.map i p))

theorem Polynomial.degree_eq_card_roots' {K : Type v} {L : Type w} [CommRing K] [Field L] {p : Polynomial K} {i : K →+* L} (p_ne_zero : Polynomial.map i p ≠ 0) (hsplit : Polynomial.Splits i p) : Polynomial.degree (Polynomial.map i p) = ↑(↑Multiset.card (Polynomial.roots (Polynomial.map i p)))

theorem Polynomial.splits_iff {K : Type v} {L : Type w} [Field K] [Field L] (i : K →+* L) (f : Polynomial K) : Polynomial.Splits i f ↔ f = 0 ∨ ∀ {g : Polynomial L}, Irreducible g → g ∣ Polynomial.map i f → Polynomial.degree g = 1

This lemma is for polynomials over a field.

theorem Polynomial.Splits.def {K : Type v} {L : Type w} [Field K] [Field L] {i : K →+* L} {f : Polynomial K} (h : Polynomial.Splits i f) : f = 0 ∨ ∀ {g : Polynomial L}, Irreducible g → g ∣ Polynomial.map i f → Polynomial.degree g = 1

This lemma is for polynomials over a field.

theorem Polynomial.splits_of_splits_mul {K : Type v} {L : Type w} [Field K] [Field L] (i : K →+* L) {f : Polynomial K} {g : Polynomial K} (hfg : f * g ≠ 0) (h : Polynomial.Splits i (f * g)) : Polynomial.Splits i f ∧ Polynomial.Splits i g

theorem Polynomial.splits_of_splits_of_dvd {K : Type v} {L : Type w} [Field K] [Field L] (i : K →+* L) {f : Polynomial K} {g : Polynomial K} (hf0 : f ≠ 0) (hf : Polynomial.Splits i f) (hgf : g ∣ f) : Polynomial.Splits i g

theorem Polynomial.splits_of_splits_gcd_left {K : Type v} {L : Type w} [Field K] [Field L] (i : K →+* L) {f : Polynomial K} {g : Polynomial K} (hf0 : f ≠ 0) (hf : Polynomial.Splits i f) : Polynomial.Splits i (EuclideanDomain.gcd f g)

theorem Polynomial.splits_of_splits_gcd_right {K : Type v} {L : Type w} [Field K] [Field L] (i : K →+* L) {f : Polynomial K} {g : Polynomial K} (hg0 : g ≠ 0) (hg : Polynomial.Splits i g) : Polynomial.Splits i (EuclideanDomain.gcd f g)

theorem Polynomial.splits_mul_iff {K : Type v} {L : Type w} [Field K] [Field L] (i : K →+* L) {f : Polynomial K} {g : Polynomial K} (hf : f ≠ 0) (hg : g ≠ 0) : Polynomial.Splits i (f * g) ↔ Polynomial.Splits i f ∧ Polynomial.Splits i g

theorem Polynomial.splits_prod_iff {K : Type v} {L : Type w} [Field K] [Field L] (i : K →+* L) {ι : Type u} {s : ι → Polynomial K} {t : Finset ι} : (∀ (j : ι), j ∈ t → s j ≠ 0) → (Polynomial.Splits i (Finset.prod t fun x => s x) ↔ ∀ (j : ι), j ∈ t → Polynomial.Splits i (s j))

theorem Polynomial.degree_eq_one_of_irreducible_of_splits {K : Type v} [Field K] {p : Polynomial K} (hp : Irreducible p) (hp_splits : Polynomial.Splits (RingHom.id K) p) : Polynomial.degree p = 1

theorem Polynomial.exists_root_of_splits {K : Type v} {L : Type w} [Field K] [Field L] (i : K →+* L) {f : Polynomial K} (hs : Polynomial.Splits i f) (hf0 : Polynomial.degree f ≠ 0) : ∃ x, Polynomial.eval₂ i x f = 0

theorem Polynomial.roots_ne_zero_of_splits {K : Type v} {L : Type w} [Field K] [Field L] (i : K →+* L) {f : Polynomial K} (hs : Polynomial.Splits i f) (hf0 : Polynomial.natDegree f ≠ 0) : Polynomial.roots (Polynomial.map i f) ≠ 0

def Polynomial.rootOfSplits {K : Type v} {L : Type w} [Field K] [Field L] (i : K →+* L) {f : Polynomial K} (hf : Polynomial.Splits i f) (hfd : Polynomial.degree f ≠ 0) : L

Pick a root of a polynomial that splits. This version is for polynomials over a field and has simpler assumptions.

Equations

• Polynomial.rootOfSplits i hf hfd = Polynomial.rootOfSplits' i hf (_ : Polynomial.degree (Polynomial.map i f) ≠ 0)

theorem Polynomial.rootOfSplits'_eq_rootOfSplits {K : Type v} {L : Type w} [Field K] [Field L] (i : K →+* L) {f : Polynomial K} (hf : Polynomial.Splits i f) (hfd : Polynomial.degree (Polynomial.map i f) ≠ 0) : Polynomial.rootOfSplits' i hf hfd = Polynomial.rootOfSplits i hf (_ : Polynomial.degree f ≠ 0)

rootOfSplits' is definitionally equal to rootOfSplits.

theorem Polynomial.map_rootOfSplits {K : Type v} {L : Type w} [Field K] [Field L] (i : K →+* L) {f : Polynomial K} (hf : Polynomial.Splits i f) (hfd : Polynomial.degree f ≠ 0) : Polynomial.eval₂ i (Polynomial.rootOfSplits i hf hfd) f = 0

theorem Polynomial.natDegree_eq_card_roots {K : Type v} {L : Type w} [Field K] [Field L] {p : Polynomial K} {i : K →+* L} (hsplit : Polynomial.Splits i p) : Polynomial.natDegree p = ↑Multiset.card (Polynomial.roots (Polynomial.map i p))

theorem Polynomial.degree_eq_card_roots {K : Type v} {L : Type w} [Field K] [Field L] {p : Polynomial K} {i : K →+* L} (p_ne_zero : p ≠ 0) (hsplit : Polynomial.Splits i p) : Polynomial.degree p = ↑(↑Multiset.card (Polynomial.roots (Polynomial.map i p)))

theorem Polynomial.roots_map {K : Type v} {L : Type w} [Field K] [Field L] (i : K →+* L) {f : Polynomial K} (hf : Polynomial.Splits (RingHom.id K) f) : Polynomial.roots (Polynomial.map i f) = Multiset.map (↑i) (Polynomial.roots f)

theorem Polynomial.image_rootSet {F : Type u} {K : Type v} {L : Type w} [Field K] [Field L] [Field F] [Algebra F K] [Algebra F L] {p : Polynomial F} (h : Polynomial.Splits (algebraMap F K) p) (f : K →ₐ[F] L) : ↑f '' Polynomial.rootSet p K = Polynomial.rootSet p L

theorem Polynomial.adjoin_rootSet_eq_range {F : Type u} {K : Type v} {L : Type w} [Field K] [Field L] [Field F] [Algebra F K] [Algebra F L] {p : Polynomial F} (h : Polynomial.Splits (algebraMap F K) p) (f : K →ₐ[F] L) : Algebra.adjoin F (Polynomial.rootSet p L) = AlgHom.range f ↔ Algebra.adjoin F (Polynomial.rootSet p K) = ⊤

theorem Polynomial.eq_prod_roots_of_splits {K : Type v} {L : Type w} [Field K] [Field L] {p : Polynomial K} {i : K →+* L} (hsplit : Polynomial.Splits i p) : Polynomial.map i p = ↑Polynomial.C (↑i (Polynomial.leadingCoeff p)) * Multiset.prod (Multiset.map (fun a => Polynomial.X - ↑Polynomial.C a) (Polynomial.roots (Polynomial.map i p)))

theorem Polynomial.eq_prod_roots_of_splits_id {K : Type v} [Field K] {p : Polynomial K} (hsplit : Polynomial.Splits (RingHom.id K) p) : p = ↑Polynomial.C (Polynomial.leadingCoeff p) * Multiset.prod (Multiset.map (fun a => Polynomial.X - ↑Polynomial.C a) (Polynomial.roots p))

theorem Polynomial.eq_prod_roots_of_monic_of_splits_id {K : Type v} [Field K] {p : Polynomial K} (m : Polynomial.Monic p) (hsplit : Polynomial.Splits (RingHom.id K) p) : p = Multiset.prod (Multiset.map (fun a => Polynomial.X - ↑Polynomial.C a) (Polynomial.roots p))

theorem Polynomial.eq_X_sub_C_of_splits_of_single_root {K : Type v} {L : Type w} [Field K] [Field L] (i : K →+* L) {x : K} {h : Polynomial K} (h_splits : Polynomial.Splits i h) (h_roots : Polynomial.roots (Polynomial.map i h) = {↑i x}) : h = ↑Polynomial.C (Polynomial.leadingCoeff h) * (Polynomial.X - ↑Polynomial.C x)

theorem Polynomial.mem_lift_of_splits_of_roots_mem_range {K : Type v} [Field K] (R : Type u_1) [CommRing R] [Algebra R K] {f : Polynomial K} (hs : Polynomial.Splits (RingHom.id K) f) (hm : Polynomial.Monic f) (hr : ∀ (a : K), a ∈ Polynomial.roots f → a ∈ RingHom.range (algebraMap R K)) : f ∈ Polynomial.lifts (algebraMap R K)

theorem Polynomial.splits_of_exists_multiset {K : Type v} {L : Type w} [Field K] [Field L] (i : K →+* L) {f : Polynomial K} {s : Multiset L} (hs : Polynomial.map i f = ↑Polynomial.C (↑i (Polynomial.leadingCoeff f)) * Multiset.prod (Multiset.map (fun a => Polynomial.X - ↑Polynomial.C a) s)) : Polynomial.Splits i f

theorem Polynomial.splits_of_splits_id {K : Type v} {L : Type w} [Field K] [Field L] (i : K →+* L) {f : Polynomial K} : Polynomial.Splits (RingHom.id K) f → Polynomial.Splits i f

theorem Polynomial.splits_iff_exists_multiset {K : Type v} {L : Type w} [Field K] [Field L] (i : K →+* L) {f : Polynomial K} : Polynomial.Splits i f ↔ ∃ s, Polynomial.map i f = ↑Polynomial.C (↑i (Polynomial.leadingCoeff f)) * Multiset.prod (Multiset.map (fun a => Polynomial.X - ↑Polynomial.C a) s)

theorem Polynomial.splits_comp_of_splits {F : Type u} {K : Type v} {L : Type w} [Field K] [Field L] [Field F] (i : K →+* L) (j : L →+* F) {f : Polynomial K} (h : Polynomial.Splits i f) : Polynomial.Splits (RingHom.comp j i) f

theorem Polynomial.splits_iff_card_roots {K : Type v} [Field K] {p : Polynomial K} : Polynomial.Splits (RingHom.id K) p ↔ ↑Multiset.card (Polynomial.roots p) = Polynomial.natDegree p

A polynomial splits if and only if it has as many roots as its degree.

theorem Polynomial.aeval_root_derivative_of_splits {K : Type v} {L : Type w} [Field K] [Field L] [Algebra K L] {P : Polynomial K} (hmo : Polynomial.Monic P) (hP : Polynomial.Splits (algebraMap K L) P) {r : L} (hr : r ∈ Polynomial.aroots P L) : ↑(Polynomial.aeval r) (↑Polynomial.derivative P) = Multiset.prod (Multiset.map (fun a => r - a) (Multiset.erase (Polynomial.aroots P L) r))

theorem Polynomial.prod_roots_eq_coeff_zero_of_monic_of_split {K : Type v} [Field K] {P : Polynomial K} (hmo : Polynomial.Monic P) (hP : Polynomial.Splits (RingHom.id K) P) : Polynomial.coeff P 0 = (-1) ^ Polynomial.natDegree P * Multiset.prod (Polynomial.roots P)

If P is a monic polynomial that splits, then coeff P 0 equals the product of the roots.

theorem Polynomial.sum_roots_eq_nextCoeff_of_monic_of_split {K : Type v} [Field K] {P : Polynomial K} (hmo : Polynomial.Monic P) (hP : Polynomial.Splits (RingHom.id K) P) : Polynomial.nextCoeff P = -Multiset.sum (Polynomial.roots P)

If P is a monic polynomial that splits, then P.nextCoeff equals the sum of the roots.