ofMulAction — Mathlib

English

The natural k-linear G-representation on k[G] is given by the left action of G on itself, extended linearly to Finsupp (the free module on G).

Русский

Естественное k-линейное G-представление на k[G] задаётся левым действием G на саму G и линейно расширяется на Finsupp.

LaTeX

$$$\\text{leftRegular} = \\mathrm{ofMulAction}(k,G,G)$ with $(g) \\cdot f(h) = f(g^{-1}h)$$$

Lean4

/-- A `G`-action on `H` induces a representation `G →* End(k[H])` in the natural way. -/
noncomputable def ofMulAction : Representation k G (H →₀ k)
    where
  toFun g := Finsupp.lmapDomain k k (g • ·)
  map_one' := by
    ext x y
    simp
  map_mul' x
    y := by
    ext z w
    simp [mul_smul]

Похожие утверждения