linearization_of — Mathlib

English

The linearization of an action X at the element x with coefficient 1 is mapped to the corresponding delta in X via ρ, i.e., ρ g x becomes Finsupp.single (X.ρ g x) 1.

Русский

Линеаризация действия X отправляет элемент x с коэффициентом 1 в соответствующую дельту: ρ g x соответствует δ_{X.ρ g x} с коэффициентом 1.

LaTeX

$$$\rho(g)(Finsupp.single(x,1)) = Finsupp.single(X.\rho(g)x,1)$$$

Lean4

@[deprecated "Use `Rep.linearization_single` instead" (since := "2025-06-02")]
theorem linearization_of (X : Action (Type u) G) (g : G) (x : X.V) :
    ((linearization k G).obj X).ρ g (Finsupp.single x (1 : k)) = Finsupp.single (X.ρ g x) (1 : k) := by simp

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