English
If localization away from the source preserves Q and composition with localization away preserves Q, and for every X→Y the P-property is equivalent to the local appLE condition, then HasRingHomProperty P for Locally Q holds.
Русский
Если локализация вдали от источника сохраняет Q и композиция с локализацией также сохраняет Q, и для каждого X→Y свойство P эквивалентно локальному условию appLE, то HasRingHomProperty P (Locally Q) выполняется.
LaTeX
$$$(\text{RingHom.LocalizationAwayPreserves } Q) \land (\text{RingHom.StableUnderCompositionWithLocalizationAway } Q) \land (\forall X,Y, f, P f \iff \forall x,\exists U,V,e, Q(f.appLE U V e).hom) \Rightarrow \text{HasRingHomProperty } P (\text{Locally } Q).$$$
Lean4
/-- `P` can be checked locally around points of the source. -/
theorem iff_exists_appLE (hQ : StableUnderCompositionWithLocalizationAwaySource Q) :
P f ↔
∀ (x : X), ∃ (U : Y.affineOpens) (V : X.affineOpens) (_ : x ∈ V.1) (e : V.1 ≤ f ⁻¹ᵁ U.1), Q (f.appLE U V e).hom :=
by
haveI inst : HasRingHomProperty P Q := inferInstance
haveI : HasRingHomProperty P (Locally Q) :=
by
apply @copy (P := P) (P' := P) (Q := Q) (Q' := Locally Q)
· infer_instance
· rfl
· intro R S _ _ f
exact
(locally_iff_of_localizationSpanTarget (isLocal_ringHomProperty P).respectsIso
(isLocal_ringHomProperty P).ofLocalizationSpanTarget _).symm
rw [iff_exists_appLE_locally (P := P) hQ]
haveI : HasRingHomProperty P Q := inst
apply (isLocal_ringHomProperty P (Q := Q)).respectsIso
