Untwisting a regular tensor representation

Let G be a group, k a commutative semiring, and S a k-linear representation of G. The diagonal action on k[G] ⊗ S is equivalent to the action on the regular factor alone. The equivalence sends

g ⊗ s ↦ g ⊗ g⁻¹s.

This Hopf-module calculation is the structural input for proving that the conjugation module Hom_k(P, S) is projective when P is finitely generated projective over a finite group algebra. That projectivity, in turn, is needed in Swan's rational detection theorem for projective \mathbb Z_p[G]-lattices.

Main results

• Representation.leftRegularTensorEquivTrivial: untwists the diagonal action on k[G] ⊗ S to the action on the regular factor alone.
• Representation.dualLeftRegularEquiv: identifies the regular representation of a finite group with its dual.

References

• J.-P. Serre, Linear Representations of Finite Groups, Part III, §14–16.
• R. G. Swan, Induced representations and projective modules, Ann. of Math. 71 (1960).

noncomputable def Representation.leftRegularTensorEquivTrivial {k : Type u} [CommSemiring k] {G : Type v} [Group G] {W : Type w} [AddCommMonoid W] [Module k W] (σ : Representation k G W) : ((leftRegular k G).tprod σ).Equiv ((leftRegular k G).tprod (trivial k G W))

Untwisting the regular tensor factor. The diagonal action on k[G] ⊗ S is equivalent to the action on the regular factor alone. On pure tensors the equivalence is g ⊗ s ↦ g ⊗ g⁻¹s.

No finiteness hypothesis on G or S is needed.

@[simp]

theorem Representation.leftRegularTensorEquivTrivial_apply_single_tmul {k : Type u} [CommSemiring k] {G : Type v} [Group G] {W : Type w} [AddCommMonoid W] [Module k W] (σ : Representation k G W) (g : G) (r : k) (w : W) : σ.leftRegularTensorEquivTrivial (MonoidAlgebra.single g r ⊗ₜ[k] w) = MonoidAlgebra.single g r ⊗ₜ[k] (σ g⁻¹) w

Untwisting sends g ⊗ s to g ⊗ g⁻¹s.

@[simp]

theorem Representation.leftRegularTensorEquivTrivial_symm_apply_single_tmul {k : Type u} [CommSemiring k] {G : Type v} [Group G] {W : Type w} [AddCommMonoid W] [Module k W] (σ : Representation k G W) (g : G) (r : k) (w : W) : σ.leftRegularTensorEquivTrivial.symm (MonoidAlgebra.single g r ⊗ₜ[k] w) = MonoidAlgebra.single g r ⊗ₜ[k] (σ g) w

The inverse of untwisting sends g ⊗ s to g ⊗ gs.

noncomputable def Representation.dualLeftRegularEquiv {k : Type u} [CommSemiring k] {G : Type v} [Group G] [Finite G] : (leftRegular k G).dual.Equiv (leftRegular k G)

The regular representation is self-dual. The coefficient pairing identifies the dual of the left regular representation with the left regular representation.

@[simp]

theorem Representation.dualLeftRegularEquiv_apply_coeff {k : Type u} [CommSemiring k] {G : Type v} [Group G] [Finite G] (f : Module.Dual k (MonoidAlgebra k G)) (g : G) : (dualLeftRegularEquiv f).coeff g = f (MonoidAlgebra.single g 1)

Under regular self-duality, the coefficient at g is evaluation on the basis vector g.

@[simp]

theorem Representation.dualLeftRegularEquiv_symm_apply_single {k : Type u} [CommSemiring k] {G : Type v} [Group G] [Finite G] (x : MonoidAlgebra k G) (g : G) : (dualLeftRegularEquiv.symm x) (MonoidAlgebra.single g 1) = x.coeff g

The inverse of regular self-duality evaluates on the basis vector g as the coefficient at g.