linearization_obj_ρ — Mathlib

English

The action ρ on the linearization (linearization k G).obj X is given by the map ρ(g) on finsupps applied pointwise, i.e., (linearization k G).obj X.ρ(g) = Finsupp.lmapDomain k k (X.ρ g).

Русский

Действие ρ на линейлизации задаётся как отображение на функции-функциях-функциях: (linearization k G).obj X.ρ(g) = Finsupp.lmapDomain k k (X.ρ g).

LaTeX

$$$((linearization\ k\ G).obj X).\rho(g) = \mathrm{Finsupp}.\mathrm{lmapDomain}\ k\ k\ (X.\rho\ g)$$$

Lean4

theorem linearization_obj_ρ (X : Action (Type u) G) (g : G) :
    ((linearization k G).obj X).ρ g = Finsupp.lmapDomain k k (X.ρ g) :=
  rfl

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