English
Definition: A property P of ring homomorphisms is Locally P if there exists a family of elements of the target S generating the unit ideal such that P holds after compositing with the localization away at each element.
Русский
Определение: свойство P кольмохомоморфизмов является Locally P, если существует семейство элементов целевого кольца S, порождающих единичную идеал, и для каждого элемента свойство P сохраняется после композиции с локализацией на этот элемент.
LaTeX
$$$\text{Locally}(P,f) := \exists s: \text{Set } S, \ \operatorname{span}(s)=\top \land \forall t\in s,\ P((algebraMap S (Localization.Away t)).\circ f).$$$
Lean4
/-- For a property of ring homomorphisms `P`, `Locally P` holds for `f : R →+* S` if
it holds locally on `S`, i.e. if there exists a subset `{ t }` of `S` generating
the unit ideal, such that `P` holds for all compositions `R →+* Sₜ`.
We may require `s` to be finite here, for the equivalence, see `locally_iff_finite`.
-/
def Locally {R S : Type u} [CommRing R] [CommRing S] (f : R →+* S) : Prop :=
∃ (s : Set S) (_ : Ideal.span s = ⊤), ∀ t ∈ s, P ((algebraMap S (Localization.Away t)).comp f)
