English
Equivalence: Locally P f is equivalent to the existence of a finite subset of S whose span is the unit ideal, together with a compatible family of local checks.
Русский
Эквивалентность: Locally P f эквивалентно существованию конечного подмножества S, чья линейная оболочка даёт единичную идею, совместно с соответствующей локальной проверкой.
LaTeX
$$$\text{Locally }P(f) \iff \exists\ s:\Finset S, \ \operatorname{span}(s)=\top \land \forall t\in s,\ P((algebraMap S (Localization.Away t)).\circ f).$$$
Lean4
theorem locally_iff_finite (f : R →+* S) :
Locally P f ↔
∃ (s : Finset S) (_ : Ideal.span (s : Set S) = ⊤), ∀ t ∈ s, P ((algebraMap S (Localization.Away t)).comp f) :=
by
constructor
· intro ⟨s, hsone, hs⟩
obtain ⟨s', h₁, h₂⟩ := (Ideal.span_eq_top_iff_finite s).mp hsone
exact ⟨s', h₂, fun t ht ↦ hs t (h₁ ht)⟩
· intro ⟨s, hsone, hs⟩
use s, hsone, hs
