English
There is a natural equivalence between the left tensor product and a hom-tensor configuration for finite free modules.
Русский
Существует естественное эквивалентное отображение между левым тензорным произведением и конфигурацией гом-тензора для конечно свободных модулей.
LaTeX
$$$P \otimes (M \to\! Q) \simeq M \to (P \otimes Q)$ under freeness assumptions.$$
Lean4
@[simp]
theorem comp_dualTensorHom (f : Module.Dual R M) (n : N) (g : Module.Dual R N) (p : P) :
dualTensorHom R N P (g ⊗ₜ[R] p) ∘ₗ dualTensorHom R M N (f ⊗ₜ[R] n) = g n • dualTensorHom R M P (f ⊗ₜ p) :=
by
ext m
simp only [coe_comp, Function.comp_apply, dualTensorHom_apply, LinearMap.map_smul, LinearMap.smul_apply]
rw [smul_comm]
