English
Two maps j,k:S → P are equal if they agree on the image of R and preserve multiplication and the unit, i.e., if j(1)=k(1), j(a b)=j(a)j(b), k(a b)=k(a)k(b), and j(algebraMap_R_S a)=k(algebraMap_R_S a) for all a ∈ R.
Русский
Две отображения j,k:S → P равны тогда и только тогда, когда они совпадают на образе R и сохраняют единицу и умножение: j(1)=k(1), j(a b)=j(a)j(b), k(a b)=k(a)k(b), и j(algebraMap_R_S a)=k(algebraMap_R_S a) для всех a.
LaTeX
$$$ \\text{If } j,k:S\\to P,\\; j(1)=k(1),\\; j(ab)=j(a)j(b),\\; k(ab)=k(a)k(b),\\; j(\\mathrm{algebraMap}_{R,S}a)=k(\\mathrm{algebraMap}_{R,S}a) \\ \\,\\forall a\\in R, \\text{ then } j=k. $$$
Lean4
@[simp]
theorem lift_of_comp (j : S →+* P) : lift (isUnit_comp M j) = j :=
RingHom.ext <| (DFunLike.ext_iff (F := MonoidHom _ _)).1 <| (toLocalizationMap M S).lift_of_comp j.toMonoidHom
