piEquiv — Mathlib

English

There is a natural linear equivalence between the product M^ι and the space of linear maps from (ι → R) to M, i.e., (ι → M) ≃ₗ[R] ((ι → R) →ₗ[R] M).

Русский

Существует естественное линейное эквивалентное сопоставление между произведением M^ι и пространством линейных отображений из (ι → R) в M.

LaTeX

$$$\text{piEquiv} : (ι \to M) \simeq_ℓ[R] ((ι \to R) \to_ℓ[R] M)$$$

Lean4

/-- The natural linear equivalence: `Mⁱ ≃ Hom(Rⁱ, M)` for an `R`-module `M`. -/
noncomputable def piEquiv : (ι → M) ≃ₗ[R] ((ι → R) →ₗ[R] M) :=
  Basis.constr (Pi.basisFun R ι) R

Похожие утверждения