English
There is a criterion: to prove j = k it suffices to verify their behavior on products and on images of R, given they map 1 to 1 and preserve multiplication.
Русский
Существует критерий: чтобы доказать j = k, достаточно проверить их поведение на произведениях и на образах R, при условии, что они отображают 1 в 1 и сохраняют умножение.
LaTeX
$$$ \\text{If } j,k : S \\to P, \\ j(1)=k(1), \\forall a,b: S,\\; j(ab)=j(a)j(b), \\forall a,b: S,\\; k(ab)=k(a)k(b), \\forall a:R,\\; j(\\mathrm{algebraMap}_{R,S} a)=k(\\mathrm{algebraMap}_{R,S} a) \\Rightarrow j=k. $$$
Lean4
/-- To show `j` and `k` agree on the whole localization, it suffices to show they agree
on the image of the base ring, if they preserve `1` and `*`. -/
protected theorem ext {P : Type*} [Monoid P] (j k : S → P) (hj1 : j 1 = 1) (hk1 : k 1 = 1)
(hjm : ∀ a b, j (a * b) = j a * j b) (hkm : ∀ a b, k (a * b) = k a * k b)
(h : ∀ a, j (algebraMap R S a) = k (algebraMap R S a)) : j = k :=
let j' : MonoidHom S P := { toFun := j, map_one' := hj1, map_mul' := hjm }
let k' : MonoidHom S P := { toFun := k, map_one' := hk1, map_mul' := hkm }
have : j' = k' := monoidHom_ext M (MonoidHom.ext h)
show j'.toFun = k'.toFun by rw [this]
