English
For any commutative rings R,S and f: R →* S, extendScalarsId is an isomorphism; its inverse on an R-module M sends m ∈ M to 1 ⊗ m. Consequently, the unit-counit interplay expresses identity after applying the inverse and then the forward map.
Русский
Для колец R,S и гомоморфизма f: R →* S расширение и ограничение скаляров дают изоморфизм, чья обратная карта на модуле M отправляет m ∈ M в 1 ⊗ m. Взаимодействие единицы и коунита даёт тождество после применения обратной и прямой карты.
LaTeX
$$$$ (\mathrm{extendScalarsId}_R)^{-1}_M(m) = 1 \otimes m \quad\text{для } m \in M, $$
$$ \mathrm{extendScalarsId}_R \text{ является изоморфизмом, и } (\mathrm{extendScalarsId}_R)^{-1}(m) = 1 \otimes m. $$$$
Lean4
theorem extendRestrictScalarsAdj_homEquiv_apply {R : Type u₁} {S : Type u₂} [CommRing R] [CommRing S] {f : R →+* S}
{M : ModuleCat.{max v u₂} R} {N : ModuleCat S} (φ : (extendScalars f).obj M ⟶ N) (m : M) :
(extendRestrictScalarsAdj f).homEquiv _ _ φ m = φ ((1 : S) ⊗ₜ m) :=
rfl
