lift_injective_iff — Mathlib

English

The lift is injective if and only if for all x,y ∈ R, algebraMap_R_S x = algebraMap_R_S y iff g(x) = g(y).

Русский

Лифт инъективен тогда и только тогда, когда для любых x,y ∈ R равенство algebraMap_R_S x = algebraMap_R_S y эквивалентно g(x) = g(y).

LaTeX

$$$ \\mathrm{Injective}(\\mathrm{lift}\\;hg) \\iff \\forall x,y, \\ algebraMap_{R,S}(x) = algebraMap_{R,S}(y) \\iff g(x)=g(y). $$$

Lean4

theorem lift_injective_iff : Injective (lift hg : S → P) ↔ ∀ x y, algebraMap R S x = algebraMap R S y ↔ g x = g y :=
  (toLocalizationMap M S).lift_injective_iff hg

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