English
If topological property holds for all base maps, then it holds for morphisms over schemes.
Русский
Если топологическое свойство выполняется для всех базовых отображений, то оно выполняется и для морфизмов схем.
LaTeX
$$topologically_isZariskiLocalAtTarget$$
Lean4
/-- If `P` respects isos, then `stalkwise P` is local at the target. -/
theorem stalkwiseIsZariskiLocalAtTarget_of_respectsIso (hP : RingHom.RespectsIso P) :
IsZariskiLocalAtTarget (stalkwise P) :=
by
have hP' : (RingHom.toMorphismProperty P).RespectsIso := RingHom.toMorphismProperty_respectsIso_iff.mp hP
letI := stalkwise_respectsIso hP
apply IsZariskiLocalAtTarget.mk'
· intro X Y f U hf x
apply ((RingHom.toMorphismProperty P).arrow_mk_iso_iff <| morphismRestrictStalkMap f U x).mpr <| hf _
· intro X Y f ι U hU hf x
have hy : f.base x ∈ iSup U := by rw [hU]; trivial
obtain ⟨i, hi⟩ := Opens.mem_iSup.mp hy
exact
((RingHom.toMorphismProperty P).arrow_mk_iso_iff <| morphismRestrictStalkMap f (U i) ⟨x, hi⟩).mp <| hf i ⟨x, hi⟩
