English
There is a linear equivalence between the R-linear maps from (ι → R) to M and the ι-indexed family M, regarded as an S-linear equivalence under a commuting action of R and S on M.
Русский
Существует линейное эквивалентство между линейными отображениями из (ι → R) в M и семейством M, индексированным по i ∈ ι, рассматриваемым как S-линейное эквивалентство при взаимоотношении действий R и S на M.
LaTeX
$$$$ ((ι \\to R) \\to_{R} M) \\simeq_{\\!S} (ι \\to M), $$$$
Lean4
/-- Linear equivalence between linear functions `Rⁿ → M` and `Mⁿ`. The spaces `Rⁿ` and `Mⁿ`
are represented as `ι → R` and `ι → M`, respectively, where `ι` is a finite type.
This as 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]. -/
def piRing : ((ι → R) →ₗ[R] M) ≃ₗ[S] ι → M :=
(LinearMap.lsum R (fun _ : ι => R) S).symm.trans (piCongrRight fun _ => LinearMap.ringLmapEquivSelf R S M)
