Casas-Alvero Conjecture

Reference:

• The Casas-Alvero conjecture for infinitely many degrees
• MathOverflow

The Casas-Alvero conjecture states that if a univariate polynomial P of degree d over a field of characteristic zero shares a non-trivial factor with its Hasse derivatives up to order d-1, then P must be of the form (X - α)ᵈ for some α in the field.

The conjecture has been proven for:

• Degrees d ≤ 8
• Degrees of the form p^k where p is prime
• Degrees of the form 2p^k where p is prime

The conjecture is false in positive characteristic p for polynomials of degree p+1.

The conjecture is now claimed to be proven in this paper:

• Proof of the Casas-Alvero conjecture: Soham Ghosh)

def CasasAlvero.HasCasasAlveroProp {K : Type u_1} [Field K] (P : Polynomial K) : Prop

A polynomial P satisfies the Casas-Alvero property if it shares a factor with each of its Hasse derivatives up to order d-1, where d is the degree of P.

Equations

• CasasAlvero.HasCasasAlveroProp P = ∀ i ∈ Finset.range P.natDegree, ¬IsCoprime P ((Polynomial.hasseDeriv i) P)

def CasasAlvero.HasCasasAlveroPropᵣ {K : Type u_1} [Field K] (P : Polynomial K) : Prop

A stronger version of the Casas-Alvero property, which requires that the polynomial P shares a root with each of its Hasse derivatives up to order deg P - 1. The subscript r indicates "root" in the definition.

Equations

• CasasAlvero.HasCasasAlveroPropᵣ P = ∀ i ∈ Finset.range P.natDegree, ∃ (α : K), P.IsRoot α ∧ ((Polynomial.hasseDeriv i) P).IsRoot α

theorem CasasAlvero.HasCasasAlveroPropᵣ.hasCasasAlveroProp {K : Type u_1} [Field K] {P : Polynomial K} (hca : HasCasasAlveroPropᵣ P) : HasCasasAlveroProp P

theorem CasasAlvero.HasCasasAlveroProp.map_iff {K : Type u_1} {L : Type u_2} [Field K] [Field L] {f : K →+* L} {P : Polynomial K} : HasCasasAlveroProp (Polynomial.map f P) ↔ HasCasasAlveroProp P

theorem CasasAlvero.hasCasasAlveroProp_iffᵣ {K : Type u_1} [Field K] {P : Polynomial K} [IsAlgClosed K] : HasCasasAlveroProp P ↔ HasCasasAlveroPropᵣ P

theorem CasasAlvero.casas_alvero_iffᵣ : (∀ {K : Type u} [inst : Field K] [CharZero K] (P : Polynomial K), P.Monic → HasCasasAlveroProp P → ∃ (α : K), P = (Polynomial.X - Polynomial.C α) ^ P.natDegree) ↔ ∀ {K : Type u} [inst : Field K] [CharZero K] (P : Polynomial K), P.Monic → HasCasasAlveroPropᵣ P → ∃ (α : K), P = (Polynomial.X - Polynomial.C α) ^ P.natDegree

Note that whether we use HasCasasAlveroProp or HasCasasAlveroPropᵣ to state the Casas-Alvero conjecture, we obtain the following equivalent statements.

theorem CasasAlvero.casas_alvero_conjecture {K : Type u_1} [Field K] [CharZero K] (P : Polynomial K) (hP : P.Monic) (hP' : HasCasasAlveroProp P) : ∃ (α : K), P = (Polynomial.X - Polynomial.C α) ^ P.natDegree

The Casas-Alvero conjecture states that in characteristic zero, if a monic polynomial P has the Casas-Alvero property, then P = (X - α)ᵈ for some α.

theorem CasasAlvero.casas_alvero.prime_power {K : Type u_1} [Field K] [CharZero K] (P : Polynomial K) (hP : P.Monic) (p k : ℕ) (hp : Nat.Prime p) (hd : P.natDegree = p ^ k) (hP' : HasCasasAlveroProp P) : ∃ (α : K), P = (Polynomial.X - Polynomial.C α) ^ P.natDegree

The Casas-Alvero conjecture holds for polynomials of prime power degree. This was proved by Graf von Bothmer, Labs, Schicho, and van de Woestijne.

Reference: The Casas-Alvero conjecture for infinitely many degrees

theorem CasasAlvero.casas_alvero.double_prime_power {K : Type u_1} [Field K] [CharZero K] (P : Polynomial K) (hP : P.Monic) (p k : ℕ) (hp : Nat.Prime p) (hd : P.natDegree = 2 * p ^ k) (hP' : HasCasasAlveroProp P) : ∃ (α : K), P = (Polynomial.X - Polynomial.C α) ^ P.natDegree

The Casas-Alvero conjecture holds for polynomials of degree 2p^k where p is prime. This was proved by Graf von Bothmer, Labs, Schicho, and van de Woestijne.

Reference: The Casas-Alvero conjecture for infinitely many degrees

theorem CasasAlvero.casas_alvero.positive_char_counterexample {p : ℕ} (hp : Nat.Prime p) : ∃ (K : Type u_3) (x : Field K) (_ : CharP K p), have P := Polynomial.X ^ (p + 1) - Polynomial.X ^ p; P.Monic ∧ HasCasasAlveroProp P ∧ ¬∃ (α : K), P = (Polynomial.X - Polynomial.C α) ^ P.natDegree

The Casas-Alvero conjecture fails in positive characteristic p for polynomials of degree p + 1. This was shown by Graf von Bothmer, Labs, Schicho, and van de Woestijne.

Reference: The Casas-Alvero conjecture for infinitely many degrees