English
In the congruence isomorphism, applying f_i to a pure tensor m_i yields the pure tensor of the images: congr f (tprod m) = tprod (f_i(m_i)).
Русский
В изоморфизме congr применяемое к простому тензору mu даёт чистый тензор изображений: congr f (tprod m) = tprod (f_i(m_i)).
LaTeX
$$$\mathrm{congr}\ f\ (\,tprod\ R\ m) = tprod\ R (\lambda i. f_i(m_i))$$$
Lean4
/-- Let `sᵢ` and `tᵢ` be families of `R`-modules.
Then there is an `R`-linear map between `⨂ᵢ Hom(sᵢ, tᵢ)` and `Hom(⨂ᵢ sᵢ, ⨂ tᵢ)` defined by
`⨂ᵢ fᵢ ↦ ⨂ᵢ aᵢ ↦ ⨂ᵢ fᵢ aᵢ`.
This is `TensorProduct.homTensorHomMap` for an arbitrary family of modules.
Note that `PiTensorProduct.piTensorHomMap (tprod R f)` is equal to `PiTensorProduct.map f`.
-/
def piTensorHomMap : (⨂[R] i, s i →ₗ[R] t i) →ₗ[R] (⨂[R] i, s i) →ₗ[R] ⨂[R] i, t i :=
lift.toLinearMap ∘ₗ lift (MultilinearMap.piLinearMap <| tprod R)
