English
There is a canonical, well-defined linear map from the quotient (Q ⊗_R N) / range (lTensor Q f) to Q ⊗_R P, given by sending the class of q ⊗ n to q ⊗ g(n) whenever f: M → N and g: N → P form an exact sequence f ∘? = 0 with g, i.e., Exact f g.
Русский
Существует каноническая хорошо определенная линейная карта из квадрата (Q ⊗_R N) / range (lTensor Q f) в Q ⊗_R P, которая отправляет класс q ⊗ n в q ⊗ g(n) при условии, что f: M → N и g: N → P образуют точную последовательность; то есть enforces точность через левый тензор.
LaTeX
$$$\\text{toFun}: (Q \\otimes_R N) / \\mathrm{range}(\\mathrm{lTensor}\\ _Q f) \\to \\; Q \\otimes_R P$ defined by $(q\\otimes n) + \\mathrm{range}(\\mathrm{lTensor}\\ _Q f) \\mapsto q \\otimes g(n)$, well-defined when $\\mathrm{Exact}(f,g)$.$$
Lean4
/-- The direct map in `lTensor.equiv` -/
noncomputable def toFun (hfg : Exact f g) : Q ⊗[R] N ⧸ LinearMap.range (lTensor Q f) →ₗ[R] Q ⊗[R] P :=
Submodule.liftQ _ (lTensor Q g) <| by
rw [LinearMap.range_le_iff_comap, ← LinearMap.ker_comp, ← lTensor_comp, hfg.linearMap_comp_eq_zero, lTensor_zero,
ker_zero]
