freeLift_hom_single_single — Mathlib

English

For a function f: α → A, basis element i, group element g and scalars r, the homomorphism of the free lift sends the elementary tensor to r times A.ρ(g) applied to f(i).

Русский

Для функции f: α → A, базисного элемента i, элемента группы g и скаляра r гомоморфизм свободного подъема отправляет элемент $single i (single g r)$ в $r \\cdot A\\!\\rho(g) f(i)$.

LaTeX

$$$(freeLift A f).hom\\big( single\\ i\\ (single\\ g\\ r)\\big) = r \\cdot A.\\rho(g)\\big(f(i)\\big)$$$

Lean4

theorem freeLift_hom_single_single (f : α → A) (i : α) (g : G) (r : k) :
    (freeLift A f).hom (single i (single g r)) = r • A.ρ g (f i) := by simp

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