English
Let P be a property of ring homomorphisms that respects isomorphisms. For any φ: R → S, the Spec-map φ is stalkwise for P if and only if for every prime ideal p of S, the induced localization morphism Localizations at p satisfies P.
Русский
Пусть P – свойство гомоморфизмов колец, сохраняющее изоморфизмы. Для любого отображения φ: R → S отображение Spec φ является локальным по точкам для P тогда и только тогда, когда для каждого простого идеала p в S соответствующее локализующее гомоморфизм локализации в p удовлетворяет P.
LaTeX
$$$\\text{stalkwise } P\\,(\\mathrm{Spec.map}\\ φ) \\iff \\forall (p : \\mathrm{Ideal}\ S) \\,(p.IsPrime)\\; P\\bigl(\\mathrm{Localization.localRingHom}\\ _\\; p\\; φ.hom\\; rfl\\bigr)$$$
Lean4
theorem stalkwise_Spec_map_iff (hP : RingHom.RespectsIso P) {R S : CommRingCat} (φ : R ⟶ S) :
stalkwise P (Spec.map φ) ↔ ∀ (p : Ideal S) (_ : p.IsPrime), P (Localization.localRingHom _ p φ.hom rfl) :=
by
have hP' : (RingHom.toMorphismProperty P).RespectsIso := RingHom.toMorphismProperty_respectsIso_iff.mp hP
trans ∀ (p : PrimeSpectrum S), P (Localization.localRingHom _ p.asIdeal φ.hom rfl)
· exact forall_congr' fun p ↦ (RingHom.toMorphismProperty P).arrow_mk_iso_iff (Scheme.arrowStalkMapSpecIso _ _)
· exact ⟨fun H p hp ↦ H ⟨p, hp⟩, fun H p ↦ H p.1 p.2⟩
