Removing the prime part of cyclic induction in the exact Grothendieck ring

In characteristic p, let D ≤ C ≤ G, with D normal in C and C/D of p-power exponent. The permutation-class identity TauCeti.indK0_of_trivial_eq_relIndex_nsmul and the projection formula give

Ind_D^G Res_D^G x = [C : D] • Ind_C^G Res_C^G x

for every class x in G₀(k[G]). In particular, when C is cyclic, its subgroup D of order prime to p replaces the term |C| • Ind_C^G Res_C^G x by |D| • Ind_D^G Res_D^G x, including for nonsplit representations.

The final theorem rewrites the full Artin coefficient sum as a finite integral linear combination of induction terms from cyclic subgroups of order prime to p. The coefficients work simultaneously for all x. This is the prime-part removal in modular Artin induction; the equality of the Artin sum with |G| • x is a separate input.

Main results

• TauCeti.indK0_resK0_eq_relIndex_nsmul: removal across a normal quotient of p-power exponent.
• Subgroup.exists_coprimePart_natCard_nsmul_indK0_resK0: the coefficient identity for a cyclic subgroup and its prime-to-p part.
• TauCeti.exists_linearCombination_indK0_resK0_eq_sum_artinCoeff: the full Artin sum uses only cyclic subgroups of order prime to p.

References

• J. Neukirch, A. Schmidt, K. Wingberg, Cohomology of Number Fields, second edition, §VII.3, (7.3.4).
• J.-P. Serre, Linear Representations of Finite Groups, Part II, §9.2.

theorem TauCeti.indK0_resK0_eq_relIndex_nsmul {k G : Type u} [Field k] [Group G] [Finite G] (p : ℕ) [Fact (Nat.Prime p)] [CharP k p] {C D : Subgroup G} (h : D ≤ C) [(D.subgroupOf C).Normal] (hpow : ∀ c ∈ C, ∃ (n : ℕ), c ^ p ^ n ∈ D) (x : ExactK0 (finiteModulesExactStructure (MonoidAlgebra k G))) : (indK0 k D) ((resK0 k D.subtype) x) = D.relIndex C • (indK0 k C) ((resK0 k C.subtype) x)

Across a normal quotient of p-power exponent, inducing a restricted class from the smaller subgroup multiplies induction from the larger subgroup by their relative index.

theorem Subgroup.exists_coprimePart_natCard_nsmul_indK0_resK0 {k G : Type u} [Field k] [Group G] [Finite G] {p : ℕ} [Fact (Nat.Prime p)] [CharP k p] (C : Subgroup G) [IsCyclic ↥C] : ∃ D ≤ C, IsCyclic ↥D ∧ ¬p ∣ Nat.card ↥D ∧ D.relIndex C = p ^ (Nat.card ↥C).factorization p ∧ ∀ (x : TauCeti.ExactK0 (TauCeti.finiteModulesExactStructure (MonoidAlgebra k G))), Nat.card ↥C • (TauCeti.indK0 k C) ((TauCeti.resK0 k C.subtype) x) = Nat.card ↥D • (TauCeti.indK0 k D) ((TauCeti.resK0 k D.subtype) x)

For a finite cyclic subgroup C, its prime-to-p part D removes the p-part of the coefficient |C| in every induced restriction, uniformly in the Grothendieck class.

theorem TauCeti.exists_linearCombination_indK0_resK0_eq_sum_artinCoeff {k G : Type u} [Field k] [Group G] [Finite G] (p : ℕ) [Fact (Nat.Prime p)] [CharP k p] : ∃ (a : { D : Subgroup G // IsCyclic ↥D ∧ ¬p ∣ Nat.card ↥D } →₀ ℤ), ∀ (x : ExactK0 (finiteModulesExactStructure (MonoidAlgebra k G))), (Finsupp.linearCombination ℤ fun (D : { D : Subgroup G // IsCyclic ↥D ∧ ¬p ∣ Nat.card ↥D }) => (indK0 k ↑D) ((resK0 k (↑D).subtype) x)) a = ∑ᶠ (C : Subgroup G), (C.artinCoeff * ↑(Nat.card ↥C)) • (indK0 k C) ((resK0 k C.subtype) x)

The Artin coefficient sum is an integral linear combination of induced restrictions from cyclic subgroups of order prime to the characteristic. A single finitely supported coefficient family gives the identity for every class in the exact Grothendieck ring.