English
Isomorphisms of schemes can be characterized stalkwise: an isomorphism is precisely a morphism whose underlying ring maps are bijective on all stalks and locally an iso.
Русский
Изоморфизм схем характеризуется по стержням: отображение является изоморфизмом тогда и только тогда, когда соответствующие отображения на стержнях биективны и локально являются изоморфизмами.
LaTeX
$$isomorphisms Scheme = inverseImage forgetToTop ∧ stalkwise bijectivity$$
Lean4
theorem isomorphisms_eq_stalkwise :
isomorphisms Scheme =
(isomorphisms TopCat).inverseImage Scheme.forgetToTop ⊓ stalkwise (fun f ↦ Function.Bijective f) :=
by
rw [isomorphisms_eq_isOpenImmersion_inf_surjective, isOpenImmersion_eq_inf, surjective_eq_topologically,
inf_right_comm]
congr 1
ext X Y f
exact
⟨fun H ↦ inferInstanceAs (IsIso (TopCat.isoOfHomeo (H.1.1.toHomeomorphOfSurjective H.2)).hom),
fun (_ : IsIso f.base) ↦
let e := (TopCat.homeoOfIso <| asIso f.base);
⟨e.isOpenEmbedding, e.surjective⟩⟩
