Projectivity of the conjugation Hom representation

Let k be a commutative semiring, G a finite group, ρ a representation of G on V and σ a representation of G on W. The k-linear maps V → W carry the conjugation action g • φ = σ g ∘ φ ∘ ρ g⁻¹ (Mathlib's Representation.linHom). This file proves that when ρ.asModule is a finitely generated projective k[G]-module and W is projective over k, the conjugation module Hom_k(V, W) is a projective k[G]-module. It also records that Hom_k(V, W) is a finitely generated k[G]-module whenever V is finitely generated and projective and W is finitely generated over k.

For the regular representation the conjugation module is induced: Hom_k(k[G], W) is identified with k[G]^* ⊗ W by the contraction map, the dual of k[G] with k[G] by the coefficient pairing (Representation.dualLeftRegularEquiv), and the diagonal action on k[G] ⊗ W with the action on the first factor alone (Representation.leftRegularTensorEquivTrivial). This exhibits Hom_k(k[G], W) as the base change k[G] ⊗[k] W. A finitely generated projective k[G]-module is a direct summand of some k[G]ⁿ, and precomposition with the inclusion and projection makes Hom_k(V, W) a direct summand of Hom_k(k[G], W)ⁿ.

Over a field k of characteristic p this says that Hom_k(P, S) is a projective k[G]-module for every finitely generated projective k[G]-module P and every k[G]-module S. In Brauer's theory of modular characters this is what lets Hom_{k[G]}(P, S) = Hom_k(P, S)^G be studied through the invariants of a projective module, whose dimension is computed by characters after lifting to characteristic zero.

Main results

• Representation.Equiv.dualTensorHomOfProjective: for V finitely generated and projective over k, the contraction V^* ⊗ W ≃ Hom_k(V, W) is an equivalence of representations.
• Representation.nonempty_linHom_leftRegular_asModule_linearEquiv: the conjugation module Hom_k(k[G], W) is isomorphic to k[G] ⊗[k] W.
• Representation.instProjectiveAsModuleLinHom: Hom_k(V, W) is a projective k[G]-module.
• Representation.instFiniteAsModuleLinHom: Hom_k(V, W) is a finitely generated k[G]-module when V is finite projective and W is finite over k.

References

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

noncomputable def Representation.Equiv.dualTensorHomOfProjective {k : Type u} [CommSemiring k] {G : Type v} [Group G] {V : Type w} [AddCommMonoid V] [Module k V] {W : Type w'} [AddCommMonoid W] [Module k W] [Module.Finite k V] [Module.Projective k V] (ρ : Representation k G V) (σ : Representation k G W) : (ρ.dual.tprod σ).Equiv (ρ.linHom σ)

The contraction V^* ⊗ W ≃ Hom_k(V, W) as an equivalence of representations, for V finitely generated and projective over the commutative semiring k. It intertwines the tensor product of the dual of ρ with σ and the conjugation representation linHom ρ σ. This generalizes Mathlib's Representation.Equiv.dualTensorHom, which is stated for finite-dimensional vector spaces over a field.

@[simp]

theorem Representation.Equiv.dualTensorHomOfProjective_apply {k : Type u} [CommSemiring k] {G : Type v} [Group G] {V : Type w} [AddCommMonoid V] [Module k V] {W : Type w'} [AddCommMonoid W] [Module k W] [Module.Finite k V] [Module.Projective k V] (ρ : Representation k G V) (σ : Representation k G W) (x : TensorProduct k (Module.Dual k V) W) : (dualTensorHomOfProjective ρ σ) x = (_root_.dualTensorHom k V W) x

theorem Representation.nonempty_linHom_leftRegular_asModule_linearEquiv {k : Type u} [CommSemiring k] {G : Type v} [Group G] {W : Type w'} [AddCommMonoid W] [Module k W] (σ : Representation k G W) [Finite G] : Nonempty (((leftRegular k G).linHom σ).asModule ≃ₗ[MonoidAlgebra k G] TensorProduct k (MonoidAlgebra k G) W)

The coinduced module Hom_k(k[G], W) is the induced module k[G] ⊗[k] W. For a finite group G and any representation σ of G on W, the conjugation module of k-linear maps from the regular representation to σ is isomorphic to the base change k[G] ⊗[k] W, on which k[G] acts on the first factor.

instance Representation.instFiniteAsModuleLinHom {k : Type u} [CommSemiring k] {G : Type v} [Group G] {V : Type w} [AddCommMonoid V] [Module k V] {W : Type w'} [AddCommMonoid W] [Module k W] (σ : Representation k G W) (ρ : Representation k G V) [Module.Finite k V] [Module.Projective k V] [Module.Finite k W] : Module.Finite (MonoidAlgebra k G) (ρ.linHom σ).asModule

If V is finitely generated and projective over k and W is finitely generated over k, then the conjugation module Hom_k(V, W) is a finitely generated k[G]-module.

instance Representation.instProjectiveAsModuleLinHom {k : Type u} [CommSemiring k] {G : Type v} [Group G] {V : Type w} [AddCommMonoid V] [Module k V] {W : Type w'} [AddCommMonoid W] [Module k W] (σ : Representation k G W) (ρ : Representation k G V) [Finite G] [Module.Finite (MonoidAlgebra k G) ρ.asModule] [Module.Projective (MonoidAlgebra k G) ρ.asModule] [Module.Projective k W] : Module.Projective (MonoidAlgebra k G) (ρ.linHom σ).asModule

The conjugation module of a projective module is projective. For a finite group G, if ρ.asModule is a finitely generated projective k[G]-module and W is projective over k, then the conjugation module Hom_k(V, W) is a projective k[G]-module.