Artin's identity as an equivalence of permutation representations

For a finite group G, put a_C = C.artinCoeff * |C|. Artin's identity says that ∑ C, a_C * |(G/C)^g| = |G| for every g. Splitting each integer coefficient into its positive and negative parts gives two actual finite G-sets:

• ArtinPositiveSet G has max a_C 0 copies of G/C for each subgroup C;
• ArtinNegativeSet G has |G| fixed points and max (-a_C) 0 copies of G/C.

These sets have equal fixed-point counts, hence equivalent permutation representations over every field of characteristic zero. In particular their integral permutation lattices become isomorphic over ℚ. This turns the signed character identity into an isomorphism to which lattice-reduction arguments can apply, even when the residue characteristic divides |G|. Only cyclic subgroups contribute copies, since every other Artin coefficient vanishes.

The fixed-point calculation uses sum_artinCoeff_mul_card_fixedBy. The criterion nonempty_equiv_ofMulAction_iff_forall_natCard_fixedBy_eq supplies the representation equivalence, and baseChangeComapEquiv identifies the rationalizations with those representations.

The actions use Mathlib's fiberwise actions on sigma types and sums: they leave the subgroup and copy index fixed and translate the coset. The fixed points in ArtinNegativeSet are represented by copies of G/⊤, so no extra trivial-action instance is needed. The equivariant equivalences artinPositiveSetEquiv and artinNegativeSetEquiv expose these decompositions while leaving the noncomputable action instances opaque.

References

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

def TauCeti.ArtinPositiveSet (G : Type u) [Group G] [Finite G] : Type u

The disjoint union of the positive terms of Artin's permutation identity. A point records a subgroup, a copy index, and a left coset of that subgroup.

instance TauCeti.instFiniteArtinPositiveSet (G : Type u) [Group G] [Finite G] : Finite (ArtinPositiveSet G)

@[instance_reducible]

noncomputable instance TauCeti.instMulActionArtinPositiveSet (G : Type u) [Group G] [Finite G] : MulAction G (ArtinPositiveSet G)

def TauCeti.ArtinNegativeSet (G : Type u) [Group G] [Finite G] : Type u

The disjoint union of the negative terms of Artin's permutation identity, together with |G| fixed points. The fixed points are copies of the singleton coset space G/⊤.

instance TauCeti.instFiniteArtinNegativeSet (G : Type u) [Group G] [Finite G] : Finite (ArtinNegativeSet G)

@[instance_reducible]

noncomputable instance TauCeti.instMulActionArtinNegativeSet (G : Type u) [Group G] [Finite G] : MulAction G (ArtinNegativeSet G)

noncomputable def TauCeti.artinPositiveSetEquiv (G : Type u) [Group G] [Finite G] : ArtinPositiveSet G ≃ (C : Subgroup G) × (_ : Fin (C.artinCoeff * ↑(Nat.card ↥C)).toNat) × G ⧸ C

The positive Artin set as its defining sigma type. This equivalence exposes the decomposition without exposing the noncomputable action instance on ArtinPositiveSet.

theorem TauCeti.artinPositiveSetEquiv_smul (G : Type u) [Group G] [Finite G] (g : G) (x : ArtinPositiveSet G) : (artinPositiveSetEquiv G) (g • x) = g • (artinPositiveSetEquiv G) x

TauCeti.artinPositiveSetEquiv is equivariant for the fiberwise action.

noncomputable def TauCeti.artinNegativeSetEquiv (G : Type u) [Group G] [Finite G] : ArtinNegativeSet G ≃ (_ : Fin (Nat.card G)) × G ⧸ ⊤ ⊕ (C : Subgroup G) × (_ : Fin (-(C.artinCoeff * ↑(Nat.card ↥C))).toNat) × G ⧸ C

The negative Artin set as the sum of its fixed-point and negative-coefficient sigma types. This equivalence exposes the decomposition without exposing its noncomputable action instance.

theorem TauCeti.artinNegativeSetEquiv_smul (G : Type u) [Group G] [Finite G] (g : G) (x : ArtinNegativeSet G) : (artinNegativeSetEquiv G) (g • x) = g • (artinNegativeSetEquiv G) x

TauCeti.artinNegativeSetEquiv is equivariant for the fiberwise action.

theorem TauCeti.card_fixedBy_artinPositiveSet {G : Type u} [Group G] [Finite G] (g : G) : Nat.card ↑(MulAction.fixedBy (ArtinPositiveSet G) g) = ∑ᶠ (C : Subgroup G), (C.artinCoeff * ↑(Nat.card ↥C)).toNat * Nat.card ↑(MulAction.fixedBy (G ⧸ C) g)

The fixed-point count of the positive Artin set, with its multiplicities explicit.

@[simp]

theorem TauCeti.ncard_fixedBy_artinPositiveSet {G : Type u} [Group G] [Finite G] (g : G) : (MulAction.fixedBy (ArtinPositiveSet G) g).ncard = ∑ᶠ (C : Subgroup G), (C.artinCoeff * ↑(Nat.card ↥C)).toNat * (MulAction.fixedBy (G ⧸ C) g).ncard

The positive Artin fixed-point count with explicit multiplicities, in simp normal form.

theorem TauCeti.card_fixedBy_artinNegativeSet {G : Type u} [Group G] [Finite G] (g : G) : Nat.card ↑(MulAction.fixedBy (ArtinNegativeSet G) g) = Nat.card G + ∑ᶠ (C : Subgroup G), (-(C.artinCoeff * ↑(Nat.card ↥C))).toNat * Nat.card ↑(MulAction.fixedBy (G ⧸ C) g)

The fixed-point count of the negative Artin set includes the |G| fixed points.

@[simp]

theorem TauCeti.ncard_fixedBy_artinNegativeSet {G : Type u} [Group G] [Finite G] (g : G) : (MulAction.fixedBy (ArtinNegativeSet G) g).ncard = Nat.card G + ∑ᶠ (C : Subgroup G), (-(C.artinCoeff * ↑(Nat.card ↥C))).toNat * (MulAction.fixedBy (G ⧸ C) g).ncard

The negative Artin fixed-point count including the fixed points, in simp normal form.

theorem TauCeti.card_fixedBy_artinPositiveSet_eq_card_fixedBy_artinNegativeSet {G : Type u} [Group G] [Finite G] (g : G) : Nat.card ↑(MulAction.fixedBy (ArtinPositiveSet G) g) = Nat.card ↑(MulAction.fixedBy (ArtinNegativeSet G) g)

The two sides of Artin's permutation identity have the same fixed-point counts.

theorem TauCeti.nonempty_equiv_artinPermutationRepresentations (G : Type u) [Group G] [Finite G] (k : Type v) [Field k] [CharZero k] : Nonempty ((Representation.ofMulAction k G (ArtinPositiveSet G)).Equiv (Representation.ofMulAction k G (ArtinNegativeSet G)))

Artin's signed permutation identity is an equivalence of actual representations over any characteristic-zero field. In particular, at k = ℚ it gives the rational isomorphism needed to compare the reductions of the two integral permutation lattices.

theorem TauCeti.nonempty_equiv_rationalized_artinPermutationLattices (G : Type u) [Group G] [Finite G] : Nonempty ((Representation.baseChange ℚ (Representation.ofDistribMulAction ℤ G (ArtinPositiveSet G →₀ ℤ))).Equiv (Representation.baseChange ℚ (Representation.ofDistribMulAction ℤ G (ArtinNegativeSet G →₀ ℤ))))

The two integral permutation lattices in Artin's identity have isomorphic rationalizations. The integral lattices themselves need not be isomorphic.