linearization_map_hom_single — Mathlib

English

The map on linearizations sends a singleton basis to the singleton on the image: ((linearization k G).map f).hom (Finsupp.single x r) = Finsupp.single (f.hom x) r.

Русский

Отображение линейлизации на базисе-одиночке отправляет единичную базисную элементу в единичный базис изображённого элемента: ρ(f,h) δ_x = δ_{f.hom x}.

LaTeX

$$$((\mathrm{linearization}\ k\ G).map f).\mathrm{hom} (\mathrm{Finsupp}.\mathrm{single}(x, r)) = \mathrm{Finsupp}.\mathrm{single}(f.hom x, r)$$$

Lean4

theorem linearization_map_hom_single (x : X.V) (r : k) :
    ((linearization k G).map f).hom (Finsupp.single x r) = Finsupp.single (f.hom x) r :=
  Finsupp.mapDomain_single

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