English
A property P of ring homomorphisms holds for R → S whenever there exists a set s ⊂ S with span s = ⊤ and P holds for R → S_r for all r ∈ s.
Русский
Свойство P гомоморфизмов кольца сохраняется для R → S, если существует множество элементов s в S со span s = ⊤ и P выполняется для R → S_r для всех r ∈ s.
LaTeX
$$$\forall R,S\,[\mathrm{CommRing} R][\mathrm{CommRing} S](f:R\to S)(s:\mathrm{Set} S)(h:\mathrm{Ideal.span}(s)=\top)\; (\forall r\in s, P((\mathrm{algebraMap}\;S\,(\mathrm{Localization.Away}\,r)).\circ f))\Rightarrow P(f)$$
Lean4
/-- A property `P` of ring homs satisfies `RingHom.OfLocalizationSpanTarget`
if `P` holds for `R →+* S` whenever there exists a set `{ r }` that spans `S` such that
`P` holds for `R →+* Sᵣ`.
Note that this is equivalent to `RingHom.OfLocalizationFiniteSpanTarget` via
`RingHom.ofLocalizationSpanTarget_iff_finite`, but this has less restrictions when applying. -/
def OfLocalizationSpanTarget : Prop :=
∀ ⦃R S : Type u⦄ [CommRing R] [CommRing S] (f : R →+* S) (s : Set S) (_ : Ideal.span s = ⊤)
(_ : ∀ r : s, P ((algebraMap S (Localization.Away (r : S))).comp f)), P f
