English
Let P be a property of ring homomorphisms that respects isomorphisms and is local on the target; then for every ring homomorphism f, Locally P f holds if and only if P f holds.
Русский
Пусть P — свойство гомоморфизмов колец, сохраняющее изоморфизмы и локальное относительно целевого кольца; тогда для любого гомоморфизма f верно, что Locally P f тогда и только тогда, когда P f.
LaTeX
$$$\forall P\,\big(\operatorname{RespectsIso} P \wedge \operatorname{OfLocalizationSpanTarget} P\big) \Rightarrow \forall R S [\mathrm{CommRing} R] [\mathrm{CommRing} S] (f : R \to+* S),\ Locally P f \leftrightarrow P f.$$$
Lean4
/-- If `P` is local on the target, then `Locally P` coincides with `P`. -/
theorem locally_iff_of_localizationSpanTarget (hPi : RespectsIso P) (hPs : OfLocalizationSpanTarget P) {R S : Type u}
[CommRing R] [CommRing S] (f : R →+* S) : Locally P f ↔ P f :=
⟨fun ⟨s, hsone, hs⟩ ↦ hPs f s hsone (fun a ↦ hs a.val a.property), locally_of hPi f⟩
