Modular Artin induction with uniform coefficients

For a finite group G and a field of prime characteristic p, multiplication by |G| on G₀(k[G]) is a finite integral linear combination of induction after restriction from cyclic subgroups of order prime to p. One coefficient family works for every virtual class.

This combines Artin's identity over every field with the removal of the prime part of cyclic subgroups. In particular, it applies when p divides |G|, without semisimplicity or a splitting-field hypothesis, and expresses every group-order multiple in the subgroup generated by such induced classes.

Main results

• TauCeti.exists_linearCombination_indK0_resK0_eq_natCard_nsmul: the uniform integral coefficient family.
• TauCeti.modularArtin_natCard_nsmul_mem_indCyclicCoprimeK0: |G| • x lies in TauCeti.indCyclicCoprimeK0, the subgroup generated by induction from cyclic subgroups of order prime to the characteristic.
• TauCeti.modularArtin_exists_nsmul_mem_indCyclicCoprimeK0: every class has a positive multiple in that subgroup.
• TauCeti.eq_of_comp_indK0_eq_of_cyclic_coprime: two homomorphisms from G₀(k[G]) to a torsion-free group agree once they agree after induction from every cyclic subgroup of order prime to the characteristic.

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.
• J. S. Milne, Arithmetic Duality Theorems, second edition, Chapter I, Lemma 2.10.

theorem TauCeti.exists_linearCombination_indK0_resK0_eq_natCard_nsmul {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 = Nat.card G • x

Modular Artin induction. A single finitely supported integral coefficient family over cyclic subgroups of order prime to p expresses |G| times every virtual class as a sum of its induced restrictions.

theorem TauCeti.modularArtin_natCard_nsmul_mem_indCyclicCoprimeK0 {k G : Type u} [Field k] [Group G] [Finite G] (p : ℕ) [Fact (Nat.Prime p)] [CharP k p] (x : ExactK0 (finiteModulesExactStructure (MonoidAlgebra k G))) : Nat.card G • x ∈ indCyclicCoprimeK0 k G p

The modular Artin theorem with multiplier |G|. In characteristic p, the group-order multiple of every class in G₀(k[G]) lies in TauCeti.indCyclicCoprimeK0, the subgroup generated by the classes induced from cyclic subgroups of order prime to p; for the prime p, order prime to p is non-divisibility of the order by p (Nat.Prime.coprime_iff_not_dvd).

theorem TauCeti.modularArtin_exists_nsmul_mem_indCyclicCoprimeK0 {k G : Type u} [Field k] [Group G] [Finite G] (p : ℕ) [Fact (Nat.Prime p)] [CharP k p] (x : ExactK0 (finiteModulesExactStructure (MonoidAlgebra k G))) : ∃ (N : ℕ), 0 < N ∧ N • x ∈ indCyclicCoprimeK0 k G p

The modular Artin induction theorem (NSW (7.3.4), Milne ADT I Lemma 2.10). In characteristic p, every class in G₀(k[G]) has a positive multiple in TauCeti.indCyclicCoprimeK0, the subgroup generated by the classes induced from cyclic subgroups of order prime to p; the multiplier |G| works for every class.

theorem TauCeti.eq_of_comp_indK0_eq_of_cyclic_coprime {k G : Type u} [Field k] [Group G] [Finite G] (p : ℕ) [Fact (Nat.Prime p)] [CharP k p] {M : Type u_1} [AddCommGroup M] [IsAddTorsionFree M] {f g : ExactK0 (finiteModulesExactStructure (MonoidAlgebra k G)) →+ M} (h : ∀ (D : Subgroup G), IsCyclic ↥D ∧ ¬p ∣ Nat.card ↥D → f.comp (indK0 k D) = g.comp (indK0 k D)) : f = g

Equality from modular Artin induction. Two additive invariants of modular representation classes with values in a torsion-free group agree if they agree after induction from every cyclic subgroup whose order is prime to the characteristic.