Forgetting the scalars of a representation

A representation of a monoid G on a k-module V is in particular a representation on the underlying abelian group, that is on V as a ℤ-module for its canonical ℤ-module structure, because every operator is additive. Representation.restrictScalarsInt packages this observation. It is the discrete counterpart of ContRepresentation.restrictScalarsInt.

It is what lets a representation that is naturally linear over a larger ring, such as a quotient M ⧸ r • M of a module over the valuation ring of a local field, be compared with integral representations that carry no such structure, such as the unit group of a local field. Tate cohomology and the Herbrand quotient of such a comparison are taken in Rep ℤ G.

Only the canonical ℤ-module structure exists on every abelian group without a choice, which is why the target ring is ℤ rather than an arbitrary subring of k.

Main definitions

• Representation.restrictScalarsInt: a representation over k, read as a representation over ℤ with the same operators.

def Representation.restrictScalarsInt {k : Type u_1} {G : Type u_2} {V : Type u_3} [Semiring k] [Monoid G] [AddCommGroup V] [Module k V] (ρ : Representation k G V) : Representation ℤ G V

A representation on a k-module, read as a representation on the underlying abelian group: each operator is restricted to a ℤ-linear map. Its operators are those of ρ (Representation.restrictScalarsInt_apply).

Equations

• ρ.restrictScalarsInt = { toFun := fun (g : G) => ↑ℤ (ρ g), map_one' := ⋯, map_mul' := ⋯ }

@[simp]

theorem Representation.restrictScalarsInt_apply {k : Type u_1} {G : Type u_2} {V : Type u_3} [Semiring k] [Monoid G] [AddCommGroup V] [Module k V] (ρ : Representation k G V) (g : G) (v : V) : (ρ.restrictScalarsInt g) v = (ρ g) v

The operators of ρ.restrictScalarsInt are those of ρ.