English
If P is preserved by localizations, then Locally P is preserved by localizations.
Русский
Если P сохраняется локализациями, то Locally P сохраняется локализациями.
LaTeX
$$$\operatorname{LocalizationPreserves}(P) \Rightarrow \operatorname{LocalizationPreserves}(\Locally P).$$$
Lean4
/-- If `P` is preserved by localizations, then so is `Locally P`. -/
theorem locally_localizationPreserves (hPl : LocalizationPreserves P) : LocalizationPreserves (Locally P) :=
by
introv R hf
obtain ⟨s, hsone, hs⟩ := hf
rw [locally_iff_exists hPl.away.respectsIso]
let Mₐ (a : s) : Submonoid (Localization.Away a.val) := (M.map f).map (algebraMap S (Localization.Away a.val))
let Sₐ (a : s) := Localization (Mₐ a)
have hM (a : s) : M.map ((algebraMap S (Localization.Away a.val)).comp f) = Mₐ a := (M.map_map _ _).symm
haveI (a : s) : IsLocalization (M.map ((algebraMap S (Localization.Away a.val)).comp f)) (Sₐ a) :=
by
rw [hM]
infer_instance
haveI (a : s) : IsLocalization (Algebra.algebraMapSubmonoid (Localization.Away a.val) (M.map f)) (Sₐ a) :=
inferInstanceAs <| IsLocalization (Mₐ a) (Sₐ a)
letI (a : s) : Algebra S' (Sₐ a) :=
(IsLocalization.map (Sₐ a) (algebraMap S (Localization.Away a.val)) (M.map f).le_comap_map).toAlgebra
haveI (a : s) : IsScalarTower S S' (Sₐ a) :=
IsScalarTower.of_algebraMap_eq' (IsLocalization.map_comp (M.map f).le_comap_map).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₁ := M.map f) (S₁ := S') (S₂ := Localization.Away a.val) (M₂ :=
Submonoid.powers a.val)
simp [Algebra.algebraMapSubmonoid]
· rw [algebraMap_toAlgebra, IsLocalization.map_comp_map]
apply hPl
exact hs a.val a.property
