English
The canonical isomorphism rTensorHomEquivHomRTensor coincides with the standard rTensorHomToHomRTensor map under finiteness/free hypotheses on M.
Русский
Каноническое изоморождение rTensorHomEquivHomRTensor совпадает с обычным rTensorHomToHomRTensor при условиях конечной свободы модуля M.
LaTeX
$$$(\\mathrm{rTensorHomEquivHomRTensor}\\;R\\;M\\;P\\;Q).\\text{toLinearMap} = rTensorHomToHomRTensor\\;R\\;M\\;P\\;Q$$$
Lean4
@[simp]
theorem rTensorHomEquivHomRTensor_toLinearMap :
(rTensorHomEquivHomRTensor R M P Q).toLinearMap = rTensorHomToHomRTensor R M P Q :=
by
let e := congr (dualTensorHomEquiv R M P) (LinearEquiv.refl R Q)
have h : Function.Surjective e.toLinearMap := e.surjective
refine (cancel_right h).1 ?_
ext f p q m
simp only [e, rTensorHomEquivHomRTensor, dualTensorHomEquiv, compr₂_apply, mk_apply, coe_comp,
LinearEquiv.coe_toLinearMap, Function.comp_apply, dualTensorHomEquivOfBasis_apply, LinearEquiv.trans_apply,
congr_tmul, dualTensorHomEquivOfBasis_symm_cancel_left, LinearEquiv.refl_apply, assoc_tmul, dualTensorHom_apply,
rTensorHomToHomRTensor_apply, smul_tmul']
