English
If there is a property Q on ring-localizations that is preserved by localization away from primes, and P is a HasRingHomProperty with Q, then P f is equivalent to the condition that for every x in X, the stalk-map at x satisfies Q.
Русский
Если существует свойство Q на локализации кол-м, сохраняемое локализацией вдали от простых идеалов, и P — HasRingHomProperty с Q, тогда P f эквивалентно условию, что для каждого x в X локальный stalk-map удовлетворяет Q.
LaTeX
$$$\forall x\in X,\; Q( f.stalkMap x ).hom$, given hf: P f.$$
Lean4
theorem locally_of_iff (hQl : LocalizationAwayPreserves Q) (hQa : StableUnderCompositionWithLocalizationAway Q)
(h :
∀ {X Y : Scheme.{u}} (f : X ⟶ Y),
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) :
HasRingHomProperty P (Locally Q)
where
isLocal_ringHomProperty := locally_propertyIsLocal hQl hQa
eq_affineLocally' :=
by
haveI : HasRingHomProperty (affineLocally (Locally Q)) (Locally Q) := ⟨locally_propertyIsLocal hQl hQa, rfl⟩
ext X Y f
rw [h, iff_exists_appLE_locally (P := affineLocally (Locally Q)) hQa.left hQa.respectsIso]
