lift_unique — Mathlib

English

If a ring homomorphism j: S → P agrees with g on the base ring under algebraMap, then lift hg = j; uniqueness of the lift.

Русский

Если гомоморфизм j: S → P совпадает с g на базовом кольце через algebraMap, то lift hg = j; уникальность подъема.

LaTeX

$$$ \\text{If } \\forall x, \\ j((\\mathrm{algebraMap}_{R,S}) x) = g(x) \\text{ then } \\mathrm{lift}\\;hg = j. $$$

Lean4

theorem lift_unique {j : S →+* P} (hj : ∀ x, j ((algebraMap R S) x) = g x) : lift hg = j :=
  RingHom.ext <|
    (DFunLike.ext_iff (F := MonoidHom _ _)).1 <|
      Submonoid.LocalizationMap.lift_unique (toLocalizationMap M S) (g := g.toMonoidHom) hg (j := j.toMonoidHom) hj

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