English
The universal property of free modules: giving a function from the basis index to N is equivalent to giving an R-linear map M → N, under a suitable SMulComm condition, parameterized by an extra semiring S.
Русский
Универсальная свойство свободных модулей: задание функции от индексов базиса в N эквивалентно заданию линейного отображения M → N при условии SMulComm и добавления дополнительного кольца S.
LaTeX
$$$$ (\mathrm{ChooseBasisIndex}(R,M) \to N) \ \cong_S\ M \to_R N $$$$
Lean4
/-- The universal property of free modules: giving a function `(ChooseBasisIndex R M) → N`, for `N`
an `R`-module, is the same as giving an `R`-linear map `M →ₗ[R] N`.
This definition is parameterized over an extra `Semiring S`,
such that `SMulCommClass R S M'` holds.
If `R` is commutative, you can set `S := R`; if `R` is not commutative,
you can recover an `AddEquiv` by setting `S := ℕ`.
See library note [bundled maps over different rings]. -/
noncomputable def constr {S : Type z} [Semiring S] [Module S N] [SMulCommClass R S N] :
(ChooseBasisIndex R M → N) ≃ₗ[S] M →ₗ[R] N :=
Basis.constr (chooseBasis R M) S
