English
The inverse construction invFun p is a right inverse of toFun p, completing the isomorphism between the quotient and the product of quotients.
Русский
invFun p является правым обратным к toFun p, завершая изоморфизм между частичным и произведением частичных квот.
LaTeX
$$Function.RightInverse (invFun p) (toFun p)$$
Lean4
theorem right_inv : Function.RightInverse (invFun p) (toFun p) :=
by
dsimp only [toFun, invFun]
rw [Function.rightInverse_iff_comp, ← coe_comp, ← @id_coe R]
refine congr_arg _ (pi_ext fun i x => Submodule.Quotient.induction_on _ x fun x' => funext fun j => ?_)
rw [comp_apply, piQuotientLift_single, mapQ_apply, quotientPiLift_mk, id_apply]
by_cases hij : i = j <;> simp only [mkQ_apply, coe_single]
· subst hij
rw [Pi.single_eq_same, Pi.single_eq_same]
· rw [Pi.single_eq_of_ne (Ne.symm hij), Pi.single_eq_of_ne (Ne.symm hij), Quotient.mk_zero]
