English
A zero linear map composed with a dualTensorHom under prodMap yields the dualTensorHom on the appropriate product modules with the corresponding inr.
Русский
Нулевая линейная карта, составленная с dualTensorHom под prodMap, даёт dualTensorHom на соответствующих произведённых модулях с inr.
LaTeX
$$$(0 : M \to N).prodMap (dualTensorHom R N Q (g \otimes q)) = dualTensorHom R (M \times N) (P \times Q) ((g \circ_\ell snd) \otimes_\ell inr(q))$$$
Lean4
@[simp]
theorem zero_prodMap_dualTensorHom (g : Module.Dual R N) (q : Q) :
(0 : M →ₗ[R] P).prodMap ((dualTensorHom R N Q) (g ⊗ₜ[R] q)) =
dualTensorHom R (M × N) (P × Q) ((g ∘ₗ snd R M N) ⊗ₜ inr R P Q q) :=
by
ext <;>
simp only [coe_comp, coe_inr, Function.comp_apply, prodMap_apply, dualTensorHom_apply, snd_apply, Prod.smul_mk,
LinearMap.zero_apply, smul_zero]
