Permutation classes of quotients of prime-power exponent

Let k have characteristic p. If D is a normal subgroup of a finite group C and every element of C has a p-power power in D, the permutation module k[C/D], regarded as a C-module, has exact Grothendieck class [C : D] • [k]. This equality uses short exact sequences and includes permutation modules which are not direct sums of trivial lines.

For prime p and a finite cyclic subgroup C, its subgroup of order prime to p satisfies these hypotheses.

Inducing to a finite group G containing C, and using that Ind_C^G k[C/D] = k[G/D] (TauCeti.indK0_of_ofMulAction_quotient), turns this into an equality of induced classes: [Ind_D^G k] = [C : D] • [Ind_C^G k] (TauCeti.indK0_of_trivial_eq_relIndex_nsmul). For a cyclic C and prime p this says that the p-part of |C| times the class of Ind_C^G k is the class induced from the trivial line of the subgroup of C of order prime to p (TauCeti.exists_coprimePart_indK0_of_trivial_eq_nsmul); this is the input that removes the p-part of a cyclic subgroup in modular Artin induction. The same theorem covers characteristic zero, p = 0, where it takes D = C and the multiplicity is one.

The class computation uses TauCeti.exactK0_asModule_eq_finrank_nsmul_of_forall_pow_eq_one; the cyclic subgroup is supplied by TauCeti.exists_coprimePart_of_isCyclic.

References

• J. Neukirch, A. Schmidt, K. Wingberg, Cohomology of Number Fields, 2nd ed., §VII.3, (7.3.4).
• J.-P. Serre, Linear Representations of Finite Groups, Part III, §14.

theorem TauCeti.exactK0_ofMulAction_quotient_eq_index_nsmul {k G : Type u} [Field k] [Group G] (p : ℕ) [Fact (Nat.Prime p)] [CharP k p] [Finite G] (D : Subgroup G) [D.Normal] (hpow : ∀ (g : G), ∃ (n : ℕ), g ^ p ^ n ∈ D) : ExactK0.of ↧(Representation.ofMulAction k G (G ⧸ D)).asModule = D.index • ExactK0.of ↧(Representation.trivial k G k).asModule

A normal quotient of p-power exponent has permutation class equal to its cardinality times the trivial class, in the exact Grothendieck group of the original group.

theorem TauCeti.exists_coprimePart_exactK0_ofMulAction_eq_nsmul {k G : Type u} [Field k] [Group G] (p : ℕ) [CharP k p] (C : Subgroup G) [Finite ↥C] [IsCyclic ↥C] : ∃ D ≤ C, (D.subgroupOf C).Normal ∧ ¬p ∣ Nat.card ↥D ∧ D.relIndex C = p ^ (Nat.card ↥C).factorization p ∧ ExactK0.of ↧(Representation.ofMulAction k (↥C) (↥C ⧸ D.subgroupOf C)).asModule = p ^ (Nat.card ↥C).factorization p • ExactK0.of ↧(Representation.trivial k (↥C) k).asModule

A finite cyclic subgroup has a subgroup of order prime to p whose coset permutation module, as a module for the cyclic subgroup, has class equal to the p-part of its order times the trivial class. In characteristic zero, p = 0, the subgroup is the whole group, the coset space is a point and the multiplicity is one.

theorem TauCeti.indK0_of_trivial_eq_relIndex_nsmul {k G : Type u} [Field k] [Group G] (p : ℕ) [Fact (Nat.Prime p)] [CharP k p] [Finite G] {C D : Subgroup G} (h : D ≤ C) [(D.subgroupOf C).Normal] (hpow : ∀ c ∈ C, ∃ (n : ℕ), c ^ p ^ n ∈ D) : (indK0 k D) (ExactK0.of ↧(Representation.trivial k (↥D) k).asModule) = D.relIndex C • (indK0 k C) (ExactK0.of ↧(Representation.trivial k (↥C) k).asModule)

Inducing across a quotient of p-power exponent. Let D ≤ C be subgroups of a finite group G, with D normal in C and every element of C having a p-power power in D. Then inducing the trivial line from D gives [C : D] times the class induced from C: [Ind_D^G k] = [C : D] • [Ind_C^G k] in the exact Grothendieck group of G.

theorem TauCeti.exists_coprimePart_indK0_of_trivial_eq_nsmul {k G : Type u} [Field k] [Group G] (p : ℕ) [CharP k p] [Finite G] (C : Subgroup G) [IsCyclic ↥C] : ∃ D ≤ C, ¬p ∣ Nat.card ↥D ∧ D.relIndex C = p ^ (Nat.card ↥C).factorization p ∧ (indK0 k D) (ExactK0.of ↧(Representation.trivial k (↥D) k).asModule) = p ^ (Nat.card ↥C).factorization p • (indK0 k C) (ExactK0.of ↧(Representation.trivial k (↥C) k).asModule)

Let k have characteristic p. A finite cyclic subgroup C has a subgroup D with p ∤ |D| such that inducing the trivial line from D gives p ^ v_p(|C|) times the class induced from C. For prime p, D is the subgroup of C of order prime to p and the multiplicity is the p-part of |C|. In characteristic zero, p = 0, one takes D = C, and the multiplicity is one.