English
Two algebra homomorphisms from a localization are equal if they agree after precomposing with the canonical algebra map from the base ring.
Русский
Два гомоморфизма алгебр из локализации равны, если они совпадают после предварительного композиирования с каноническим отображением из базовой кольцевой структуры.
LaTeX
$$$\\forall f,g: L \\to_{\\!R} B,\\; f \\circ (\\mathrm{Algebra.algHom}\\; R\\; A\\; L) = g \\circ (\\mathrm{Algebra.algHom}\\; R\\; A\\; L) \\Rightarrow f = g$$$
Lean4
theorem algHom_ext {R A L B : Type*} [CommSemiring R] [CommSemiring A] [CommSemiring L] [Semiring B] (W : Submonoid A)
[Algebra A L] [IsLocalization W L] [Algebra R A] [Algebra R L] [IsScalarTower R A L] [Algebra R B] {f g : L →ₐ[R] B}
(h : f.comp (Algebra.algHom R A L) = g.comp (Algebra.algHom R A L)) : f = g :=
AlgHom.coe_ringHom_injective <| IsLocalization.ringHom_ext W <| RingHom.ext <| AlgHom.ext_iff.mp h
