Iobj_ρ_apply — Mathlib

English

Let rep be a G-representation on TopModuleCat R. The G-action on a function f: G → rep.V is given by (g • f)(x) = g • f(g⁻¹ x).

Русский

Пусть rep — представление G над TopModuleCat R. Действие G на функцию f: G → rep.V задаётся как (g • f)(x) = g • f(g⁻¹ x).

LaTeX

$$$((Iobj\\; rep).\\rho\\; g).hom\\; f\\; x = (rep.\\rho\\; g).hom\\; (f(g^{-1} * x))$$$

Lean4

theorem Iobj_ρ_apply (rep : Action (TopModuleCat R) G) (g f x) :
    ((Iobj rep).ρ g).hom f x = (rep.ρ g).hom (f (g⁻¹ * x)) :=
  rfl

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