English
Locally P f is equivalent to the existence of a finite localization data for every t with IsLocalization.Away, yielding P on the composed maps.
Русский
Locally P f эквивалентно существованию конечного набора локализаций с IsLocalization.Away, дающих P после композиции.
LaTeX
$$$\text{Locally }P f \iff \exists s:(\text{Finset }S)\;\forall t\in s\; (IsLocalization.Away\; t)\Rightarrow P((algebraMap S (S_t)).\circ f).$$$
Lean4
/-- In the definition of `Locally` we may replace `Localization.Away` with an arbitrary
algebra satisfying `IsLocalization.Away`. -/
theorem locally_iff_isLocalization (hP : RespectsIso P) (f : R →+* S) :
Locally P f ↔
∃ (s : Finset S) (_ : Ideal.span (s : Set S) = ⊤),
∀ t ∈ s,
∀ (Sₜ : Type u) [CommRing Sₜ] [Algebra S Sₜ] [IsLocalization.Away t Sₜ], P ((algebraMap S Sₜ).comp f) :=
by
rw [locally_iff_finite P f]
refine ⟨fun ⟨s, hsone, hs⟩ ↦ ⟨s, hsone, fun t ht Sₜ _ _ _ ↦ ?_⟩, fun ⟨s, hsone, hs⟩ ↦ ?_⟩
· let e : Localization.Away t ≃+* Sₜ := (IsLocalization.algEquiv (Submonoid.powers t) _ _).toRingEquiv
have : algebraMap S Sₜ = e.toRingHom.comp (algebraMap S (Localization.Away t)) :=
RingHom.ext (fun x ↦ (AlgEquiv.commutes (IsLocalization.algEquiv _ _ _) _).symm)
rw [this, RingHom.comp_assoc]
exact hP.left _ _ (hs t ht)
· exact ⟨s, hsone, fun t ht ↦ hs t ht _⟩
