English
piTensorHomMapFun₂ is additive in its argument: piTensorHomMapFun₂ (φ + ψ) = piTensorHomMapFun₂ φ + piTensorHomMapFun₂ ψ.
Русский
piTensorHomMapFun₂ аддитивно по аргументу: phi+psi → сумма соответствующих отображений.
LaTeX
$$$\piTensorHomMapFun₂ (\varphi + \psi) = \piTensorHomMapFun₂ \varphi + \piTensorHomMapFun₂ \psi$$$
Lean4
/-- Let `sᵢ`, `tᵢ` and `t'ᵢ` be families of `R`-modules.
Then there is an linear map from `⨂ᵢ Hom(sᵢ, Hom(tᵢ, t'ᵢ))` to `Hom(⨂ᵢ sᵢ, Hom(⨂ tᵢ, ⨂ᵢ t'ᵢ))`
defined by `⨂ᵢ fᵢ ↦ ⨂ᵢ aᵢ ↦ ⨂ᵢ bᵢ ↦ ⨂ᵢ fᵢ aᵢ bᵢ`.
This is `TensorProduct.homTensorHomMap` for two arbitrary families of modules.
-/
def piTensorHomMap₂ : (⨂[R] i, s i →ₗ[R] t i →ₗ[R] t' i) →ₗ[R] (⨂[R] i, s i) →ₗ[R] (⨂[R] i, t i) →ₗ[R] (⨂[R] i, t' i)
where
toFun := piTensorHomMapFun₂
map_add' x y := piTensorHomMapFun₂_add x y
map_smul' x y := piTensorHomMapFun₂_smul x y
