Artin's identity in the exact Grothendieck ring

For a finite group G, let a_C = C.artinCoeff * |C|. The two actual G-sets TauCeti.ArtinPositiveSet G and TauCeti.ArtinNegativeSet G split the positive and negative parts of the coefficients a_C. Their fixed-point counts agree, so the permutation-class comparison identifies their classes in G₀(k[G]) over every field, including when the characteristic divides |G|. Expanding the two disjoint unions and recombining the positive and negative parts gives

|G| [k] = ∑ᶠ C, a_C [k[G/C]].

Rewriting the coset classes as induced units gives Artin's identity in the Grothendieck ring. The projection formula then gives the identity for every virtual class by multiplication.

Main results

• TauCeti.permK0_artinPositiveSet and TauCeti.permK0_artinNegativeSet: expansion of the two Artin permutation classes.
• TauCeti.permK0_artinPositiveSet_eq_artinNegativeSet: their classes agree over every field.
• TauCeti.natCard_nsmul_permK0_quotient_top_eq_sum_artinCoeff: the signed permutation-class identity.
• TauCeti.natCard_nsmul_one_eq_sum_artinCoeff_indK0: Artin's identity written with induction from subgroups.
• TauCeti.natCard_nsmul_eq_sum_artinCoeff_indK0_resK0: the identity for every virtual class.

References

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

theorem TauCeti.permK0_artinPositiveSet (k G : Type u) [CommRing k] [Group G] [Finite G] : permK0 k G (ArtinPositiveSet G) = ∑ᶠ (C : Subgroup G), (C.artinCoeff * ↑(Nat.card ↥C)).toNat • permK0 k G (G ⧸ C)

The class of the positive Artin set is the sum of the positive parts of the Artin coefficients times the corresponding coset classes.

theorem TauCeti.permK0_artinNegativeSet (k G : Type u) [CommRing k] [Group G] [Finite G] : permK0 k G (ArtinNegativeSet G) = Nat.card G • permK0 k G (G ⧸ ⊤) + ∑ᶠ (C : Subgroup G), (-(C.artinCoeff * ↑(Nat.card ↥C))).toNat • permK0 k G (G ⧸ C)

The class of the negative Artin set is the sum of |G| fixed points and the negative parts of the Artin coefficients times the corresponding coset classes.

theorem TauCeti.permK0_artinPositiveSet_eq_artinNegativeSet (k G : Type u) [Field k] [Group G] [Finite G] : permK0 k G (ArtinPositiveSet G) = permK0 k G (ArtinNegativeSet G)

The positive and negative Artin sets have equal permutation classes over every field.

theorem TauCeti.natCard_nsmul_permK0_quotient_top_eq_sum_artinCoeff (k G : Type u) [Field k] [Group G] [Finite G] : Nat.card G • permK0 k G (G ⧸ ⊤) = ∑ᶠ (C : Subgroup G), (C.artinCoeff * ↑(Nat.card ↥C)) • permK0 k G (G ⧸ C)

Artin's signed permutation identity in the exact Grothendieck group over every field.

theorem TauCeti.natCard_nsmul_one_eq_sum_artinCoeff_indK0 (k G : Type u) [Field k] [Group G] [Finite G] : Nat.card G • 1 = ∑ᶠ (C : Subgroup G), (C.artinCoeff * ↑(Nat.card ↥C)) • (indK0 k C) 1

Artin's identity in G₀(k[G]) over every field, written as induction of the unit from subgroups. No division by the group order is required.

theorem TauCeti.natCard_nsmul_eq_sum_artinCoeff_indK0_resK0 (k G : Type u) [Field k] [Group G] [Finite G] (x : ExactK0 (finiteModulesExactStructure (MonoidAlgebra k G))) : Nat.card G • x = ∑ᶠ (C : Subgroup G), (C.artinCoeff * ↑(Nat.card ↥C)) • (indK0 k C) ((resK0 k C.subtype) x)

Artin's induction identity for every virtual class over every field. Multiplying by |G| expresses a class as the Artin-coefficient sum of its induced restrictions.