The ideal Möbius function and Möbius inversion

The Möbius function of a nonzero ideal A of the ring of integers of a number field K is (-1) ^ k when A is a product of k distinct prime ideals and 0 otherwise. This file packages it as a TauCeti.IdealArithmeticFunction K, computes it on prime powers, and proves that it is the inverse of the everywhere-one function for the ideal Dirichlet convolution. That inverse relation is the ideal Möbius inversion formula, stated here as an equivalence between the two directions.

Main definitions

• TauCeti.IdealArithmeticFunction.moebius is the ideal Möbius function, the complex-valued restriction of Mathlib's UniqueFactorizationMonoid.moebius to the nonzero ideals of 𝓞 K.

Main results

• TauCeti.Ideal.sum_moebius_divisorsAntidiagonal_of_ne_one: the Möbius function sums to zero over the factorizations of a nonzero ideal other than the unit ideal. This is the combinatorial heart of the file.
• TauCeti.IdealArithmeticFunction.convolution_moebius_one and TauCeti.IdealArithmeticFunction.convolution_one_moebius: the ideal Möbius function is a two-sided inverse of the everywhere-one function for ideal convolution.
• TauCeti.IdealArithmeticFunction.convolution_one_eq_iff: ideal Möbius inversion, the equivalence between convolution f 1 = g and f = convolution g moebius.
• TauCeti.IdealArithmeticFunction.moebius_apply_prime, TauCeti.IdealArithmeticFunction.moebius_apply_prime_pow, and TauCeti.IdealArithmeticFunction.moebius_mul_of_isRelPrime: the prime-power values and multiplicativity on coprime ideals.
• TauCeti.IdealArithmeticFunction.not_exists_multiplicativeIdealWeight_eq_moebius and TauCeti.IdealArithmeticFunction.not_exists_unitaryIdealWeight_eq_moebius: the rejection tests. The ideal Möbius function underlies neither ideal-weight carrier, because those carriers are completely multiplicative while μ (𝔭 ^ 2) = 0.

Implementation notes

Mathlib's UniqueFactorizationMonoid.moebius already supplies the definition, the squarefree and prime values, and multiplicativity on relatively prime elements for an arbitrary unique factorization monoid, so TauCeti.IdealArithmeticFunction.moebius is its complex-valued restriction rather than a fresh definition. What Mathlib does not supply — and what this file proves — is the divisor-sum identity, since the divisor sum needs a finite index set, and for ideals that is TauCeti.Ideal.divisorsAntidiagonal.

The divisor sum is proved over ℤ and then cast, so that it can consume Mathlib's Finset.sum_powerset_neg_one_pow_card_of_nonempty directly. The proof reindexes the squarefree factorizations of A by the subsets of the finite set of prime ideals dividing A: a squarefree divisor is the product of the subset of primes it is divisible by, and the Möbius function of that divisor is (-1) to the size of the subset. The alternating sum over a nonempty powerset vanishes.

The ideal Möbius function is not completely multiplicative, so it is not a TauCeti.MultiplicativeIdealWeight; the two rejection theorems record this rather than leaving it to the reader, following TauCeti.MultiplicativeIdealWeight.not_exists_toIdealArithmeticFunction_eq_one.

References

• J. Neukirch, Algebraic Number Theory, Chapter VII.
• G. Tenenbaum, Introduction to Analytic and Probabilistic Number Theory, Chapter I.2.

The ideal Möbius function

noncomputable def TauCeti.IdealArithmeticFunction.moebius {K : Type u_1} [Field K] [NumberField K] : IdealArithmeticFunction K

The ideal Möbius function of a number field K: the value at a nonzero ideal A is (-1) ^ k when A is a product of k distinct prime ideals, and 0 when A is divisible by the square of a prime ideal.

It is the complex-valued restriction of Mathlib's UniqueFactorizationMonoid.moebius for the unique factorization monoid Ideal (𝓞 K).

theorem TauCeti.IdealArithmeticFunction.moebius_apply {K : Type u_1} [Field K] [NumberField K] (A : ↥(nonZeroDivisors (Ideal (NumberField.RingOfIntegers K)))) : moebius A = ↑(UniqueFactorizationMonoid.moebius ↑A)

@[simp]

theorem TauCeti.IdealArithmeticFunction.moebius_one {K : Type u_1} [Field K] [NumberField K] : moebius 1 = 1

@[simp]

theorem TauCeti.IdealArithmeticFunction.moebius_of_not_squarefree {K : Type u_1} [Field K] [NumberField K] {A : ↥(nonZeroDivisors (Ideal (NumberField.RingOfIntegers K)))} (hA : ¬Squarefree ↑A) : moebius A = 0

The Möbius function vanishes at an ideal divisible by the square of a prime.

theorem TauCeti.IdealArithmeticFunction.moebius_apply_of_squarefree {K : Type u_1} [Field K] [NumberField K] {A : ↥(nonZeroDivisors (Ideal (NumberField.RingOfIntegers K)))} (hA : Squarefree ↑A) : moebius A = (-1) ^ (UniqueFactorizationMonoid.normalizedFactors ↑A).card

