Representations whose identity is a norm

Let ρ be a representation of a finite group G on a k-module V. The group acts on End_k(V) by conjugation (Representation.linHom ρ ρ), and the norm of this action sends φ to x ↦ ∑ g, ρ g (φ (ρ g⁻¹ x)). When the identity of V is such a norm, V is a direct summand of the induced module k[G] ⊗_k V; if moreover V is projective over k, then V is a projective k[G]-module. This is the easy direction of Higman's criterion, and the way the theorem of Nakayama and Rim produces projective modules (Serre, Local Fields, IX §§3–5).

Whether the identity is a norm can be decided one prime divisor of |G| at a time: if for every such prime p some subgroup of index prime to p has the identity as a norm, then so does G.

Main statements

• Representation.norm_linHom_apply: the norm of the action on linear maps between two representations, including conjugation on End_k(V).
• Representation.index_nsmul_id_mem_range_norm_linHom: if the identity is an H-norm, then [G : H] times the identity is a G-norm.
• Representation.id_mem_range_norm_linHom_of_forall_prime: if for every prime divisor p of |G| the identity is a norm for a subgroup of index prime to p, then it is a G-norm.
• Rep.projective_of_id_mem_range_norm_linHom, Rep.moduleProjective_of_id_mem_range_norm_linHom: a representation that is projective over k and whose identity is a norm is projective, in Rep k G and as a k[G]-module.

References

• J.-P. Serre, Local Fields, Chapter IX, §§3–5.
• K. S. Brown, Cohomology of Groups, Chapter VI, §8.

theorem Representation.norm_linHom_apply {k : Type u_1} {G : Type u_2} {V : Type u_3} [CommSemiring k] [Group G] [Fintype G] [AddCommMonoid V] [Module k V] (ρ : Representation k G V) {W : Type u_4} [AddCommMonoid W] [Module k W] (σ : Representation k G W) (φ : V →ₗ[k] W) (x : V) : ((ρ.linHom σ).norm φ) x = ∑ g : G, (σ g) (φ ((ρ g⁻¹) x))

The norm of the action of G on linear maps from ρ to σ sends φ to x ↦ ∑ g, σ g (φ (ρ g⁻¹ x)).

theorem Representation.index_nsmul_id_mem_range_norm_linHom {k : Type u_1} {G : Type u_2} {V : Type u_3} [CommSemiring k] [Group G] [Fintype G] [AddCommMonoid V] [Module k V] (ρ : Representation k G V) (H : Subgroup G) [Fintype ↥H] (h : LinearMap.id ∈ LinearMap.range (norm (MonoidHom.comp (ρ.linHom ρ) H.subtype))) : H.index • LinearMap.id ∈ LinearMap.range (ρ.linHom ρ).norm

If the identity of V is the norm of φ for the conjugation action of a subgroup H, then [G : H] times the identity is the norm of φ for the conjugation action of G.

theorem Representation.id_mem_range_norm_linHom_of_forall_prime {k : Type u_1} {G : Type u_2} {V : Type u_3} [CommSemiring k] [Group G] [Fintype G] [AddCommGroup V] [Module k V] (ρ : Representation k G V) (h : ∀ (p : ℕ), Nat.Prime p → p ∣ Fintype.card G → ∃ (H : Subgroup G) (x : Fintype ↥H), ¬p ∣ H.index ∧ LinearMap.id ∈ LinearMap.range (norm (MonoidHom.comp (ρ.linHom ρ) H.subtype))) : LinearMap.id ∈ LinearMap.range (ρ.linHom ρ).norm

The identity is a norm if it is one at every relevant prime. If for every prime divisor p of |G| the identity of V is a norm for the conjugation action of a subgroup of index prime to p, then it is a norm for the conjugation action of G.

theorem Rep.projective_of_id_mem_range_norm_linHom {k G : Type u} [CommRing k] [Group G] [Fintype G] (A : Rep k G) [Module.Projective k ↑A] (h : LinearMap.id ∈ LinearMap.range (A.ρ.linHom A.ρ).norm) : CategoryTheory.Projective A

A representation whose identity is a norm is projective. If A is projective over k and id_A = ∑ g, A.ρ g ∘ φ ∘ A.ρ g⁻¹ for a k-linear φ, then A is projective.

theorem Rep.moduleProjective_of_id_mem_range_norm_linHom {k G : Type u} [CommRing k] [Group G] [Fintype G] (A : Rep k G) [Module.Projective k ↑A] (h : LinearMap.id ∈ LinearMap.range (A.ρ.linHom A.ρ).norm) : Module.Projective (MonoidAlgebra k G) A.ρ.asModule

A representation that is projective over k and whose identity is a norm is a projective k[G]-module.