English
A property P of ring homomorphisms is preserved if P holds for the map f whenever there exists a finite set of elements {r} spanning the target S, and P holds for the localized maps R → S_r for each r in the finite set.
Русский
Свойство P стойко сохраняется, если существует конечное множество элементов {r}, образующее базис охвата S, и P выполняется для локализаций R → S_r для каждого r из множества.
LaTeX
$$$\forall R,S\,[\text{CommutativeRing }R,...]\; (f:R\to S)\; (s:\mathrm{Finset}\;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.OfLocalizationFiniteSpanTarget`
if `P` holds for `R →+* S` whenever there exists a finite set `{ r }` that spans `S` such that
`P` holds for `R →+* Sᵣ`.
Note that this is equivalent to `RingHom.OfLocalizationSpanTarget` via
`RingHom.ofLocalizationSpanTarget_iff_finite`, but this is easier to prove. -/
def OfLocalizationFiniteSpanTarget : Prop :=
∀ ⦃R S : Type u⦄ [CommRing R] [CommRing S] (f : R →+* S) (s : Finset S) (_ : Ideal.span (s : Set S) = ⊤)
(_ : ∀ r : s, P ((algebraMap S (Localization.Away (r : S))).comp f)), P f
