English
A property P of ring homs holds for R → S whenever there exists a finite spanning set {r} of S such that P holds for R → S_r.
Русский
Свойство P гомоморфизмов кольца выполняется для R → S, если существует конечный порождающий набор {r} для S такой, что P выполняется для R → S_r.
LaTeX
$$$\\forall \\text{finite spanning set } s \\subseteq S, \\; P(f) \\Rightarrow P(\\text{Localization Away map for each } r \\in s).$$$
Lean4
/-- A property `P` of ring homs satisfies `RingHom.OfLocalizationFiniteSpan`
if `P` holds for `R →+* S` whenever there exists a finite set `{ r }` that spans `R` such that
`P` holds for `Rᵣ →+* Sᵣ`.
Note that this is equivalent to `RingHom.OfLocalizationSpan` via
`RingHom.ofLocalizationSpan_iff_finite`, but this is easier to prove. -/
def OfLocalizationFiniteSpan :=
∀ ⦃R S : Type u⦄ [CommRing R] [CommRing S] (f : R →+* S) (s : Finset R) (_ : Ideal.span (s : Set R) = ⊤)
(_ : ∀ r : s, P (Localization.awayMap f r)), P f
