Reducing a representation modulo a scalar

For a representation ρ of a monoid G on a module V over a commutative ring k and an element r : k, every operator ρ g is k-linear and so preserves r • V. The representation therefore descends to the quotient QuotSMulTop r V = V ⧸ r • V; this is Representation.quotSMulTop, whose operators are Mathlib's QuotSMulTop.map r applied to those of ρ. It is Mathlib's Representation.quotient by the G-stable submodule r • ⊤.

Reducing the regular representation k[G] modulo r gives, up to isomorphism, the regular representation of G over k ⧸ (r). Such reductions are the graded pieces of filtrations V ⊇ r • V ⊇ r ^ 2 • V ⊇ ⋯ of a representation, and of the multiplicative filtrations of unit groups modelled on them.

Main definitions

• Representation.quotSMulTop: the representation induced by ρ on V ⧸ r • V.
• Representation.IntertwiningMap.quotSMulTop: the reduction modulo r of an intertwining map.

Main statements

• Representation.quotSMulTop_forall_eq_sum: if the identity of ρ is a norm x ↦ ∑ g, ρ g (φ (ρ g⁻¹ x)), then so is the identity of ρ.quotSMulTop r.

noncomputable def Representation.quotSMulTop {k : Type u_1} {G : Type u_2} {V : Type u_3} [CommRing k] [Monoid G] [AddCommGroup V] [Module k V] (ρ : Representation k G V) (r : k) : Representation k G (QuotSMulTop r V)

The representation induced by ρ on the reduction V ⧸ r • V of V modulo r: Mathlib's quotient representation Representation.quotient by the G-stable submodule r • ⊤. Its operators are QuotSMulTop.map r (ρ g) (Representation.quotSMulTop_apply).

Equations

• ρ.quotSMulTop r = ρ.quotient (r • ⊤) ⋯

@[simp]

theorem Representation.quotSMulTop_apply {k : Type u_1} {G : Type u_2} {V : Type u_3} [CommRing k] [Monoid G] [AddCommGroup V] [Module k V] (ρ : Representation k G V) (r : k) (g : G) : (ρ.quotSMulTop r) g = (QuotSMulTop.map r) (ρ g)

The operators of ρ.quotSMulTop r are the reductions QuotSMulTop.map r (ρ g).

theorem Representation.quotSMulTop_apply_mk {k : Type u_1} {G : Type u_2} {V : Type u_3} [CommRing k] [Monoid G] [AddCommGroup V] [Module k V] (ρ : Representation k G V) (r : k) (g : G) (x : V) : ((ρ.quotSMulTop r) g) (Submodule.Quotient.mk x) = Submodule.Quotient.mk ((ρ g) x)

ρ.quotSMulTop r g sends the class of x to the class of ρ g x.

noncomputable def Representation.IntertwiningMap.quotSMulTop {k : Type u_1} {G : Type u_2} {V : Type u_3} [CommRing k] [Monoid G] [AddCommGroup V] [Module k V] {W : Type u_4} [AddCommGroup W] [Module k W] {ρ : Representation k G V} {σ : Representation k G W} (f : ρ.IntertwiningMap σ) (r : k) : (ρ.quotSMulTop r).IntertwiningMap (σ.quotSMulTop r)

Reduction of an intertwining map modulo r: QuotSMulTop.map r f : V ⧸ rV → W ⧸ rW intertwines ρ.quotSMulTop r and σ.quotSMulTop r.

Equations

• f.quotSMulTop r = { toLinearMap := (QuotSMulTop.map r) f.toLinearMap, isIntertwining' := ⋯ }

@[simp]

theorem Representation.IntertwiningMap.toLinearMap_quotSMulTop {k : Type u_1} {G : Type u_2} {V : Type u_3} [CommRing k] [Monoid G] [AddCommGroup V] [Module k V] {W : Type u_4} [AddCommGroup W] [Module k W] {ρ : Representation k G V} {σ : Representation k G W} (f : ρ.IntertwiningMap σ) (r : k) : (f.quotSMulTop r).toLinearMap = (QuotSMulTop.map r) f.toLinearMap

The linear map underlying the reduction of an intertwining map is QuotSMulTop.map.

theorem Representation.quotSMulTop_forall_eq_sum {k : Type u_1} {V : Type u_3} [CommRing k] [AddCommGroup V] [Module k V] {G : Type u_4} [Group G] [Fintype G] {ρ : Representation k G V} (φ : V →ₗ[k] V) (hφ : ∀ (x : V), x = ∑ g : G, (ρ g) (φ ((ρ g⁻¹) x))) (r : k) (x : QuotSMulTop r V) : x = ∑ g : G, ((ρ.quotSMulTop r) g) (((QuotSMulTop.map r) φ) (((ρ.quotSMulTop r) g⁻¹) x))

If the identity of ρ is the norm x ↦ ∑ g, ρ g (φ (ρ g⁻¹ x)) of a k-linear map φ, then the identity of ρ.quotSMulTop r is the norm of the reduction QuotSMulTop.map r φ.