algHom_subsingleton — Mathlib

English

There is at most one R-algebra hom from the localization S to P compatible with units on M.

Русский

Единичность отображения Алгебры: существует не более одного гомоморфизма локализации S в P, совместимого с единицами на M.

LaTeX

$$$\\#\\bigl(\\mathrm{AlgHom}\\_R(S, P)\\bigr) = 1$$$

Lean4

theorem algHom_subsingleton [Algebra R P] : Subsingleton (S →ₐ[R] P) :=
  ⟨fun f g =>
    AlgHom.coe_ringHom_injective <| IsLocalization.ringHom_ext M <| by rw [f.comp_algebraMap, g.comp_algebraMap]⟩

Похожие утверждения