The average of a multiset of complex roots of unity

A sum of d complex roots of unity has absolute value at most d. This file proves an arithmetic sharpening: if the average of the summands happens to be an algebraic integer, then the sum is either 0 or of absolute value exactly d, with nothing in between possible.

The proof is Kronecker's theorem. Fix a primitive n-th root of unity ζ; the number field ℚ(ζ) contains every n-th root of unity, hence the sum x and its average α = x / d. A field embedding of ℚ(ζ) into ℂ sends each summand to an n-th root of unity, so it sends x to a sum of d complex numbers of modulus one; therefore ‖α‖ ≤ 1 at every embedding, not just the inclusion we started with. A nonzero algebraic integer with that property is a root of unity (NumberField.Embeddings.pow_eq_one_of_norm_le_one), so ‖α‖ = 1.

The hypothesis on the average is what makes the statement bite: without it the bound ‖x‖ ≤ d is all there is, and intermediate absolute values really do occur, 1 + i being a sum of two fourth roots of unity of absolute value √2.

Main statements

• TauCeti.sum_eq_zero_or_norm_sum_eq_card_of_isIntegral: a multiset of n-th roots of unity whose average is integral over ℤ has sum 0, or a sum whose absolute value is its cardinality.
• TauCeti.norm_map_multiset_sum_le_card: the image in ℂ of a sum of n-th roots of unity has absolute value at most the number of summands, under any ring homomorphism.

References

• Kronecker's theorem on algebraic integers in the closed unit disc, in Mathlib as NumberField.Embeddings.pow_eq_one_of_norm_le_one.
• I. M. Isaacs, Character Theory of Finite Groups (1976), Theorem 3.8, where this is the Kronecker half of Burnside's vanishing theorem for character values, applied to the average once the arithmetic half has shown that average to be an algebraic integer.

theorem TauCeti.norm_map_multiset_sum_le_card {K : Type u_1} [Semiring K] {n : ℕ} (hn : n ≠ 0) {t : Multiset K} (ht : ∀ ν ∈ t, ν ^ n = 1) (φ : K →+* ℂ) : ‖φ t.sum‖ ≤ ↑t.card

A ring homomorphism into ℂ sends a multiset of n-th roots of unity to complex numbers of modulus one, so it sends their sum to a complex number of modulus at most the cardinality.

theorem TauCeti.sum_eq_zero_or_norm_sum_eq_card_of_isIntegral {n : ℕ} (hn : n ≠ 0) {s : Multiset ℂ} (hs : ∀ μ ∈ s, μ ^ n = 1) (hint : IsIntegral ℤ (s.sum / ↑s.card)) : s.sum = 0 ∨ ‖s.sum‖ = ↑s.card

The average of a multiset of roots of unity is 0 or of modulus one, once it is an algebraic integer. If every element of a multiset s of complex numbers is an n-th root of unity and the average s.sum / #s is integral over ℤ, then either s.sum = 0 or ‖s.sum‖ = #s.

This is Kronecker's theorem applied inside ℚ(ζ) for ζ a primitive n-th root of unity: the average is an algebraic integer all of whose conjugates lie in the closed unit disc, because each conjugate is again an average of #s complex numbers of modulus one.