The fifth cyclotomic polynomial over a field containing √5

Over any field E of characteristic different from 2 containing a square root s of 5, the fifth cyclotomic polynomial factors as

Φ_5 = (X² − αX + 1) (X² − βX + 1), with α = (s − 1)/2 and β = (−s − 1)/2,

because α + β = −1 and αβ = (1 − s²)/4 = −1. In particular Φ_5 is not irreducible over E.

The hypothesis 2 ≠ 0 is genuinely needed: over ZMod 2 one has 1 ^ 2 = 5 while Φ_5 is irreducible, since 2 has order 4 modulo 5.

Main results

• Polynomial.cyclotomic_five_eq_mul_of_sq_eq_five: the explicit factorisation.
• Polynomial.not_irreducible_cyclotomic_five_of_sq_eq_five: Φ_5 is reducible over E.

References

Over K = ℚ(√5) the fifth cyclotomic polynomial is reducible. This is why irreducibility of Φ_q over a general base needs a hypothesis such as unramifiedness: 5 ramifies in ℚ(√5).

That ℚ(√5) is the quadratic subfield of ℚ(ζ_5) is Sharifi, Algebraic Number Theory, Lemma 3.2.2.

theorem Polynomial.cyclotomic_five_eq_mul_of_sq_eq_five {E : Type u_1} [Field E] [NeZero 2] {s : E} (hs : s ^ 2 = 5) : cyclotomic 5 E = (X ^ 2 - C ((s - 1) / 2) * X + 1) * (X ^ 2 - C ((-s - 1) / 2) * X + 1)

Φ_5 factors over a field containing √5. With s ^ 2 = 5 the two factors are X² − ((s − 1)/2) X + 1 and X² − ((−s − 1)/2) X + 1.

Source: Sharifi, Algebraic Number Theory, Lemma 3.2.2 (ℚ(√5) ⊆ ℚ(µ_5)), made explicit.

theorem Polynomial.not_irreducible_cyclotomic_five_of_sq_eq_five {E : Type u_1} [Field E] [NeZero 2] (h5 : ∃ (x : E), x ^ 2 = 5) : ¬Irreducible (cyclotomic 5 E)

Φ_5 is reducible over a field containing √5.

This bounds no degree by itself: E may already contain ζ_5, in which case Φ_5 splits into linear factors. What the statement gives is reducibility, and hence that Φ_5 is not the minimal polynomial of a primitive fifth root of unity over E.