localRingHom_unique — Mathlib

English

Uniqueness of a local ring homomorphism given its restriction on the base ring.

Русский

Уникальность локального гомоморфизма, заданного на базовом кольце.

LaTeX

$$$\text{localRingHom} I K f hIJ = j \implies j$ is determined by its action on $R$.$$

Lean4

theorem localRingHom_unique (J : Ideal P) [J.IsPrime] (f : R →+* P) (hIJ : I = J.comap f)
    {j : Localization.AtPrime I →+* Localization.AtPrime J}
    (hj : ∀ x : R, j (algebraMap _ _ x) = algebraMap _ _ (f x)) : localRingHom I J f hIJ = j :=
  map_unique _ _ hj

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