Isomorphisms of K-local-ringed spaces through the base and the stalks #
A morphism of locally ringed spaces whose underlying map is a homeomorphism and whose stalk maps
are all bijective is an isomorphism: the sheaf component f.c : ๐ช_Y โถ f_* ๐ช_X is an isomorphism
of sheaves because its stalk maps are (TopCat.Presheaf.isIso_of_stalkFunctor_map_iso, the stalk
of f_* ๐ช_X at f x being the stalk of ๐ช_X at x for a homeomorphism f), so f is an
isomorphism of presheafed spaces (PresheafedSpace.isIso_of_components), hence of sheafed and of
locally ringed spaces (the forgetful functors reflect isomorphisms). The criterion recognises the
K-isomorphism (G', ๐_{G'}) โ
X|V at a simple point [Hir64, Ch. 0, ยง1, p. 121] from its
stalks, and identifies a space with a coproduct (Hironaka/AnalyticSpace/SigmaLemmas.lean).
LocallyRingedSpace.isIso_of_isIso_base_of_stalkMap_bijective;KLocallyRingedSpace.isIso_of_isIso_base_of_stalkMap_bijective(throughisIso_of_isIso_val).
A morphism of locally ringed spaces with a homeomorphism as base map (an isomorphism in
TopCat) and bijective stalk maps is an isomorphism.
A K-morphism with a homeomorphism as base map and bijective stalk maps is a K-isomorphism
(isIso_of_isIso_val: a K-morphism whose underlying morphism is an isomorphism is one).