English
If P is a morphism-property of schemes and Q is a ring-hom property stable under localization away from the source, then P f is equivalent to the existence, for affine opens U,V around each point, of a morphism appLE with Q-hom property.
Русский
Если P — свойство морфизмов схем, а Q — свойство колом гомоморфизмов, устойчивое к локализации от источника, то P(f) эквивалентно существованию афинных открытых множеств U,V вокруг каждой точки, такие что существует соответствующий appLE с свойством Q.
LaTeX
$$$\text{StableUnderCompositionWithLocalizationAwaySource } Q \Rightarrow (\text{RespectsIso } Q) \Rightarrow (P \text{ holds } f \iff \text{local existence of } U,V,e \text{ with } Q(f.appLE U V e).hom).$$$
Lean4
/-- If `P` is induced by `Locally Q`, it suffices to check `Q` on affine open sets locally around
points of the source. -/
theorem iff_exists_appLE_locally (hQ : RingHom.StableUnderCompositionWithLocalizationAwaySource Q) (hQi : RespectsIso Q)
[HasRingHomProperty P (Locally 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
have := respects_isOpenImmersion (P := P) (RingHom.locally_StableUnderCompositionWithLocalizationAwaySource hQ)
refine ⟨fun hf x ↦ ?_, fun hf ↦ (IsZariskiLocalAtSource.iff_exists_resLE (P := P)).mpr <| fun x ↦ ?_⟩
· obtain ⟨U, hU, hfx, _⟩ := Opens.isBasis_iff_nbhd.mp (isBasis_affine_open Y) (Opens.mem_top <| f.base x)
obtain ⟨V, hV, hx, e⟩ := Opens.isBasis_iff_nbhd.mp (isBasis_affine_open X) (show x ∈ f ⁻¹ᵁ U from hfx)
simp_rw [HasRingHomProperty.iff_appLE (P := P), locally_iff_isLocalization hQi] at hf
obtain ⟨s, hs, hfs⟩ := hf ⟨U, hU⟩ ⟨V, hV⟩ e
apply iSup_basicOpen_of_span_eq_top at hs
have : x ∈ (⨆ i ∈ s, X.basicOpen i) := hs.symm ▸ hx
have : ∃ r ∈ s, x ∈ X.basicOpen r := by simpa using this
obtain ⟨r, hr, hrs⟩ := this
refine ⟨⟨U, hU⟩, ⟨X.basicOpen r, hV.basicOpen r⟩, hrs, (X.basicOpen_le r).trans e, ?_⟩
rw [← f.appLE_map e (homOfLE (X.basicOpen_le r)).op]
haveI : IsLocalization.Away r Γ(X, X.basicOpen r) := hV.isLocalization_basicOpen r
exact hfs r hr _
· obtain ⟨U, V, hxV, e, hf⟩ := hf x
use U, V, hxV, e
simp only [iff_of_isAffine (P := P), Scheme.Hom.appLE, homOfLE_leOfHom] at hf ⊢
haveI : (toMorphismProperty (Locally Q)).RespectsIso :=
toMorphismProperty_respectsIso_iff.mp <| (isLocal_ringHomProperty P).respectsIso
exact
(MorphismProperty.arrow_mk_iso_iff (toMorphismProperty (Locally Q)) (arrowResLEAppIso f U V e)).mpr
(locally_of hQi _ hf)
