English
There is a canonical S-linear equivalence between the R-linear endomorphisms of R into M and the elements of M themselves; evaluation at 1 yields the isomorphism.
Русский
Существуют канонические S-линейные эквивалентности между линейными отображениями R → R в M и самими элементами M; значение в 1 дает изоморфизм.
LaTeX
$$$$ (R \\,→_R \\, M) \\\\simeq_S M \\\\text{ via } f \mapsto f(1), \\; x \mapsto (r \\mapsto r x) $$$$
Lean4
/-- The equivalence between R-linear maps from `R` to `M`, and points of `M` itself.
This says that the forgetful functor from `R`-modules to types is representable, by `R`.
This is an `S`-linear equivalence, under the assumption that `S` acts on `M` commuting with `R`.
When `R` is commutative, we can take this to be the usual action with `S = R`.
Otherwise, `S = ℕ` shows that the equivalence is additive.
See note [bundled maps over different rings].
-/
@[simps]
def ringLmapEquivSelf [Module S M] [SMulCommClass R S M] : (R →ₗ[R] M) ≃ₗ[S] M :=
{ applyₗ' S (1 : R) with
toFun := fun f ↦ f 1
invFun := smulRight (1 : R →ₗ[R] R)
left_inv := fun f ↦ by
ext
simp only [coe_smulRight, Module.End.one_apply, smul_eq_mul, ← map_smul f, mul_one]
right_inv := fun x ↦ by simp }
