Finite character-sum criteria for bijectivity

Complex-valued characters form a basis of the function space on a finite abelian group. Consequently, if a self-map preserves the sum of every character, then it preserves the sum of every complex-valued function. Point indicators then force surjectivity, hence bijectivity.

For finite fields we also record the multiplicative analogue needed by the MCM-permutation argument. If a map has zero as its unique zero and preserves every multiplicative-character sum, restrict it to the unit group and apply the additive criterion to Additive Kˣ.

theorem KasamiCyclicAdditive.bijective_of_addChar_sum_eq {G : Type u_1} [AddCommGroup G] [Fintype G] (f : G → G) (hchar : ∀ (ψ : AddChar G ℂ), ∑ x : G, ψ (f x) = ∑ x : G, ψ x) : Function.Bijective f

A self-map of a finite abelian group is bijective if it preserves the sum of every complex-valued additive character.

theorem KasamiCyclicAdditive.bijective_of_mulChar_sum_eq {K : Type u_2} [Field K] [Fintype K] (f : K → K) (hzero : ∀ (x : K), f x = 0 ↔ x = 0) (hchar : ∀ (χ : MulChar K ℂ), ∑ x : K, χ (f x) = ∑ x : K, χ x) : Function.Bijective f

A finite-field self-map is bijective if zero is its unique zero and it preserves the sum of every complex-valued multiplicative character.