awayToAwayLeft — Mathlib

English

For y ∈ R, the map awayToAwayLeft y: S → P is defined using the universal lift for the localization away from x.

Русский

Для элементa y ∈ R отображение awayToAwayLeft y: S → P задаётся через универсальный lift локализации away от x.

LaTeX

$$$\\text{awayToAwayLeft} : S \\to P$ is defined by\\; z \\mapsto \\text{lift}\\; x\\; (\\text{isUnit_of_dvd}(y\\,x))\\big(z\\big)$$$

Lean4

/-- Given `x y : R` and localizations `S`, `P` away from `x` and `y * x`
respectively, the homomorphism induced from `S` to `P`. -/
noncomputable def awayToAwayLeft (y : R) [Algebra R P] [IsLocalization.Away (y * x) P] : S →+* P :=
  lift x <| isUnit_of_dvd (y * x) (dvd_mul_left _ _)

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