linearization_single — Mathlib

English

Acting by g on a basic delta vector is given by transporting the fundamental basis: ρ g (Finsupp.single x r) = Finsupp.single (X.ρ g x) r.

Русский

Действие g на базисный вектор-дельта переводится в базис на X.ρ g x: ρ g (δ_x) = δ_{X.ρ g x} с тем же коэффициентом r.

LaTeX

$$$\rho(g)\bigl(\mathrm{Finsupp}.\mathrm{single}(x, r)\bigr) = \mathrm{Finsupp}.\mathrm{single}(X.\rho g x, r)$$$

Lean4

theorem linearization_single (X : Action (Type u) G) (g : G) (x : X.V) (r : k) :
    ((linearization k G).obj X).ρ g (Finsupp.single x r) = Finsupp.single (X.ρ g x) r := by simp

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