English
If P is preserved by localization away, then Locally P is preserved by localization away as well.
Русский
Если P сохраняется под локализацией Away, то Locally P сохраняется подAway.
LaTeX
$$$\operatorname{LocalizationAwayPreserves}(P) \Rightarrow \operatorname{LocalizationAwayPreserves}(\Locally P).$$$
Lean4
/-- If `P` is preserved by localization away, then so is `Locally P`. -/
theorem locally_localizationAwayPreserves (hPl : LocalizationAwayPreserves P) : LocalizationAwayPreserves (Locally P) :=
by
introv R hf
obtain ⟨s, hsone, hs⟩ := hf
rw [locally_iff_exists hPl.respectsIso]
let rₐ (a : s) : Localization.Away a.val := algebraMap _ _ (f r)
let Sₐ (a : s) := Localization.Away (rₐ a)
haveI (a : s) : IsLocalization.Away (((algebraMap S (Localization.Away a.val)).comp f) r) (Sₐ a) :=
inferInstanceAs (IsLocalization.Away (rₐ a) (Sₐ a))
haveI (a : s) :
IsLocalization (Algebra.algebraMapSubmonoid (Localization.Away a.val) (Submonoid.map f (Submonoid.powers r)))
(Sₐ a) :=
by
convert inferInstanceAs (IsLocalization.Away (rₐ a) (Sₐ a))
simp [rₐ, Algebra.algebraMapSubmonoid]
have H (a : s) : Submonoid.powers (f r) ≤ (Submonoid.powers (rₐ a)).comap (algebraMap S (Localization.Away a.val)) :=
by simp [rₐ, Submonoid.powers_le]
letI (a : s) : Algebra S' (Sₐ a) :=
(IsLocalization.map (Sₐ a) (algebraMap S (Localization.Away a.val)) (H a)).toAlgebra
haveI (a : s) : IsScalarTower S S' (Sₐ a) := IsScalarTower.of_algebraMap_eq' (IsLocalization.map_comp (H a)).symm
refine ⟨s, fun a ↦ algebraMap S S' a.val, ?_, Sₐ, inferInstance, inferInstance, fun a ↦ ?_, fun a ↦ ?_⟩
· rw [← Set.image_eq_range, ← Ideal.map_span, hsone, Ideal.map_top]
· convert
IsLocalization.commutes (T := Sₐ a) (M₁ := (Submonoid.powers r).map f) (S₁ := S') (S₂ := Localization.Away a.val)
(M₂ := Submonoid.powers a.val)
simp [Algebra.algebraMapSubmonoid]
· rw [algebraMap_toAlgebra, IsLocalization.Away.map, IsLocalization.map_comp_map]
exact hPl ((algebraMap _ (Localization.Away a.val)).comp f) r R' (Sₐ a) (hs _ a.2)
