English
TensorProduct.map distributes over dualTensorHom in a natural way, yielding a dualTensorHom on the tensor of the product modules.
Русский
TensorProduct.map приносит совместимый эффект над dualTensorHom, порождая dualTensorHom на тензоре произведённых модулей.
LaTeX
$$$\mathrm{TensorProduct}.map\big(\mathrm{dualTensorHom}(R M P)(f \otimes p) , \mathrm{dualTensorHom}(R N Q)(g \otimes q)\big) = \mathrm{dualTensorHom}(R, M \otimes N, P \otimes Q)(\mathrm{dualDistrib}(R M N)(f \otimes g) \otimes (p \otimes q)).$$$
Lean4
theorem map_dualTensorHom (f : Module.Dual R M) (p : P) (g : Module.Dual R N) (q : Q) :
TensorProduct.map (dualTensorHom R M P (f ⊗ₜ[R] p)) (dualTensorHom R N Q (g ⊗ₜ[R] q)) =
dualTensorHom R (M ⊗[R] N) (P ⊗[R] Q) (dualDistrib R M N (f ⊗ₜ g) ⊗ₜ[R] (p ⊗ₜ[R] q)) :=
by
ext m n
simp only [compr₂_apply, mk_apply, map_tmul, dualTensorHom_apply, dualDistrib_apply, ← smul_tmul_smul]
