Invariant dimensions on the Grothendieck group of a group algebra

Let G be a finite group and k a field whose characteristic does not divide #G. Maschke's theorem makes the invariants functor exact, so the dimension of the invariant subspace is additive in short exact sequences of finite-dimensional representations (FDRep.finrank_invariants_add_of_shortExact). This file descends that dimension to a homomorphism

finrankInvariantsK0 k G : G₀(k[G]) →+ ℤ.

The Grothendieck ring product is induced by the tensor product of representations. Hence, for a fixed finite-dimensional representation A, multiplication by [A] followed by invariant dimension gives another additive homomorphism,

finrankTensorInvariantsK0 A : G₀(k[G]) →+ ℤ,

whose value at [M] is dimₖ (M ⊗ A)^G. This packages the semisimple representation-theoretic functional used in Euler characteristic calculations.

Induction from a subgroup S does not change invariant dimension (FDRep.finrank_invariants_indFDRep), so finrankInvariantsK0 is unchanged by induction on Grothendieck groups (finrankInvariantsK0_indK0).

References

• J.-P. Serre, Linear Representations of Finite Groups, Springer GTM 42 (1977), §§1.4 and 14.1.

noncomputable def TauCeti.finrankInvariantsK0 {k G : Type u} [Field k] [Group G] [Finite G] [NeZero ↑(Nat.card G)] : ExactK0 (finiteModulesExactStructure (MonoidAlgebra k G)) →+ ℤ

Invariant dimension on the group-algebra Grothendieck group. When #G is nonzero in k, this homomorphism sends the class of a finite-dimensional representation V to dimₖ(Vᴳ).

@[simp]

theorem TauCeti.finrankInvariantsK0_of {k G : Type u} [Field k] [Group G] [Finite G] [NeZero ↑(Nat.card G)] (V : FDRep k G) : finrankInvariantsK0 (ExactK0.of ↧(Representation.asModule V.ρ)) = ↑(Module.finrank k ↥(Representation.invariants V.ρ))

The invariant-dimension homomorphism evaluates on the class of the group-algebra module of a representation V as the dimension of the invariant subspace of V.

noncomputable def TauCeti.finrankTensorInvariantsK0 {k G : Type u} [Field k] [Group G] [Finite G] [NeZero ↑(Nat.card G)] (A : FDRep k G) : ExactK0 (finiteModulesExactStructure (MonoidAlgebra k G)) →+ ℤ

Invariant dimension after tensoring with A. This additive homomorphism sends a class [M] to dimₖ (M ⊗ A)ᴳ.

theorem TauCeti.finrankTensorInvariantsK0_apply {k G : Type u} [Field k] [Group G] [Finite G] [NeZero ↑(Nat.card G)] (A : FDRep k G) (x : ExactK0 (finiteModulesExactStructure (MonoidAlgebra k G))) : (finrankTensorInvariantsK0 A) x = finrankInvariantsK0 (x * (fdRepK0RingEquiv k G) (ExactK0.of A))

finrankTensorInvariantsK0 A is invariant dimension after multiplication by the class of A.

@[simp]

theorem TauCeti.finrankTensorInvariantsK0_of {k G : Type u} [Field k] [Group G] [Finite G] [NeZero ↑(Nat.card G)] (A M : FDRep k G) : (finrankTensorInvariantsK0 A) (ExactK0.of ↧(Representation.asModule M.ρ)) = ↑(Module.finrank k ↥(Representation.invariants (CategoryTheory.MonoidalCategoryStruct.tensorObj M A).ρ))

Evaluating finrankTensorInvariantsK0 A on the class of the group-algebra module of M gives the dimension of the invariants of the tensor product M ⊗ A.

theorem TauCeti.finrankInvariantsK0_indK0 {k G : Type u} [Field k] [Group G] [Finite G] [NeZero ↑(Nat.card G)] (S : Subgroup G) [NeZero ↑(Nat.card ↥S)] (x : ExactK0 (finiteModulesExactStructure (MonoidAlgebra k ↥S))) : finrankInvariantsK0 ((indK0 k S) x) = finrankInvariantsK0 x

Induction preserves invariant dimension on Grothendieck groups. Evaluating invariant dimension after induction from a subgroup gives invariant dimension over that subgroup.