English
The transpose of dualTensorHom corresponds to swapping the roles of the two factors in the tensor product, up to the dual-distribution adjustment.
Русский
Транспонирование dualTensorHom соответствует смене ролей факторов в тензорном произведении, с учётом двойственной дистрибутивности.
LaTeX
$$$\operatorname{Dual}.\operatorname{transpose}(\,\mathrm{dualTensorHom}(R,M,M)(f \otimes m)\,) = \mathrm{dualTensorHom}(R, M^*, M^*)(\mathrm{Dual.eval}(R,M)(m) \otimes f)$$$
Lean4
@[simp]
theorem transpose_dualTensorHom (f : Module.Dual R M) (m : M) :
Dual.transpose (R := R) (dualTensorHom R M M (f ⊗ₜ m)) = dualTensorHom R _ _ (Dual.eval R M m ⊗ₜ f) :=
by
ext f' m'
simp only [Dual.transpose_apply, coe_comp, Function.comp_apply, dualTensorHom_apply, LinearMap.map_smulₛₗ,
RingHom.id_apply, Algebra.id.smul_eq_mul, Dual.eval_apply, LinearMap.smul_apply]
exact mul_comm _ _
