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