English
Let R be a commutative semiring and M an R-module. For every linear map f: N → R, the composite of the left unitor with the right-tensoring map equals the lift of the map obtained by applying the scalar multiplication action on M after f. In symbols, (lid_R M) ∘ (rTensor M f) = lift ((lsmul R M) ∘ f).
Русский
Пусть R — коммутативная полуполугруппа, M — модуль над R. Пусть f: N → R — линейный отображение. Тогда композиция левого тождественного отображения с правой тензоризацией f равна подъему отображения, полученного из f путём применения скалярного умножения на M. Обозначается как (lid_R M) ∘ (rTensor M f) = lift ((lsmul R M) ∘ f).
LaTeX
$$$ (\\mathrm{lid} \\, R \\, M) \\circ (\\mathrm{rTensor} \\, M \\, f) = \\mathrm{lift}\\big((\\mathrm{lsmul} \\, R \\, M) \\circ f\\big). $$$
Lean4
theorem lid_comp_rTensor (f : N →ₗ[R] R) : (lid R M).comp (rTensor M f) = lift ((lsmul R M).comp f) :=
ext' fun _ _ ↦ rfl