At a squarefree ideal the Möbius function is (-1) to the number of prime factors.

theorem TauCeti.IdealArithmeticFunction.moebius_apply_prime {K : Type u_1} [Field K] [NumberField K] {A : ↥(nonZeroDivisors (Ideal (NumberField.RingOfIntegers K)))} (hA : Prime ↑A) : moebius A = -1

The Möbius function of a prime ideal is -1.

theorem TauCeti.IdealArithmeticFunction.moebius_apply_pow_of_not_isUnit {K : Type u_1} [Field K] [NumberField K] {A : ↥(nonZeroDivisors (Ideal (NumberField.RingOfIntegers K)))} (hA : ¬IsUnit ↑A) {n : ℕ} (hn : 2 ≤ n) : moebius (A ^ n) = 0

The Möbius function vanishes at a power with exponent at least two of any ideal that is not the unit ideal, since that power is then divisible by a square.

theorem TauCeti.IdealArithmeticFunction.moebius_apply_prime_pow {K : Type u_1} [Field K] [NumberField K] {A : ↥(nonZeroDivisors (Ideal (NumberField.RingOfIntegers K)))} (hA : Prime ↑A) {n : ℕ} (hn : 2 ≤ n) : moebius (A ^ n) = 0

The Möbius function vanishes at a prime power with exponent at least two.

theorem TauCeti.IdealArithmeticFunction.moebius_mul_of_isRelPrime {K : Type u_1} [Field K] [NumberField K] {A B : ↥(nonZeroDivisors (Ideal (NumberField.RingOfIntegers K)))} (h : IsRelPrime ↑A ↑B) : moebius (A * B) = moebius A * moebius B

The Möbius function is multiplicative on coprime ideals. Together with TauCeti.IdealArithmeticFunction.moebius_apply_prime_pow this is the precise sense in which it is multiplicative: it is not completely multiplicative.

theorem TauCeti.IdealArithmeticFunction.isMultiplicative_moebius {K : Type u_1} [Field K] [NumberField K] : moebius.IsMultiplicative

The ideal Möbius function is multiplicative on relatively prime ideals.

The divisor sum of the Möbius function

theorem TauCeti.Ideal.sum_moebius_divisorsAntidiagonal_of_ne_one {K : Type u_1} [Field K] [NumberField K] {A : ↥(nonZeroDivisors (Ideal (NumberField.RingOfIntegers K)))} (hA : A ≠ 1) : ∑ p ∈ divisorsAntidiagonal A, UniqueFactorizationMonoid.moebius ↑p.1 = 0

The Möbius function sums to zero over the factorizations of a nonzero ideal that is not the unit ideal.

The squarefree first entries of the antidiagonal are exactly the products of subsets of the finite set P of prime ideals dividing A, and the Möbius function of such a product is (-1) to the size of the subset; the alternating sum over the powerset of a nonempty P vanishes. The entries that are not squarefree contribute nothing.

Möbius inversion

@[simp]

theorem TauCeti.IdealArithmeticFunction.convolution_moebius_one {K : Type u_1} [Field K] [NumberField K] : moebius.convolution 1 = delta

The ideal Möbius function is a left inverse of the everywhere-one function for ideal convolution.

@[simp]

theorem TauCeti.IdealArithmeticFunction.convolution_one_moebius {K : Type u_1} [Field K] [NumberField K] : convolution 1 moebius = delta

The ideal Möbius function is a right inverse of the everywhere-one function for ideal convolution.

theorem TauCeti.IdealArithmeticFunction.convolution_one_eq_iff {K : Type u_1} [Field K] [NumberField K] {f g : IdealArithmeticFunction K} : f.convolution 1 = g ↔ f = g.convolution moebius

Ideal Möbius inversion. Summing an ideal arithmetic function over the divisors of an ideal is inverted by convolving with the ideal Möbius function.

theorem TauCeti.IdealArithmeticFunction.normCoeff_moebius_mul_normCoeff_one {K : Type u_1} [Field K] [NumberField K] : (normCoeff K) moebius * (normCoeff K) 1 = 1

Regrouping by absolute norm sends the ideal Möbius inversion identity to the corresponding identity for Mathlib's Dirichlet convolution of arithmetic functions.

The Möbius function is not an ideal weight

theorem TauCeti.IdealArithmeticFunction.not_exists_multiplicativeIdealWeight_eq_moebius {K : Type u_1} [Field K] [NumberField K] : ¬∃ (χ : MultiplicativeIdealWeight K), χ.toIdealArithmeticFunction = moebius

Rejection test. The ideal Möbius function underlies no multiplicative ideal weight: such a weight is completely multiplicative, so it takes the value 1 at the square of a prime at which it takes the value -1, whereas the Möbius function vanishes there.

theorem TauCeti.IdealArithmeticFunction.not_exists_unitaryIdealWeight_eq_moebius {K : Type u_1} [Field K] [NumberField K] : ¬∃ (χ : UnitaryIdealWeight K), χ.toIdealArithmeticFunction = moebius

Rejection test. The ideal Möbius function underlies no unitary ideal weight either, since a unitary weight is in particular a multiplicative one.