English
The hom equivalence for the identity extension matches the restriction identification: the isomorphism between Hom((extendScalars id).obj M, N) and Hom((restrictScalars id).obj M, N) agrees with the standard restriction isomorphism.
Русский
Гом-эквивалентность для идентичного расширения совпадает с идентификацией ограниченного случая: изоморфизм между Hom((extendScalars id).obj M, N) и Hom((restrictScalars id).obj M, N) согласуется с обычной гом-эквивалентностью ограничения.
LaTeX
$$$$ \mathrm{homEquiv}_{\mathrm{id}}(M,N) = \text{restriction-identity isomorphism}. $$$$
Lean4
theorem homEquiv_extendScalarsId (M : ModuleCat R) :
(extendRestrictScalarsAdj (RingHom.id R)).homEquiv _ _ ((extendScalarsId R).hom.app M) =
(restrictScalarsId R).inv.app M :=
by
ext m
rw [extendRestrictScalarsAdj_homEquiv_apply, ← extendScalarsId_inv_app_apply, ← comp_apply]
simp
