Tensor-invariant dimensions of lines and of the regular representation

Let G be a finite group and k a field in which #G is nonzero. This file evaluates the tensor-invariant dimension TauCeti.finrankTensorInvariantsK0 A, [M] ↦ dimₖ (M ⊗ A)ᴳ, on the two kinds of classes that occur in the Grothendieck-group computation of local Galois cohomology:

• for a one-dimensional representation M, the line M^∨ ⊗ M is trivial (Representation.dualTprodEquivTrivial), so [M^∨] * [M] = 1 in G₀(k[G]) (TauCeti.fdRepK0RingEquiv_dual_mul_self_eq_one);
• the regular representation k[G] is induced from the trivial subgroup, so by the projection formula and Frobenius reciprocity dimₖ (k[G] ⊗ V)ᴳ = dimₖ V (TauCeti.finrankInvariantsK0_permK0_self_mul).

Together they give TauCeti.finrankTensorInvariantsK0_dual_mul_one_add_add: for a line M and c : ℕ, the class [M^∨] * (1 + [M] + c [k[G]]) has tensor-invariant dimension dim (M^∨ ⊗ A)ᴳ + dim Aᴳ + c dim A. With M = μ_ℓ, this is the final count in the proof of Tate's local Euler characteristic formula, where H¹(L, 𝔽_ℓ) has the class [μ_ℓ^∨] * [Lˣ/(Lˣ)^ℓ] and [Lˣ/(Lˣ)^ℓ] = 1 + [μ_ℓ] + [ℓ = p] [K : ℚ_p] [k[G]].

References

• J. Neukirch, A. Schmidt, K. Wingberg, Cohomology of Number Fields, 2nd ed., proof of (7.3.1).
• J. S. Milne, Arithmetic Duality Theorems, 2nd ed., I, proof of Theorem 2.8.

theorem TauCeti.fdRepK0RingEquiv_dual_mul_self_eq_one {k G : Type u} [Field k] [Group G] [Finite G] (M : FDRep k G) (h : Module.finrank k ↑M.V = 1) : (fdRepK0RingEquiv k G) (ExactK0.of (FDRep.of (Representation.dual M.ρ))) * (fdRepK0RingEquiv k G) (ExactK0.of M) = 1

[M^∨] * [M] = 1 for a line. In G₀(k[G]), the class of the dual of a one-dimensional representation is inverse to the class of the representation.

theorem TauCeti.finrankInvariantsK0_permK0_self_mul {k G : Type u} [Field k] [Group G] [Finite G] [NeZero ↑(Nat.card G)] (V : FDRep k G) : finrankInvariantsK0 (permK0 k G G * (fdRepK0RingEquiv k G) (ExactK0.of V)) = ↑(Module.finrank k ↑V.V)

The regular representation absorbs invariants. Tensoring with the regular representation k[G] and taking invariants gives back the dimension: dimₖ (k[G] ⊗ V)ᴳ = dimₖ V. Indeed k[G] is induced from the trivial subgroup, so by the projection formula k[G] ⊗ V is induced from the restriction of V to the trivial subgroup, whose invariants are all of V.

theorem TauCeti.finrankTensorInvariantsK0_dual_mul_one_add_add {k G : Type u} [Field k] [Group G] [Finite G] [NeZero ↑(Nat.card G)] (M A : FDRep k G) (hM : Module.finrank k ↑M.V = 1) (c : ℕ) : (finrankTensorInvariantsK0 A) ((fdRepK0RingEquiv k G) (ExactK0.of (FDRep.of (Representation.dual M.ρ))) * (1 + (fdRepK0RingEquiv k G) (ExactK0.of M) + c • permK0 k G G)) = ↑(Module.finrank k ↥((Representation.dual M.ρ).tprod A.ρ).invariants) + ↑(Module.finrank k ↥(Representation.invariants A.ρ)) + ↑c * ↑(Module.finrank k ↑A.V)

The tensor-invariant dimension of [M^∨] * (1 + [M] + c [k[G]]) for a line M: it is dimₖ (M^∨ ⊗ A)ᴳ + dimₖ Aᴳ + c dimₖ A. The three terms come from [M^∨] * 1 = [M^∨], from [M^∨] * [M] = 1 (TauCeti.fdRepK0RingEquiv_dual_mul_self_eq_one), and from the regular representation (TauCeti.finrankInvariantsK0_permK0_self_mul).