English
IsSeparated is Zariski-local on the target. In particular, the property IsSeparated is local with respect to Zariski covers of the target scheme.
Русский
IsSeparated локально по Zariski-объему на цели; свойство IsSeparated локально по Zariski-объёму на целевой схеме.
LaTeX
$$$\text{IsSeparated} \text{ is IsZariskiLocalAtTarget}. $$$
Lean4
/-- If `Q` is a property of ring maps that can be checked on prime ideals, the
associated property of scheme morphisms can be checked on stalks. -/
theorem of_stalkMap (hQ : OfLocalizationPrime Q) (H : ∀ x, Q (f.stalkMap x).hom) : P f :=
by
have hQi := (HasRingHomProperty.isLocal_ringHomProperty P).respectsIso
wlog hY : IsAffine Y generalizing X Y f
· rw [IsZariskiLocalAtTarget.iff_of_iSup_eq_top (P := P) _ (iSup_affineOpens_eq_top _)]
intro U
refine this (fun x ↦ ?_) U.2
exact (hQi.arrow_mk_iso_iff (AlgebraicGeometry.morphismRestrictStalkMap f U x)).mpr (H x.val)
wlog hX : IsAffine X generalizing X f
· rw [IsZariskiLocalAtSource.iff_of_iSup_eq_top (P := P) _ (iSup_affineOpens_eq_top _)]
intro U
refine this ?_ U.2
intro x
rw [Scheme.stalkMap_comp, CommRingCat.hom_comp, hQi.cancel_right_isIso]
exact H x.val
wlog hXY : ∃ R S, Y = Spec R ∧ X = Spec S generalizing X Y
· rw [← P.cancel_right_of_respectsIso (g := Y.isoSpec.hom)]
rw [← P.cancel_left_of_respectsIso (f := X.isoSpec.inv)]
refine this inferInstance (fun x ↦ ?_) inferInstance ?_
· rw [Scheme.stalkMap_comp, Scheme.stalkMap_comp, CommRingCat.hom_comp, hQi.cancel_right_isIso,
CommRingCat.hom_comp, hQi.cancel_left_isIso]
apply H
· use Γ(Y, ⊤), Γ(X, ⊤)
obtain ⟨R, S, rfl, rfl⟩ := hXY
obtain ⟨φ, rfl⟩ := Spec.map_surjective f
rw [Spec_iff (P := P)]
apply hQ
intro P hP
specialize H ⟨P, hP⟩
rwa [hQi.arrow_mk_iso_iff (Scheme.arrowStalkMapSpecIso φ _)] at H
