English
There exists a natural linear equivalence between the quotient (Q ⊗_R N) / range (lTensor Q f) and Q ⊗_R P when h is a right inverse of g and f,g are exact. This linear equivalence is given by toFun and inverse_of_rightInverse with the appropriate right inverse.
Русский
Существует естественное линейное эквивалентное отображение между квадратом и левым тензором, полученное из обратной карты и прямой карты, когда f,g точны и есть правый обратный h.
LaTeX
$$$lTensor.linearEquiv_of_rightInverse\_Q: ((Q\\otimes_R N) / \\mathrm{range}(lTensor\\ Q\\ f)) \\simeq_R (Q\\otimes_R P)$$$
Lean4
/-- The inverse map in `lTensor.equiv` -/
noncomputable def inverse : Q ⊗[R] P →ₗ[R] Q ⊗[R] N ⧸ LinearMap.range (lTensor Q f) :=
lTensor.inverse_of_rightInverse Q hfg (Function.rightInverse_surjInv hg)
