Character sums over a subgroup

For a finite subgroup H of a group G and a multiplicative character χ : G →* k, this file studies the element ∑_{h ∈ H} χ(h) h of the group algebra k[G], here TauCeti.subgroupCharSum χ H.

Two instances of it occur throughout representation theory, and are what this file exists to share: the norm element ∑_{h ∈ H} h of a subgroup, which is χ = 1, and the signed sum ∑_{h ∈ H} sgn(h) h of a subgroup of a permutation group, which is χ = sgn. The row symmetrizer and the column antisymmetrizer of a Young tableau are exactly these two.

Everything here follows from χ being multiplicative; no assumption that χ takes values in square roots of 1 is needed, even for the square. The translation laws say that left or right multiplication by p ∈ H rescales the sum by χ(p⁻¹), which is proved by reindexing the sum along the bijection h ↦ p * h of H; the square is then obtained by summing the left translation law over H, where the scalars χ(h) χ(h⁻¹) = χ(1) = 1 collapse and leave the order of H.

Main definitions and results

• TauCeti.subgroupCharSum: the character sum ∑_{h ∈ H} χ(h) h in k[G];
• TauCeti.subgroupCharSum_coeff: its coefficients are χ on H and zero off H;
• TauCeti.single_mul_subgroupCharSum and TauCeti.subgroupCharSum_mul_single: the two translation laws, scaling by χ(p⁻¹) for p ∈ H;
• TauCeti.subgroupCharSum_mul_self: the character sum squares to Nat.card H times itself;
• TauCeti.subgroupCharSum_eq_one and TauCeti.subgroupCharSum_eq_sum_of_eq_top: its values on the two extreme subgroups, ⊥ and ⊤.

noncomputable def TauCeti.subgroupCharSum {k : Type u_1} {G : Type u_2} [CommSemiring k] [Group G] (χ : G →* k) (H : Subgroup G) [Fintype ↥H] : MonoidAlgebra k G

The character sum ∑_{h ∈ H} χ(h) h of a multiplicative character χ over a finite subgroup H, as an element of the group algebra k[G].

Equations

• TauCeti.subgroupCharSum χ H = ∑ h : ↥H, χ ↑h • (MonoidAlgebra.of k G) ↑h

theorem TauCeti.subgroupCharSum_def {k : Type u_1} {G : Type u_2} [CommSemiring k] [Group G] (χ : G →* k) (H : Subgroup G) [Fintype ↥H] : subgroupCharSum χ H = ∑ h : ↥H, χ ↑h • (MonoidAlgebra.of k G) ↑h

The character sum is the χ-weighted sum of the basis elements indexed by H.

@[simp]

theorem TauCeti.subgroupCharSum_coeff {k : Type u_1} {G : Type u_2} [CommSemiring k] [Group G] (χ : G →* k) (H : Subgroup G) [Fintype ↥H] [DecidablePred fun (x : G) => x ∈ H] (g : G) : (subgroupCharSum χ H).coeff g = if g ∈ H then χ g else 0

The coefficient of a group element in the character sum is χ on H and zero off H.

@[simp]

theorem TauCeti.single_mul_subgroupCharSum {k : Type u_1} {G : Type u_2} [CommSemiring k] [Group G] (χ : G →* k) (H : Subgroup G) [Fintype ↥H] (p : ↥H) : MonoidAlgebra.single (↑p) 1 * subgroupCharSum χ H = χ (↑p)⁻¹ • subgroupCharSum χ H

Left multiplication by a member of H scales the character sum by χ of its inverse.

@[simp]

theorem TauCeti.subgroupCharSum_mul_single {k : Type u_1} {G : Type u_2} [CommSemiring k] [Group G] (χ : G →* k) (H : Subgroup G) [Fintype ↥H] (p : ↥H) : subgroupCharSum χ H * MonoidAlgebra.single (↑p) 1 = χ (↑p)⁻¹ • subgroupCharSum χ H

Right multiplication by a member of H scales the character sum by χ of its inverse.

@[simp]

theorem TauCeti.subgroupCharSum_mul_self {k : Type u_1} {G : Type u_2} [CommSemiring k] [Group G] (χ : G →* k) (H : Subgroup G) [Fintype ↥H] : subgroupCharSum χ H * subgroupCharSum χ H = Nat.card ↥H • subgroupCharSum χ H

The character sum squares to the order of H times itself.

theorem TauCeti.subgroupCharSum_eq_one {k : Type u_1} {G : Type u_2} [CommSemiring k] [Group G] (χ : G →* k) (H : Subgroup G) [Fintype ↥H] (h : H = ⊥) : subgroupCharSum χ H = 1

Over the trivial subgroup the character sum has the single term χ 1 • 1, so it is 1.

theorem TauCeti.subgroupCharSum_eq_sum_of_eq_top {k : Type u_1} {G : Type u_2} [CommSemiring k] [Group G] (χ : G →* k) (H : Subgroup G) [Fintype ↥H] [Fintype G] (h : H = ⊤) : subgroupCharSum χ H = ∑ g : G, χ g • (MonoidAlgebra.of k G) g

The character sum over the whole group is the χ-weighted sum over the group.