Representations as multiplicative automorphisms

Representation.toMulAut views a representation of a group on a module as an action by automorphisms on its multiplicative type tag. This lets the representation act on exponents in a group algebra via MonoidAlgebra.domCongrAut.

noncomputable def Representation.toMulAut {R : Type u_1} {G : Type u_2} {M : Type u_3} [Semiring R] [Group G] [AddCommMonoid M] [Module R M] (rho : Representation R G M) : G →* MulAut (Multiplicative M)

A representation, acting by automorphisms in multiplicative notation.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem Representation.toMulAut_apply {R : Type u_1} {G : Type u_2} {M : Type u_3} [Semiring R] [Group G] [AddCommMonoid M] [Module R M] (rho : Representation R G M) (g : G) (m : Multiplicative M) : (rho.toMulAut g) m = Multiplicative.ofAdd ((rho g) (Multiplicative.toAdd m))

The multiplicative automorphism acts by the representation on the underlying module.

@[simp]

theorem Representation.toMulAut_symm_apply {R : Type u_1} {G : Type u_2} {M : Type u_3} [Semiring R] [Group G] [AddCommMonoid M] [Module R M] (rho : Representation R G M) (g : G) (m : Multiplicative M) : (MulEquiv.symm (rho.toMulAut g)) m = Multiplicative.ofAdd ((rho g⁻¹) (Multiplicative.toAdd m))

The inverse multiplicative automorphism acts by the representation of the inverse element.