away — Mathlib

English

If a property P is preserved under localization, then there is a corresponding way to descend to localization away preserving P.

Русский

Если свойство P сохраняется при локализации, существует соответствующий способ переноса на локализацию away, сохраняющий P.

LaTeX

$$$\\text{LocalizationPreserves }P \\to \\text{LocalizationAwayPreserves }P$$$

Lean4

theorem away (H : RingHom.LocalizationPreserves @P) : RingHom.LocalizationAwayPreserves P :=
  by
  intro R S _ _ f r R' S' _ _ _ _ _ _ hf
  have : IsLocalization ((Submonoid.powers r).map f) S' := by rw [Submonoid.map_powers]; assumption
  exact H f (Submonoid.powers r) R' S' hf

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