awayToAwayRight — Mathlib

English

Similarly, for y ∈ R, awayToAwayRight y: S → P is defined using the universal lift for the localization away from x·y.

Русский

Аналогично, для y ∈ R отображение awayToAwayRight y: S → P задаётся через универсальный lift локализации away от x·y.

LaTeX

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

Lean4

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

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