awayLift — Mathlib

English

Given a ring map f: R →+* P and an element r ∈ R with f(r) invertible, there exists a canonical map from Localization.Away r to P extending f.

Русский

Существет каноническое отображение от локализации Away r к P, продолжающее отображение f при условии, что f(r) обратимо.

LaTeX

$$$\text{AwayLift } f r : \text{Localization.Away } r \to+* P$$$

Lean4

/-- Given a map `f : R →+* S` and an element `r : R`, such that `f r` is invertible,
  we may construct a map `Rᵣ →+* S`. -/
noncomputable abbrev awayLift (f : R →+* P) (r : R) (hr : IsUnit (f r)) : Localization.Away r →+* P :=
  IsLocalization.Away.lift r hr

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