English
Uniqueness of algebra homs out of a localization: if two maps agree after composing with the base AlgHom, they are equal.
Русский
Уникальность алгебраических гомоморфизмов, выходящих из локализации: если два отображения совпадают после композиции с базовым AlgHom, они равны.
LaTeX
$$$\\forall f,g: Localization\\ W \\to_{R} B,\; f \\circ (\\mathrm{Algebra.algHom}\\; R\\; A\\; (Localization W)) = g \\circ (\\mathrm{Algebra.algHom}\\; R\\; A\\; (Localization W)) \\Rightarrow f = g$$$
Lean4
@[ext high]
theorem algHom_ext {R A B : Type*} [CommSemiring R] [CommSemiring A] [Semiring B] [Algebra R A] [Algebra R B]
(W : Submonoid A) {f g : Localization W →ₐ[R] B}
(h : f.comp (Algebra.algHom R A _) = g.comp (Algebra.algHom R A _)) : f = g :=
IsLocalization.algHom_ext W h
