English
If e is a linear isomorphism M2 ≃ₗ[R] M3, then postcomposing with e yields an S-linear isomorphism between the spaces (M →ₗ[R] M2) and (M →ₗ[R] M3).
Русский
Если e — линейный изоморфизм M2 ≃ₗ[R] M3, то композиция справа с e задаёт S-линейное изоморфизм между пространствами отображений M → M2 и M → M3.
LaTeX
$$$ (M \to_{\mathbb{R}} M_2) \simeq_{\mathsf{S}} (M \to_{\mathbb{R}} M_3) $$$
Lean4
/-- An `R`-linear isomorphism between two `R`-modules `M₂` and `M₃` induces an `S`-linear
isomorphism between `M₂ →ₗ[R] M` and `M₃ →ₗ[R] M`, if `M` is both an `R`-module and an
`S`-module and their actions commute. -/
def congrLeft {R} (S) [Semiring R] [Semiring S] [Module R M₂] [Module R M₃] [Module R M] [Module S M]
[SMulCommClass R S M] (e : M₂ ≃ₗ[R] M₃) : (M₂ →ₗ[R] M) ≃ₗ[S] (M₃ →ₗ[R] M)
where
__ := e.arrowCongrAddEquiv (.refl ..)
map_smul' _ _ := rfl
