Additions to AddChar

Stream: mathlib4

[Daniel Weber]

Hi! As I've said in #mathlib4 > github permission , I've been working on a few theorems for docs#AddChar, and I want to contribute them. This is what I proved (I'm aware some of these names are terrible, I'd love better ideas):

• equiv_addChar (h : R ≃+ R₂) : AddChar R R' ≃* AddChar R₂ R': there is an isomorphism between characters on isomorphic groups.
• map_sum_prod (ψ : AddChar R R') (f : l → R) : ψ (∑ x, f x) = ∏ x, (ψ (f x)): an extension of map_add_mul for finite sums and products.
• equiv_directSum_addChar : AddChar (⨁ i, f i) R' ≃ Π i, AddChar (f i) R': AddChar distributes over direct sum. This is actually an isomorphism, but direct product doesn't seem to be defined for multiplicative groups, so I'm not sure how to state that.
• zmod_equiv_addChar (n : ℕ+) (h : 1 < n) : AddChar (ZMod n) R' ≃* rootsOfUnity n R': this is an extension of zmodChar which also provides the other direction.
• card_AddChar [Fact (∀ n : ℕ+, Fintype.card (rootsOfUnity n R') = n)] : Nat.card (AddChar R R') = Nat.card R: the additive characters from a finite commutative group to a domain with full roots of unity have the same cardinality as the group.
• noncomputable def embed [Fact (∀ n : ℕ+, Fintype.card (rootsOfUnity n R') = n)] : R ≃ (AddChar R R'): under the above conditions, there is a (noncomputable) equivalence between characters of a group and elements of it.
• noncomputable instance fintype: Fintype (AddChar R R') : There is a finite number of characters from a finite commutative group to a domain.
• orthogonality (h : ψ ≠ φ) : ∑ a, ψ a * φ⁻¹ a = 0
• norm : ∑ a, ψ a * ψ⁻¹ a = Fintype.card R
• sum_chars_ne [Fact (∀ n : ℕ+, Fintype.card (rootsOfUnity n R') = n)] [Invertible (Fintype.card R : R')] (h : x ≠ y) : ∑ χ : AddChar R R', χ x * χ⁻¹ y = 0 (I'm not sure if the cardinality being invertible is required, but my proof needs it)
• sum_chars_eq : ∑ χ : AddChar R R', χ x * χ⁻¹ x = Fintype.card (AddChar R R')

[Daniel Weber]

I also want to prove a few results about Fourier analysis on finite groups. Where should these be placed?

[Junyan Xu]

• equiv_addChar should be equivAddChar by naming convention, but I think AddEquiv.addCharCongr is a better name.
• We should provide List, Multiset, and Finset versions of map_sum_prod to make a complete API. Maybe call them AddChar.map_list_sum, AddChar.map_multiset_sum, AddChar.map_finset_sum (I think it's also common to omit finset_); the Fintype version should be subsumed by the Finset version.
• equiv_directSum_addChar (better name: AddChar.directSumEquiv): there are instances docs#Pi.monoid and docs#Pi.group on the direct product, maybe you're just missing imports?
• zmod_equiv_addChar (better name: AddChar.zmodEquiv): why require 1 < n?
• capitalization of card_AddChar should be card_addChar by naming convention. The condition for all n : ℕ+ is too restrictive, for example no fields of positive characteristic p could possibly satisfy it, because there's only one pth root of unity. However, it suffices to require the equality for n = exponent of R.
• embed: AddChar R R' is canonically isomorphic to the docs#PontryaginDual of R (if you give R the discrete topology). May be we should define the canonical MulEquiv between AddChar R R' and AddChar R circle?
• orthogonality: mathlib might prefer a more descriptive name like AddChar.sum_apply_mul_inv_apply_eq_zero.
• norm: maybe sum_apply_mul_inv_apply_eq_card.
• sum_chars_ne (maybe sum_eval_mul_inv_eval_eq_zero): you can rewrite the summand as χ (x - y) and notice that evaluation at x - y is a homomorphism from AddChar R R' to R', so the sum is equal to the cardinality of the kernel times the sum of the image. If the image isn't {1} then its sum is zero (I can imagine proving this via Vieta's formula or by summing geometric series; not sure which approach you took). So indeed the Invertible condition shouldn't be required.
• sum_chars_eq: maybe sum_eval_mul_inv_eval_eq_card.
  (Note that I'm establishing a convention that apply refers to a sum in which the same character(s) are applied to different elements, while eval refers to a sum over characters applied to the same elements.)

[Daniel Weber]

Thanks for the feedback!

• zmodEquiv: You're right, it isn't needed
• Regarding card_addChar, would it be better to require the equality of the cardinality for exponent R, or require giving an exponent R-th primitive root?
• For embed, I'm not exactly sure what you mean, could you please clarify?
• sum_eval_mul_inv_eval_eq_zero: I proved it by creating two matrices A i j = (embed i) j, A* i j = (embed j)⁻¹ i, showing (using sum_apply_mul_inv_apply_eq_zero and sum_apply_mul_inv_apply_eq_card) that A A* = card I, and then using mul_eq_one_comm after rewriting it as (A / card) A* = I. Do you know any references for a proof that doesn't require the invertibility?

[Eric Wieser]

I recommend contributing a few of these at a time, rather than all of them at once

[Eric Wieser]

map_sum_prod and friends feel like they're rather foundational, so might make sense to do first

[Yaël Dillies]

Sorry, I have basically all of this material in LeanAPAP already, and I am about to open a bunch of PRs to add it to mathlib.

[Daniel Weber]

Yaël Dillies said:

Sorry, I have basically all of this material in LeanAPAP already, and I am about to open a bunch of PRs to add it to mathlib.

Oh, ok. Please ping me when you open these PRs. I see you have also defined and proven some results on DFT, which is also the application I needed it for. Have you proven Vazirani’s XOR lemma (a bound on the non-trivial Fourier coefficients of a distribution implies a bound on its statistical distance from the uniform distribution), by any chance?

[Yaël Dillies]

Never heard of Vazirani's XOR lemma, no!

[Daniel Weber]

Ok, then I'll prove it, and I guess I'll depend on LeanAPAP until it's added to mathlib

[Yaël Dillies]

Sorry that this is taking so long (I wrote most of this code this summer) but upstreaming 170 files is no easy task.

[Yaël Dillies]

(there's roughly 60 left right now)

[Junyan Xu]

• Re: card_addChar: #(rootsOfUnity n R')=n is equivalent to the existence of a primitive nth root of unity in a domain, so either should be fine. Maybe it's better to introduce a predicate (typeclass?) HasPrimitiveRoot and use it everywhere ...
• Re embed: please ignore what I said; there isn't actually a canonical isomorphism between AddChar R R' and AddChar R circle since R' doesn't have distinguished primitive roots of unity.
• Re sum_eval_mul_inv_eval_eq_zero: I think you can just apply docs#IntegralDomain.html#sum_hom_units_eq_zero to the evaluation homomorphism (at x - y). The homomorphism is not 1 since x - y is not 0 (for this you need that for every prime p dividing the exponent (equivalently, cardinality) of R, there exists a primitive pth root of unity, but it's not necessary that there exists a primitive (exponent R)-th root of unity).