English
A property P of ring homs is preserved by localization if P holds for R → S implies P holds for the localized map after localization at M.
Русский
Свойство P гомоморфизмов сохраняется после локализации, если P выполняется для R → S, тогда P выполняется для локализованного отображения после локализации по M.
LaTeX
$$$\\forall \\text{f}, M, R', S', \\; P(f) \\Rightarrow P(\\text{Localization.map } S' f \\; (\\text{Submonoid.le_comap_map } M)).$$$
Lean4
/-- A property `P` of ring homs is said to be preserved by localization
if `P` holds for `M⁻¹R →+* M⁻¹S` whenever `P` holds for `R →+* S`. -/
def LocalizationPreserves :=
∀ ⦃R S : Type u⦄ [CommRing R] [CommRing S] (f : R →+* S) (M : Submonoid R) (R' S' : Type u) [CommRing R']
[CommRing S'] [Algebra R R'] [Algebra S S'] [IsLocalization M R'] [IsLocalization (M.map f) S'],
P f → P (IsLocalization.map S' f (Submonoid.le_comap_map M) : R' →+* S')
