Orthogonality of Dirichlet characters

Stream: PR reviews

[Michael Stoll]

I am starting a series of PRs with the goal of getting the following statement into Mathlib:

theorem sum_char_inv_mul_char_eq [HasEnoughRootsOfUnity R n.totient] {a : ZMod n}
    (ha : IsUnit a) (b : ZMod n) :
    ∑ χ : DirichletCharacter R n, χ a⁻¹ * χ b = if a = b then n.totient else 0 := by

This is a requirement for Dirichlet's Theorem on primes in AP (and useful beyond that).

The overall plan is to do it in stages:

1. results for finite cyclic groups
2. results for finite abelian groups
3. results for multiplicative characters
4. results for Dirichlet characters

The "results" of the kind Hom(G, G') ≃* G and related, where the target G' "has enough roots of unity". See the Orthogonality file in EulerProducts for the complete development (~500 loc).

The first installment is #18659, which establishes a multiplicative version of the classification theorem for finite abelian groups (this helps in going from 1. to 2. above). Reviews are welcome!

[Michael Stoll]

The next one is #18669; it splits RingTheory.RootsOfUnity.Basic into two files: RingTheory.RootsOfUnity.Basic (~ first quarter) and RingTheory.RootsOfUnity.PrimitiveRoots (the remaining three quarters). The natural splitting point is where primitive roots of unity are introduced.

This is in preparation for adding more material; the current Basic file has already close to 1000 lines.

[Riccardo Brasca]

Merging it.

[Michael Stoll]

#18673 adds some API around Pi.mulSingle, which is helpful for dealing with products (this is used in deriving results for general finite abelian groups from results on cyclic groups).

[Michael Stoll]

#18675 adds NeZero instances for Monoid.exponent G and n.totient, which are convenient for the later development.

[Michael Stoll]

#18681 introduces the class HasEnoughRootsOfUnity, which is the property we need for targets of Hom groups to give a workable notion of duality.

[Michael Stoll]

After the preparations, #18687 now deals with point 1 above (results for cyclic groups).

[Michael Stoll]

:ping_pong: #18687 has an approving review. Is there more to be done?

[Michael Stoll]

#18729 is again a preparatory PR: it moves GroupTheory.FiniteAbelian as GroupTheory.FiniteAbelian.Basic to a new folder, so that I can add a new file GroupTheory.FiniteAbelian.Duality with new material (that requires more imports) in the next PR.
BTW, thanks for merging these PRs quickly!

[Michael Stoll]

#18738 is now dealing with point 2 above (duality for finite abelian groups). It adds a new file GroupTheory.FiniteAbelian.Duality (and has some minor fixes of documentation and a missing namespace).

[Riccardo Brasca]

Having a look

[Michael Stoll]

#18759 adds an instance HasEnoughRootsOfUnity F n when F is an algebraically closed field and n is not divisible by the characteristic of F. In particular, this provides HasEnoughRootsOfUnity ℂ n for all nonzero n, which will be needed for Dirichlet's Theorem and should also be useful for #15999.

[Michael Stoll]

#18760 does step 3 above (duality for multiplicative characters).

[Michael Stoll]

@Yaël Dillies I will look at #15999 later today, after #18759 is merged (so that I can try to use it for golfing).

[Yaël Dillies]

Amazing!

[Michael Stoll]

Michael Stoll said:

#18760 does step 3 above (duality for multiplicative characters).

:ping_pong:

[Michael Stoll]

#18777 is now the last step, culminating in the statement given in the first message of this thread.