English
Let R and S be commutative rings and f: R →* S a ring hom. For any R–module X and S–module Y, and any S-linear map g: Y → (coextendScalars f).obj X, the corresponding map under the restriction–extension equivalence sends an element y ∈ Y to g.hom y evaluated at the unit of S; i.e., (HomEquiv.toRestriction f g).hom y = g.hom y (1_S).
Русский
Пусть R и S — коммутативные кольца, f: R →* S — гомоморфизм колец. Пусть X — R-модуль, Y — S-модуль, и g: Y → (корасширение скаляров f) X — S-отображение. Соответствующее отображение через ограничение по кольцам отправляет элемент y ∈ Y в g.hom y, умноженное на единицу кольца S; то есть (HomEquiv.toRestriction f g).hom y = g.hom y (1_S).
LaTeX
$$$$\forall R,S\;[\text{CommRing }R][\text{CommRing }S],\; f:R\to_* S,\; X\in \mathrm{Mod}_R,\; Y\in \mathrm{Mod}_S,\; g: Y \to (\mathrm{coextendScalars}_f)X,\; y\in Y:\quad (\mathrm{HomEquiv}^{-1}_{f}g)\!\cdot y = g.y(1_S). $$$$
Lean4
/-- This should be autogenerated by `@[simps]` but we need to give `1` the correct type here. -/
@[simp]
theorem toRestriction_hom_apply {X : ModuleCat R} {Y : ModuleCat S} (g : Y ⟶ (coextendScalars f).obj X) (y) :
(HomEquiv.toRestriction f g).hom y = g.hom y (1 : S) :=
rfl
