Defining cyclotomic polynomials

Stream: maths

[Antoine Chambert-Loir]

This is a follow up to
https://leanprover.zulipchat.com/#narrow/stream/116395-maths/topic/.239856.20little.20wedderburn/near/258812366
where @Riccardo Brasca observes that the definition of cyclotomic polynomials in mathlib involves complex numbers and the exponential, and asks about a more algebraic definition.

I see two other options

• using, as an intermediate object, a field of char 0 with all nth roots of unity, such as a splitting extension of $T^n-1$.
• building an inductive definition via the relation $\prod_{d|n}\Phi_d=T^n-1$, possibly using Möbius inversion formula.
  But in this second option, the Möbius inversion formula gives a rational function, and you have to prove it is a polynomial. It is not so hard, but not so easy to see that the product for $d|n$ and $d<n$ of all $\Phi_d$ divides $T^n-1$, if one observes that they are pairwise coprime in $\mathbf Q[T]$.

[Riccardo Brasca]

Once one has a field with a primitive n-th root of unity for all n, changing the definition should be very easy.

[Riccardo Brasca]

An interesting experiment would be to see what happens if one use different fields for various n (for example the splitting field of X ^ n - 1).

[Joël Riou]

Isn't it possible to combine both options @Antoine Chambert-Loir ?

• First, construct each individual Phi_n in a any field with a given primitive nth root of unity
• Show that in the case of the complex numbers, these polynomials are in Z[X] and satisfy the expected divisibility properties (i.e. product formula).
• Define by induction the sequence Phi_n for any commutative ring A, with Phi_n defined as the quotient of X^n-1 by the monic polynomial given by the product of the Phi_d for d strictly dividing n.
• Finally, show that the two constructions coincide (using that if a field has a given primitive nth root, it also has dth roots for d dividing n).
  (I do not think this would require Möbius inversion formula or rational functions, even though I have often taught this subject using your second option...)

[Kevin Buzzard]

Here's a start on the second option. Note that polynomial division f /ₘ g is monic polynomial division and it rounds (it's another polynomial) so we never need to consider rational functions.

import tactic
import data.polynomial.div -- I divide polynomials by monic polynomials
import algebra.big_operators.finprod -- I use set.finite products

-- Get access to R[X] notation and ∏ᶠ notation
open_locale polynomial big_operators

open polynomial

-- Definition of Euler Phi directly over ℤ
noncomputable def euler_phi : ℕ → ℤ[X]
| 0 := X^37
| 1 := X - 1
| (n + 2) := (X^(n+2)-1) /ₘ ∏ᶠ d : {d : ℕ // d < n + 2 ∧ d ∣ n + 2},
begin
  -- make d < n + 2 an assumption and then the equation compiler
  -- will let us exit with euler_phi d
  rcases d with ⟨d, hd, -⟩,
  exact (euler_phi d),
end

lemma euler_phi_zero : euler_phi 0 = X^37 :=by simp [euler_phi]

lemma euler_phi_one : euler_phi 1 = X - 1 := by simp [euler_phi]

lemma euler_phi_ge_two (n : ℕ) : euler_phi (n + 2) =
(X^(n+2)-1) /ₘ ∏ᶠ d : {d : ℕ // d < n + 2 ∧ d ∣ n + 2}, euler_phi d :=
begin
  rw euler_phi,
  congr',
  ext ⟨d, hdn, hddiv⟩,
  congr',
end

lemma euler_phi_def (m : ℕ) (hm : 2 ≤ m) :
euler_phi m = (X^m-1) /ₘ ∏ᶠ d : {d : ℕ // d < m ∧ d ∣ m}, euler_phi d :=
begin
  rcases m with h0|h1|m,
  { cases hm },
  { rcases hm with _ | ⟨_, ⟨⟩⟩, },
  { exact euler_phi_ge_two m },
end

[Riccardo Brasca]

In any case the file ring_theory.cyclotomic.basic is now pretty big (more than 1000 lines). It makes sense to split it, I think it should only contains results whose proof really depends on the definition. At the end we can even make the definition irreducible if we want.

[Riccardo Brasca]

I have the impression that what we want is a polynomial cyclotomic n ℤ such that if we base change it to a ring (field? domain? whatever) that has a primitive root of unity, than its roots are exactly the primitive roots of unity. All the rest should follow by this, ignoring the actual definition.

[Antoine Chambert-Loir]

Joël Riou said:

Isn't it possible to combine both options Antoine Chambert-Loir ?

• First, construct each individual Phi_n in a any field with a given primitive nth root of unity
• Show that in the case of the complex numbers, these polynomials are in Z[X] and satisfy the expected divisibility properties (i.e. product formula).
• Define by induction the sequence Phi_n for any commutative ring A, with Phi_n defined as the quotient of X^n-1 by the monic polynomial given by the product of the Phi_d for d strictly dividing n.
• Finally, show that the two constructions coincide (using that if a field has a given primitive nth root, it also has dth roots for d dividing n).
  (I do not think this would require Möbius inversion formula or rational functions, even though I have often taught this subject using your second option...)

Certainly it should be.
Questions.
About step 3, do you define Phi_n as the quotient, even before you proved the rest is 0?
About step 4, I also believe that the uniqueness of the construction should be stated carefully, for example: if P_n and Q_n satisfy \prod_{d|n} P_d = \prod_{d|n} Q_d for all n | N, then P_n = Q_n for all n | N.

[Kevin Buzzard]

Yes that's right, I defined Phi_n the quotient of two polynomials without worrying about the remainder. It's mathematically correct but to a mathematician looks a bit strange. You then have to prove what you're dividing by does divide what you're dividing so you can use the lemma saying a=b/c iff a*c=b which is of course not true in general