English
The left regular representation on k[G] acts by left-translation on the function space; equivalently, the image of g under the representation is the endomorphism sending f to f translated by g⁻¹.
Русский
Левое регулярное представление на k[G] действует посредством левого переноса; изображение g превращает f в Translated по g⁻¹.
LaTeX
$$$(\\text{leftRegular}(g) f)(h) = f(g^{-1} h)$$$
Lean4
@[simp]
theorem ofMulAction_apply {H : Type*} [MulAction G H] (g : G) (f : H →₀ k) (h : H) :
ofMulAction k G H g f h = f (g⁻¹ • h) :=
by
conv_lhs => rw [← smul_inv_smul g h]
let h' := g⁻¹ • h
change ofMulAction k G H g f (g • h') = f h'
have hg : Function.Injective (g • · : H → H) := by
intro h₁ h₂
simp
simp only [ofMulAction_def, Finsupp.lmapDomain_apply, Finsupp.mapDomain_apply, hg]
-- Noncomputable since `MonoidAlgebra.instMul` is now noncomputable
