English
Two canonical isomorphisms between a left-tensor product and a Hom-tensor construction agree as linear maps.
Русский
Два канонических изоморфизма между левым тензорным произведением и конструкцией Hom-тензор совпадают как линейные отображения.
LaTeX
$$$(lTensorHomEquivHomLTensor\\;R\\;M\\;P\\;Q).\\text{toLinearMap} = lTensorHomToHomLTensor\\;R\\;M\\;P\\;Q$$$
Lean4
@[simp]
theorem lTensorHomEquivHomLTensor_toLinearMap :
(lTensorHomEquivHomLTensor R M P Q).toLinearMap = lTensorHomToHomLTensor R M P Q :=
by
let e := congr (LinearEquiv.refl R P) (dualTensorHomEquiv R M Q)
have h : Function.Surjective e.toLinearMap := e.surjective
refine (cancel_right h).1 ?_
ext f q m
simp only [e, lTensorHomEquivHomLTensor, dualTensorHomEquiv, LinearEquiv.comp_coe, compr₂_apply, mk_apply,
LinearEquiv.coe_coe, LinearEquiv.trans_apply, congr_tmul, LinearEquiv.refl_apply, dualTensorHomEquivOfBasis_apply,
dualTensorHomEquivOfBasis_symm_cancel_left, leftComm_tmul, dualTensorHom_apply, coe_comp, Function.comp_apply,
lTensorHomToHomLTensor_apply, tmul_smul]
