English
A property P of ring homs is preserved by localization away if P holds for R → S whenever P holds for the same map in localized form away from a specific element.
Русский
Свойство P гомоморфов сохраняется при локализацииAway, если P выполняется для R → S, когда P выполняется для локализованной формы вдали от элемента.
LaTeX
$$$\\text{StableUnderCompositionWithLocalizationAwaySource} P$ and similar for target; $P(f) \\Rightarrow P(g)$ for localized maps.$$
Lean4
/-- A property `P` of ring homs is said to be preserved by localization away
if `P` holds for `Rᵣ →+* Sᵣ` whenever `P` holds for `R →+* S`. -/
def LocalizationAwayPreserves :=
∀ ⦃R S : Type u⦄ [CommRing R] [CommRing S] (f : R →+* S) (r : R) (R' S' : Type u) [CommRing R'] [CommRing S']
[Algebra R R'] [Algebra S S'] [IsLocalization.Away r R'] [IsLocalization.Away (f r) S'],
P f → P (IsLocalization.Away.map R' S' f r : R' →+* S')
