Invariants of group representations

Mathlib names the group sum ∑ g, ρ g of a finite-group representation Representation.norm, builds the averaging projection Representation.averageMap separately out of the group-algebra element GroupAlgebra.average, and records that the latter projects onto the invariants (Representation.isProj_averageMap). What it does not record is how the two operators relate. The group sum is the shape a symmetrization operator actually takes at a use site, where the normalizing factor ⅟(#G) is usually left implicit, and reinstating it by hand is the step that gets rewritten.

This file supplies the bridge. Unfolding the group algebra once identifies averageMap with norm scaled by ⅟(#G), and since scaling by a unit changes no image, norm has the same range as the projection: the invariants.

There is a different integral reason for the norm to map onto the invariants. The norm does so on the regular representation over any commutative ring, hence on every projective group-algebra module by passage to a free module and a direct summand. As a consequence, taking invariants preserves a surjection onto a projective representation. This exactness property is the input needed to lift modular invariant vectors to an integral projective lattice.

The file also records the companion description of the invariants available when G is cyclic. Invariance is a condition on every group element, but a vector fixed by a generator is fixed by all of its powers, so testing a single generator g suffices and the invariants are cut out by the one linear map ρ(g) - 1. Mathlib states this elementwise, in Representation.mem_invariants_iff_of_forall_mem_zpowers; the submodule-level equality with ker (ρ(g) - 1) is the form used to present the (co)homology of a finite cyclic group as a subquotient of M, where each group is the homology of ρ(g) - 1 and the norm in one order or the other.

Finally, a nontrivial irreducible representation has no nonzero invariant vector. This is what makes the Haar integral of a nontrivial irreducible character vanish. A dimension-based corollary handles the common case where nontriviality follows from the dimension being other than one.

Taking invariants under a normal subgroup S, Mathlib's Rep.quotientToInvariantsFunctor, is an additive functor from representations of G to representations of G ⧸ S.

Main results

• Representation.averageMap_eq_invOf_card_smul_norm: the averaging projection is the group sum Representation.norm scaled by the inverse of the group order.
• Representation.range_norm_eq_invariants: the group sum Representation.norm ρ has the invariants as its range.
• Representation.range_norm_eq_invariants_of_projective: the same conclusion without inverting the group order, when the underlying group-algebra module is projective.
• Representation.range_norm_trivial: for trivial coefficients, the range of the norm is the ideal generated by the group order.
• Representation.exists_invariant_preimage_of_surjective_of_projective: a surjective equivariant additive map, possibly between representations over different coefficient rings, lifts invariant vectors when its target is projective over the target group algebra.
• Representation.Equiv.invariantsLinearEquiv: equivalent representations have isomorphic invariants.
• Rep.invariantsFunctor_map_surjective_of_surjective_of_projective: taking invariants preserves a surjective morphism of representations whose target is projective over the group algebra.
• Rep.FiniteCyclicGroup.invariants_eq_ker_apply_sub: for a cyclic group, the invariants are the kernel of the action of a generator minus the identity.
• Representation.IsIrreducible.invariants_eq_bot: a nontrivial irreducible representation has no nonzero invariant vector.
• Representation.IsIrreducible.invariants_eq_bot_of_finrank_ne_one: the dimension-based specialization.
• Representation.IsIrreducible.eq_trivial_of_invariants_ne_bot and Representation.IsIrreducible.finrank_eq_one_of_invariants_ne_bot: the two contrapositives, which turn a nonzero invariant vector of an irreducible representation into triviality and into dimension one.
• Rep.quotientToInvariantsFunctor is additive.

theorem Representation.averageMap_eq_invOf_card_smul_norm {k : Type u_1} {G : Type u_2} {V : Type u_3} [CommRing k] [Group G] [AddCommGroup V] [Module k V] (ρ : Representation k G V) [Fintype G] [Invertible ↑(Fintype.card G)] : ρ.averageMap = ⅟↑(Fintype.card G) • ρ.norm

The averaging projection is the normalized group sum. Mathlib defines Representation.averageMap through the group algebra; this unfolds that definition to the group sum Representation.norm, scaled by the inverse of the group order.

@[simp]

theorem Representation.range_norm_eq_invariants {k : Type u_1} {G : Type u_2} {V : Type u_3} [CommRing k] [Group G] [AddCommGroup V] [Module k V] (ρ : Representation k G V) [Fintype G] [Invertible ↑(Fintype.card G)] : LinearMap.range ρ.norm = ρ.invariants

The group sum has the invariants as its range. When #G is invertible in k, the operator Representation.norm ρ = ∑ g, ρ g maps onto the invariants of ρ: it agrees with the averaging projection up to the unit #G, so the two have the same image.

@[simp]

theorem Representation.range_norm_trivial (k : Type u_1) (H : Type u_2) [CommSemiring k] [Group H] [Fintype H] : LinearMap.range (trivial k H k).norm = Ideal.span {↑(Nat.card H)}

For trivial coefficients, the range of the norm is the ideal generated by the group order.

@[simp]

theorem Representation.range_norm_eq_invariants_of_projective {k : Type u_1} {G : Type u_2} {V : Type u_3} [CommRing k] [Group G] [AddCommGroup V] [Module k V] [Fintype G] (ρ : Representation k G V) [Module.Projective (MonoidAlgebra k G) ρ.asModule] : LinearMap.range ρ.norm = ρ.invariants

The norm maps onto the invariants of a projective representation. Let G be finite over an arbitrary commutative ring k. If the k[G]-module underlying ρ is projective, then every invariant vector is the norm of a vector.

This is the integral replacement for Representation.range_norm_eq_invariants, which assumes that the order of G is invertible in k.

theorem Representation.exists_invariant_preimage_of_surjective_of_projective {k : Type u_1} {G : Type u_2} {V : Type u_3} [CommRing k] [Group G] [AddCommGroup V] [Module k V] {l : Type u_4} [CommRing l] [Finite G] {X : Type u_5} [AddCommGroup X] [Module l X] (ρ : Representation k G V) (σ : Representation l G X) (f : V →+ X) (hf : Function.Surjective ⇑f) (hfg : ∀ (g : G) (x : V), f ((ρ g) x) = (σ g) (f x)) [Module.Projective (MonoidAlgebra l G) σ.asModule] (y : ↥σ.invariants) : ∃ (x : ↥ρ.invariants), f ↑x = ↑y

Equivariant surjections lift invariants when the target is projective. Let ρ and σ be representations of the same finite group, possibly over different commutative rings. If an equivariant additive map f : V →+ X is surjective and σ.asModule is projective over l[G], then every invariant vector of σ has an invariant preimage under f.

Allowing the coefficient rings to differ is essential for reduction of an integral projective lattice modulo a prime.

def Representation.Equiv.invariantsLinearEquiv {k : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} [CommRing k] [Group G] [AddCommGroup V] [Module k V] [AddCommGroup W] [Module k W] {ρ : Representation k G V} {σ : Representation k G W} (φ : ρ.Equiv σ) : ↥ρ.invariants ≃ₗ[k] ↥σ.invariants

Equivalent representations have isomorphic invariants. An equivalence of representations maps invariant vectors to invariant vectors, and so does its inverse.

Equations

• φ.invariantsLinearEquiv = { toFun := fun (x : ↥ρ.invariants) => ⟨φ ↑x, ⋯⟩, map_add' := ⋯, map_smul' := ⋯, invFun := fun (x : ↥σ.invariants) => ⟨φ.symm ↑x, ⋯⟩, left_inv := ⋯, right_inv := ⋯ }

@[simp]

theorem Representation.Equiv.coe_invariantsLinearEquiv_apply {k : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} [CommRing k] [Group G] [AddCommGroup V] [Module k V] [AddCommGroup W] [Module k W] {ρ : Representation k G V} {σ : Representation k G W} (φ : ρ.Equiv σ) (x : ↥ρ.invariants) : ↑(φ.invariantsLinearEquiv x) = φ ↑x

theorem Rep.invariantsFunctor_map_surjective_of_surjective_of_projective {k : Type u_1} {G : Type u_2} [CommRing k] [Group G] {A B : Rep k G} (f : A ⟶ B) (hf : Function.Surjective ⇑(Hom.hom f)) [Module.Projective (MonoidAlgebra k G) B.ρ.asModule] : Function.Surjective ⇑(ModuleCat.Hom.hom ((invariantsFunctor k G).map f))

Invariants preserve surjections onto projective representations. If f : A ⟶ B is surjective and the k[G]-module underlying B is projective, then every invariant of B lifts to an invariant of A.

theorem Representation.IsIrreducible.invariants_eq_bot {k : Type u_1} {G : Type u_2} {V : Type u_3} [Field k] [Group G] [AddCommGroup V] [Module k V] {ρ : Representation k G V} (h : ρ.IsIrreducible) (hρ : ρ ≠ trivial k G V) : ρ.invariants = ⊥

A nontrivial irreducible representation has no nonzero invariant vector.

theorem Representation.IsIrreducible.invariants_eq_bot_of_finrank_ne_one {k : Type u_1} {G : Type u_2} {V : Type u_3} [Field k] [Group G] [AddCommGroup V] [Module k V] {ρ : Representation k G V} (h : ρ.IsIrreducible) (hV : Module.finrank k V ≠ 1) : ρ.invariants = ⊥

An irreducible representation of dimension other than one has no nonzero invariant vector.

theorem Representation.IsIrreducible.eq_trivial_of_invariants_ne_bot {k : Type u_1} {G : Type u_2} {V : Type u_3} [Field k] [Group G] [AddCommGroup V] [Module k V] {ρ : Representation k G V} (h : ρ.IsIrreducible) (hne : ρ.invariants ≠ ⊥) : ρ = trivial k G V

An irreducible representation with a nonzero invariant vector is the trivial representation, the contrapositive of Representation.IsIrreducible.invariants_eq_bot.

theorem Representation.IsIrreducible.finrank_eq_one_of_invariants_ne_bot {k : Type u_1} {G : Type u_2} {V : Type u_3} [Field k] [Group G] [AddCommGroup V] [Module k V] {ρ : Representation k G V} (h : ρ.IsIrreducible) (hne : ρ.invariants ≠ ⊥) : Module.finrank k V = 1

An irreducible representation with a nonzero invariant vector is a line, the contrapositive of Representation.IsIrreducible.invariants_eq_bot_of_finrank_ne_one.

theorem Rep.FiniteCyclicGroup.invariants_eq_ker_apply_sub {R : Type u_1} {G : Type u_2} [CommRing R] [Group G] (M : Rep R G) (g : G) (hg : ∀ (x : G), x ∈ Subgroup.zpowers g) : M.ρ.invariants = (M.ρ g - LinearMap.id).ker

If g generates G, the invariants of a representation are the kernel of ρ(g) - 1.

instance TauCeti.instAdditiveRepQuotientSubgroupQuotientToInvariantsFunctor_tauCeti {k : Type u_1} {G : Type u_2} [CommRing k] [Group G] (S : Subgroup G) [S.Normal] : (Rep.quotientToInvariantsFunctor k S).Additive

Taking S-invariants is additive, so it maps short complexes of representations of G to short complexes of representations of G ⧸ S.