English
If P holds for localization away maps, then Locally P holds as well.
Русский
Если P выполняется для локализации черезAway, то Locally P выполняется также.
LaTeX
$$$\operatorname{HoldsForLocalizationAway}(P) \Rightarrow \operatorname{HoldsForLocalizationAway}(\Locally P).$$$
Lean4
/-- If `P` holds for localization away maps, then so does `Locally P`. -/
theorem locally_holdsForLocalizationAway (hPa : HoldsForLocalizationAway P) : HoldsForLocalizationAway (Locally P) :=
by
introv R _
use { 1 }
simp only [Set.mem_singleton_iff, forall_eq, Ideal.span_singleton_one, exists_const]
let e : S ≃ₐ[R] (Localization.Away (1 : S)) :=
(IsLocalization.atUnits S (Submonoid.powers 1) (by simp)).restrictScalars R
haveI : IsLocalization.Away r (Localization.Away (1 : S)) :=
IsLocalization.isLocalization_of_algEquiv (Submonoid.powers r) e
rw [← IsScalarTower.algebraMap_eq]
apply hPa _ r
