English
If P respects isos, then stalkwise P is local and respects isomorphisms universally.
Русский
Если P сохраняет изоморфизмы, то stalkwise P локален и универсально сохраняет изоморфизмы.
LaTeX
$$stalkwiseIsZariskiLocalAtTarget_of_respectsIso$$
Lean4
/-- If `P` respects isos, then `stalkwise P` respects isos. -/
theorem stalkwise_respectsIso (hP : RingHom.RespectsIso P) : (stalkwise P).RespectsIso
where
precomp {X Y Z} e (he : IsIso e) f
hf := by
simp only [stalkwise, Scheme.comp_coeBase, TopCat.coe_comp, Function.comp_apply]
intro x
rw [Scheme.stalkMap_comp]
exact (RingHom.RespectsIso.cancel_right_isIso hP _ _).mpr <| hf (e.base x)
postcomp {X Y Z} e (he : IsIso _) f
hf := by
simp only [stalkwise, Scheme.comp_coeBase, TopCat.coe_comp, Function.comp_apply]
intro x
rw [Scheme.stalkMap_comp]
exact (RingHom.RespectsIso.cancel_left_isIso hP _ _).mpr <| hf x
