| name | polynomial-proof |
| description | Prove properties of polynomials including irreducibility, factorization, and minimal polynomials. Use Eisenstein's criterion, reduction mod p, and the factor theorem. Triggers on "irreducible polynomial", "Eisenstein", "minimal polynomial", "factor theorem", "reducible", "polynomial factorization" |
| tags | ["proof","algebra","polynomial","irreducibility"] |
Polynomial Proof
Prove properties of polynomials including irreducibility, factorization, roots, and minimal polynomials.
The Key Insight
Irreducibility over a ring depends on the ring. A polynomial irreducible over ℚ may factor over ℝ, ℂ, or 𝔽_p. Criteria like Eisenstein and mod p reduction help determine irreducibility.
Step 1: Identify the Ring
Key Definitions
Irreducible over R: A polynomial f ∈ R[x] is irreducible if:
- f is not a unit
- If f = gh, then g or h is a unit
Over different rings:
- Over ℤ: units are ±1
- Over ℚ, ℝ, ℂ: units are nonzero constants
- Over 𝔽_p: units are nonzero elements
Step 2: Check for Easy Factorizations
Rational Root Theorem
For f(x) = aₙxⁿ + ... + a₁x + a₀ ∈ ℤ[x]:
Possible rational roots: ±(divisors of a₀)/(divisors of aₙ)
If none work, f has no linear factors over ℚ.
Factor Theorem
α is a root of f(x) ⟺ (x - α) divides f(x)
Degree Considerations
- deg 1: Always irreducible (over fields)
- deg 2, 3: Irreducible ⟺ no roots
- deg ≥ 4: No roots doesn't imply irreducible
Step 3: Apply Irreducibility Criteria
Eisenstein's Criterion
Theorem: Let f(x) = aₙxⁿ + ... + a₁x + a₀ ∈ ℤ[x].
If there exists a prime p such that:
- p ∤ aₙ (p does not divide leading coefficient)
- p | aᵢ for all i < n (p divides all other coefficients)
- p² ∤ a₀ (p² does not divide constant term)
Then f is irreducible over ℚ.
Example: x⁴ + 10x³ + 15x² + 5x + 5
With p = 5: 5 ∤ 1, 5 | 10, 15, 5, 5, and 25 ∤ 5. ✓
Shift for Eisenstein
If Eisenstein doesn't apply directly, try substituting x → x + a:
Example: f(x) = xᵖ⁻¹ + xᵖ⁻² + ... + x + 1 = (xᵖ - 1)/(x - 1)
Substitute x → x + 1:
g(x) = f(x + 1) = ((x+1)ᵖ - 1)/x = xᵖ⁻¹ + (p choose 1)xᵖ⁻² + ... + p
Apply Eisenstein with prime p. Since f(x) irreducible ⟺ g(x) irreducible, done.
Reduction Mod p
Theorem: If f ∈ ℤ[x] is monic and f̄ (reduction mod p) is irreducible in 𝔽_p[x] with deg(f̄) = deg(f), then f is irreducible over ℚ.
Procedure:
- Choose a prime p
- Reduce all coefficients mod p
- Check if the reduced polynomial is irreducible over 𝔽_p
Caution: Converse is false. f can be irreducible over ℚ but reducible mod every p.
Perron's Criterion
If f(x) = xⁿ + aₙ₋₁xⁿ⁻¹ + ... + a₀ ∈ ℤ[x] with a₀ ≠ 0 and:
|aₙ₋₁| > 1 + |aₙ₋₂| + ... + |a₀|
then f is irreducible over ℚ.
Step 4: Minimal Polynomials
Definition
The minimal polynomial of α over F is the monic polynomial m(x) ∈ F[x] of least degree such that m(α) = 0.
Properties
- m(x) is irreducible over F
- If f(α) = 0 for f ∈ F[x], then m | f
- deg(m) = [F(α) : F] (extension degree)
Finding Minimal Polynomials
- Express powers of α: 1, α, α², ... until linear dependence
- Find the linear relation: c₀ + c₁α + ... + cₙαⁿ = 0
- The minimal polynomial is xⁿ + (cₙ₋₁/cₙ)xⁿ⁻¹ + ... + (c₀/cₙ)
Step 5: Lean Formalization
import Mathlib.RingTheory.Polynomial.Basic
import Mathlib.RingTheory.Polynomial.Eisenstein.Basic
-- Irreducible polynomial
example : Irreducible (X^2 + 1 : ℤ[X]) := by
sorry -- Need to prove no factorization
-- Eisenstein's criterion in Mathlib
-- Polynomial.irreducible_of_eisenstein_criterion
-- Factor theorem
example (f : ℚ[X]) (a : ℚ) (h : f.eval a = 0) :
(X - C a) ∣ f := by
exact Polynomial.dvd_iff_isRoot.mpr h
-- Minimal polynomial
-- minpoly ℚ α gives the minimal polynomial of α over ℚ
variable {F : Type*} [Field F] {E : Type*} [Field E] [Algebra F E]
variable (α : E)
-- Minimal polynomial divides any polynomial with α as root
example (f : F[X]) (h : Polynomial.aeval α f = 0) :
minpoly F α ∣ f := minpoly.dvd F α h
Example: Prove x⁴ + 1 is Irreducible over ℚ
Problem: Show that x⁴ + 1 is irreducible over ℚ.
Proof:
Attempt 1 - Eisenstein: No prime works directly.
Attempt 2 - Substitution: Let g(x) = (x + 1)⁴ + 1.
g(x) = x⁴ + 4x³ + 6x² + 4x + 2
With p = 2:
- 2 ∤ 1 (leading coefficient) ✓
- 2 | 4, 6, 4, 2 ✓
- 4 ∤ 2 ✓
By Eisenstein, g(x) is irreducible over ℚ.
Since g(x) = f(x + 1), and the substitution x → x + 1 is an automorphism of ℚ[x], f(x) is irreducible over ℚ. ∎
Example: Find Minimal Polynomial of √2 + √3 over ℚ
Problem: Find the minimal polynomial of α = √2 + √3.
Solution:
Let α = √2 + √3.
α - √2 = √3
(α - √2)² = 3
α² - 2√2α + 2 = 3
α² - 1 = 2√2α
(α² - 1)² = 8α²
α⁴ - 2α² + 1 = 8α²
α⁴ - 10α² + 1 = 0
So α is a root of f(x) = x⁴ - 10x² + 1.
Verify irreducibility:
- No rational roots (±1 don't work)
- Suppose f = (x² + ax + b)(x² + cx + d) over ℚ
- Expanding and comparing: bd = 1, a + c = 0, b + d + ac = -10
- This gives b + d - a² = -10 and bd = 1
- Solving: no rational solutions
Therefore x⁴ - 10x² + 1 is the minimal polynomial. ∎
Output Format
**Polynomial:** f(x) = [expression] over [ring]
**Irreducibility Test:**
Method: [Eisenstein/Reduction mod p/Direct/etc.]
[Detailed application of criterion]
**Conclusion:** f(x) is [irreducible/reducible] over [ring].
[If reducible, give factorization]
**Lean Proof:**
[Formal verification]
Common Pitfalls
- Wrong ring: x² - 2 is irreducible over ℚ but not over ℝ
- Eisenstein requires monic: Or at least leading coefficient not divisible by p
- Degree 4+: No roots ≠ irreducible; could factor into quadratics
- Mod p reduction: Degree must be preserved (leading coefficient nonzero mod p)
- Minimal polynomial: Must be monic by definition
Advanced Techniques
Cyclotomic Polynomials
The nth cyclotomic polynomial Φₙ(x) is irreducible over ℚ.
- Φₚ(x) = xᵖ⁻¹ + ... + x + 1 for prime p
- Degree: φ(n) (Euler's totient)
Resultants and Discriminants
- Discriminant Δ(f): Related to repeated roots
- Δ = 0 ⟺ f has repeated roots
- For quadratic: Δ = b² - 4ac
Newton Polygon
For polynomials over p-adic fields, Newton polygon gives factorization information.
Algebraic Extensions
If [F(α):F] = n, then the minimal polynomial has degree n.
This connects irreducibility to extension degrees.
