English
The linear equivalence lTensor.linearEquiv_of_rightInverse is the canonical equivalence between the quotient (Q ⊗ N) / range (lTensor Q f) and (Q ⊗ P) induced by a right inverse h of g, with left and right inverse data ensuring the equivalence.
Русский
Линейное эквивалентность строится из правого обратного и образует каноническое соответствие между квотой и левым тензором.
LaTeX
$$lTensor.linearEquiv_of_rightInverse Q hgh : ((Q ⊗ N) / range (lTensor Q f)) ≃_L (Q ⊗ P)$$
Lean4
/-- For a surjective `f : N →ₗ[R] P`,
the natural equivalence between `Q ⊗ N ⧸ (image of ker f)` to `Q ⊗ P`
(computably, given a right inverse) -/
noncomputable def linearEquiv_of_rightInverse {h : P → N} (hgh : Function.RightInverse h g) :
((Q ⊗[R] N) ⧸ (LinearMap.range (lTensor Q f))) ≃ₗ[R] (Q ⊗[R] P) :=
{ toLinearMap := lTensor.toFun Q hfg
invFun := lTensor.inverse_of_rightInverse Q hfg hgh
left_inv := fun y ↦ by
simp only [lTensor.toFun, AddHom.toFun_eq_coe, coe_toAddHom]
obtain ⟨y, rfl⟩ := Submodule.mkQ_surjective _ y
simp only [Submodule.mkQ_apply, Submodule.liftQ_apply, lTensor.inverse_of_rightInverse_apply]
right_inv := fun z ↦ by
simp only [AddHom.toFun_eq_coe, coe_toAddHom]
obtain ⟨y, rfl⟩ := lTensor_surjective Q (hgh.surjective) z
rw [lTensor.inverse_of_rightInverse_apply]
simp only [lTensor.toFun, Submodule.liftQ_apply] }
