English
The product map of a zero map with a dual-tensor hom equals the dual-tensor hom on the product modules with a suitable tensor on the left.
Русский
Произведение prodMap нулевой линейной карты и гомоморфии dualTensorHom эквивалентно dualTensorHom на произведённых модулях с подходящим тензорным элементом слева.
LaTeX
$$$(\,dualTensorHom R M P\,(f \otimes p)\,).prodMap(0) = dualTensorHom R (M \times N) (P \times Q)\big((f \circ_\ell fst) \otimes_\ell inl(p)\big)$$$
Lean4
@[simp]
theorem dualTensorHom_prodMap_zero (f : Module.Dual R M) (p : P) :
((dualTensorHom R M P) (f ⊗ₜ[R] p)).prodMap (0 : N →ₗ[R] Q) =
dualTensorHom R (M × N) (P × Q) ((f ∘ₗ fst R M N) ⊗ₜ inl R P Q p) :=
by
ext <;>
simp only [coe_comp, coe_inl, Function.comp_apply, prodMap_apply, dualTensorHom_apply, fst_apply, Prod.smul_mk,
LinearMap.zero_apply, smul_zero]
