Character orthogonality for finite commutative groups

For a finite commutative group G and a domain M with enough roots of unity, the characters of G are the monoid homomorphisms G →* Mˣ. This file records the column orthogonality relation — the one summed over the character group — in both its punctured and its normal form, and shows that the commutativity it assumes is necessary: the column relation fails for every finite non-commutative group whenever the number of characters is nonzero in M, as it is in characteristic zero. The underlying group-theoretic fact, that homomorphisms into a commutative monoid separate elements only in a commutative group, is TauCeti.isMulCommutative_of_forall_exists_monoidHom_apply_ne_one in TauCeti.GroupTheory.Commutator.

Main results

• CommGroup.sum_monoidHom_apply_eq_zero_of_ne_one: for g ≠ 1, the sum ∑ χ : G →* Mˣ, χ g over all characters vanishes.
• CommGroup.sum_monoidHom_apply_eq_ite: the same sum in normal form, Nat.card G at g = 1 and 0 elsewhere. This is the shape an indicator-formula consumer wants, and it is the simp normal form for such a sum.
• CommGroup.sum_monoidHom_apply_eq_ite's tagged form, CommGroup.sum_inv_mul_monoidHom_apply_eq_ite: summing (χ σ)⁻¹ * χ g isolates the single element σ, giving Nat.card G when g = σ and 0 otherwise.
• AddChar.sum_units_mul_eq_neg_one: a nontrivial additive character of a finite field sums to -1 over the nonzero elements, even after multiplication by a unit.
• TauCeti.sum_monoidHom_apply_eq_card_of_mem_commutator: at an element of the commutator subgroup the character sum is the number of characters, every summand being 1.
• TauCeti.exists_sum_inv_mul_monoidHom_apply_ne_ite: column orthogonality fails for every finite non-commutative group whenever the number of characters is nonzero in M, as in characteristic zero: at the tag 1 and a nontrivial commutator the tagged sum is the number of characters, not 0.

The file also registers Fintype (G →* Mˣ), which Mathlib leaves at Finite; without it a consumer's own character sum does not elaborate, and two ad-hoc Fintype.ofFinite introductions give syntactically distinct sums. That instance needs only LeftCancelMonoid G, so it also serves consumers indexing over the characters of a finite noncommutative group or monoid.

Row orthogonality and punctured additive-character sums

The companion row relation — for a nontrivial χ : G →* Mˣ, the sum ∑ g : G, χ g over the group vanishes — is already sum_hom_units_eq_zero in Mathlib/RingTheory/IntegralDomain.lean, which states exactly that for an arbitrary monoid homomorphism G →* R into a domain. Specialising it to a character is sum_hom_units_eq_zero ((Units.coeHom M).comp χ), i.e. the Mathlib lemma composed with the unit coercion and nothing else, so no declaration for it is added. Callers wanting the row relation should use the Mathlib lemma directly. (MulChar.sum_eq_zero_of_ne_one in Mathlib/NumberTheory/MulChar/Basic.lean is the analogous statement in the MulChar vocabulary, for a multiplicative character of a finite commutative monoid valued in a domain.)

The theorem AddChar.sum_units_mul_eq_neg_one below is not a restatement of that full row relation: it removes the zero term from a finite-field additive-character sum and reindexes the remaining nonzero elements by Fˣ. This punctured form is what character computations over a finite field consume directly.

The column relation genuinely is not in Mathlib in this generality. It appears there only in specialisations: the ZMod n one, DirichletCharacter.sum_characters_eq_zero in Mathlib/NumberTheory/DirichletCharacter/Orthogonality.lean, and the finite-additive-group one over ℂ, AddChar.sum_apply_eq_ite in Mathlib/Analysis/Fourier/FiniteAbelian/PontryaginDuality.lean (with AddChar.sum_apply_eq_zero_iff_ne_zero beside it). Neither implies the statement below, which is multiplicative and valued in an arbitrary domain with enough roots of unity rather than in ℂ or over ZMod n.

References

Two of the results are adapted from CBirkbeck/chebotarev-density (Apache-2.0, Birkbeck--Brasca).

• CommGroup.sum_monoidHom_apply_eq_zero_of_ne_one comes from sum_char_apply_eq_zero_of_ne_one in CebotarevDensity/ForMathlib/CharacterOrthogonality.lean, at commit 8575c9df1ae0a61120ab5c964c7911414254bec7.
• CommGroup.sum_inv_mul_monoidHom_apply_eq_ite comes from the private sum_galoisCharacter_mul_inv_eq in CebotarevDensity/Cyclotomic.lean, at commit 55a89985d47a3befcf6069aca1da250ff088b5c7, where the argument is attributed to Sharifi, Algebraic Number Theory, 7.2.1 step (iii), p. 142. The source writes the sum as ∑ χ, χ σ * (χ τ)⁻¹ with the inverse on the second argument and concludes σ * τ⁻¹ = 1; the statement here carries the inverse on the tag and concludes g = σ, which is the same identity read in the other orientation.

