Roots, splitting and divisibility of X ^ n - C a

For n ≠ 0, membership in the root set of X ^ n - C a is the equation x ^ n = a in any domain algebra. For n = 2, a single square root δ of a splits the binomial over any commutative ring: its linear factors have roots δ and -δ. No primitive root of unity is needed, so the splitting statement also applies in characteristic 2. Over an ordered field, X ^ 2 + 1 = X ^ 2 - C (-1) is irreducible since -1 is not a square. Over any nontrivial ring, the monic X ^ n - C a of degree n does not divide the geometric sum 1 + X + ⋯ + X ^ (n - 1), which is monic of degree n - 1.

Main results

• Polynomial.mem_rootSet_X_pow_sub_C: root-set membership is an n-th power equation.
• Polynomial.splits_map_X_pow_two_sub_C: a square root splits the quadratic binomial.
• Polynomial.map_X_pow_sub_C_eq_X_sub_C_pow: in exponential characteristic p, a p-th root δ of a makes X ^ p - C a the p-th power (X - C δ) ^ p.
• Polynomial.irreducible_X_sq_add_one: X ^ 2 + 1 is irreducible over an ordered field.
• Polynomial.not_X_pow_sub_C_dvd_geom_sum: X ^ n - C a does not divide 1 + X + ⋯ + X ^ (n - 1).

@[simp]

theorem Polynomial.mem_rootSet_X_pow_sub_C {F : Type u} [CommRing F] {E : Type v} [CommRing E] [IsDomain E] [Algebra F E] {a : F} {n : ℕ} (hn : n ≠ 0) {x : E} : x ∈ (X ^ n - C a).rootSet E ↔ x ^ n = (algebraMap F E) a

An element of a domain algebra is a root of X ^ n - C a exactly when its n-th power is a.

theorem Polynomial.splits_map_X_pow_two_sub_C {F : Type u} [CommRing F] {E : Type v} [CommRing E] [Algebra F E] {a : F} {δ : E} (hδ : δ ^ 2 = (algebraMap F E) a) : (map (algebraMap F E) (X ^ 2 - C a)).Splits

A square root of a in E splits X ^ 2 - C a there: the two linear factors are X - C δ and X + C δ. Unlike Polynomial.X_pow_sub_C_splits_of_isPrimitiveRoot this needs no primitive root of unity, so it also covers characteristic 2, where the two factors coincide.

theorem Polynomial.map_X_pow_sub_C_eq_X_sub_C_pow {F : Type u} [CommRing F] {E : Type v} [CommRing E] [Algebra F E] {a : F} {δ : E} (p : ℕ) [ExpChar E p] (hδ : δ ^ p = (algebraMap F E) a) : map (algebraMap F E) (X ^ p - C a) = (X - C δ) ^ p

In exponential characteristic p, a p-th root δ of a in E makes X ^ p - C a a p-th power there: its image in E[X] is (X - C δ) ^ p.

theorem Polynomial.irreducible_X_sq_add_one (K : Type u_1) [Field K] [LinearOrder K] [IsStrictOrderedRing K] : Irreducible (X ^ 2 + 1)

X ^ 2 + 1 is irreducible over an ordered field: a square is never -1.

theorem Polynomial.not_X_pow_sub_C_dvd_geom_sum {R : Type u} [Ring R] [Nontrivial R] (a : R) {n : ℕ} (hn : n ≠ 0) : ¬X ^ n - C a ∣ ∑ k ∈ Finset.range n, X ^ k

For n ≠ 0, X ^ n - C a does not divide 1 + X + ⋯ + X ^ (n - 1), which is nonzero of degree less than n.