English
Equivalence: Locally P f is equivalent to the existence of a cover by algebras S_t with isLocalization, and for each t, P holds after composing with the corresponding map.
Русский
Эквивалентность: Locally P f эквивалентно существованию покрытия алгебр S_t с изоляцией и тем, что для каждого t выполняется P.
LaTeX
$$$\text{Locally }P(f) \iff \exists \iota,\ s:\iota \to S,\text{...},\forall i,\IsLocalization.Away (s i)\, S_i,\ P( (algebraMap S S_i) \circ f).$$$
Lean4
/-- Equivalence variant of `locally_of_exists`. This is sometimes easier to use, if the
`IsLocalization.Away` instance can't be automatically inferred. -/
theorem locally_iff_exists (hP : RespectsIso P) (f : R →+* S) :
Locally P f ↔
∃ (ι : Type u) (s : ι → S) (_ : Ideal.span (Set.range s) = ⊤) (Sₜ : ι → Type u) (_ : (i : ι) → CommRing (Sₜ i)) (_
: (i : ι) → Algebra S (Sₜ i)) (_ : (i : ι) → IsLocalization.Away (s i : S) (Sₜ i)),
∀ i, P ((algebraMap S (Sₜ i)).comp f) :=
⟨fun ⟨s, hsone, hs⟩ ↦
⟨s, fun t : s ↦ (t : S), by simpa, fun t ↦ Localization.Away (t : S), inferInstance, inferInstance, inferInstance,
fun t ↦ hs t.val t.property⟩,
fun ⟨ι, s, hsone, Sₜ, _, _, hislocal, hs⟩ ↦ locally_of_exists hP f s hsone Sₜ hs⟩