theorem AddChar.sum_units_mul_eq_neg_one {F : Type u_1} [Field F] [Fintype F] {R : Type u_2} [CommRing R] [IsDomain R] (ψ : AddChar F R) (hψ : ψ ≠ 1) (c : Fˣ) : ∑ d : Fˣ, ψ (↑c * ↑d) = -1

A nontrivial additive character of a finite field sums to -1 over the units, even after multiplication by a fixed unit. This is the punctured form of AddChar.sum_eq_zero_of_ne_one.

@[instance_reducible]

noncomputable instance instFintypeMonoidHomUnits {G : Type u_1} [Finite G] {M : Type u_2} [CommRing M] [IsDomain M] [LeftCancelMonoid G] : Fintype (G →* Mˣ)

The characters of a finite left-cancellative monoid valued in a domain form a Fintype. Mathlib registers only Finite (G →* Mˣ), so a character sum written by a consumer has no Finset to range over without this; it mirrors AddChar.instFintype. Neither commutativity nor invertibility is needed: Finite (G →* Mˣ) already holds at LeftCancelMonoid, which is where this is stated.

Equations

• instFintypeMonoidHomUnits = Fintype.ofFinite (G →* Mˣ)

theorem CommGroup.sum_monoidHom_apply_eq_zero_of_ne_one {G : Type u_1} [Finite G] {M : Type u_2} [CommRing M] [IsDomain M] [CommGroup G] [HasEnoughRootsOfUnity M (Monoid.exponent G)] {g : G} (hg : g ≠ 1) : ∑ χ : G →* Mˣ, ↑(χ g) = 0

Character-column orthogonality for a finite commutative group G valued in a domain M with enough roots of unity: for g ≠ 1, the sum of χ g over all characters χ : G →* Mˣ vanishes.

@[simp]

theorem CommGroup.sum_monoidHom_apply_eq_ite {G : Type u_1} [Finite G] {M : Type u_2} [CommRing M] [IsDomain M] [CommGroup G] [HasEnoughRootsOfUnity M (Monoid.exponent G)] [DecidableEq G] (g : G) : ∑ χ : G →* Mˣ, ↑(χ g) = if g = 1 then ↑(Nat.card G) else 0

Column orthogonality in normal form: the character sum is Nat.card G at the identity and vanishes elsewhere. This covers both cases at once, and states the identity value as the cardinality of G itself rather than of its dual, which is the shape an indicator-formula consumer wants.

@[simp]

theorem CommGroup.sum_inv_mul_monoidHom_apply_eq_ite {G : Type u_1} [Finite G] {M : Type u_2} [CommRing M] [IsDomain M] [CommGroup G] [HasEnoughRootsOfUnity M (Monoid.exponent G)] [DecidableEq G] (σ g : G) : ∑ χ : G →* Mˣ, ↑(χ σ)⁻¹ * ↑(χ g) = if g = σ then ↑(Nat.card G) else 0

Tagged column orthogonality. Summing (χ σ)⁻¹ * χ g over all characters isolates the single element σ: the sum is Nat.card G when g = σ and 0 otherwise. This is the form a fibre-selecting argument uses, sum_monoidHom_apply_eq_ite being the case σ = 1.

The inverse sits on the tag σ, not on the argument g. Without it the sum is ∑ χ, χ (σ * g), which is the indicator of g = σ⁻¹ — a different fibre, and one that genuinely differs whenever σ is not an involution.

@[simp]

theorem TauCeti.sum_monoidHom_apply_eq_card_of_mem_commutator {G : Type u_1} [Finite G] {M : Type u_2} [CommRing M] [IsDomain M] [Group G] {g : G} (hg : g ∈ commutator G) : ∑ χ : G →* Mˣ, ↑(χ g) = ↑(Nat.card (G →* Mˣ))

The character sum at an element of the commutator subgroup counts the characters. Every character χ : G →* Mˣ kills the commutator subgroup, so at such an element every summand of the column sum is 1. For a commutative group the commutator subgroup is trivial and this is the g = 1 case of CommGroup.sum_monoidHom_apply_eq_ite; for a non-commutative group it is the value at which the column relation breaks.

theorem TauCeti.exists_sum_inv_mul_monoidHom_apply_ne_ite {G : Type u_1} [Finite G] {M : Type u_2} [CommRing M] [IsDomain M] [Group G] [DecidableEq G] (hG : ¬IsMulCommutative G) (hcard : ↑(Nat.card (G →* Mˣ)) ≠ 0) : ∃ (σ : G) (g : G), ∑ χ : G →* Mˣ, ↑(χ σ)⁻¹ * ↑(χ g) ≠ if g = σ then ↑(Nat.card G) else 0

Column orthogonality fails for every finite non-commutative group. In a non-commutative group some commutator g = ⁅a, b⁆ differs from 1, and every character kills it, so the tagged sum at σ = 1 and this g is the number of characters rather than the 0 that CommGroup.sum_inv_mul_monoidHom_apply_eq_ite gives for g ≠ σ in a commutative group. Besides the standing assumption that M is a domain, the only hypothesis on M is that this count is nonzero in M; in characteristic zero it is supplied by Nat.cast_ne_zero.mpr Nat.card_pos.ne', and no roots of unity are needed.