Isomorphisms over an open set: from points and stalks

Three general tools for the predicate f.IsIsoOver U := IsIso (f.restrictSet U) (condition (2) of a resolution in [Hir64, Introduction]; [Kol07, Theorem 45 (2)]), used to show that the local resolution map is an isomorphism over the simple locus and wherever that clause is used:

• AnalyticSpace.Hom.restrictSet_eq_restrictTo: the restriction f | f⁻¹V of the vocabulary is Hom.restrictTo at the opens openOf, definitionally — the bridge from the predicate to the local-isomorphism vocabulary of Hironaka/AnalyticSpace/LocalIso.lean;
• AnalyticSpace.isIso_restrictTo_of_bijOn_of_bijective_stalkMap: a morphism of analytic K-spaces which is bijective from U onto V and has bijective stalk maps at the points of U is a K-isomorphism X | U ≅ Y | V — the local isomorphisms of exists_isIso_restrictTo_of_bijective_stalkMap make the base map open, so it is a homeomorphism, and the criterion isIso_of_isIso_base_of_stalkMap_bijective applies;
• QuotientSpace.fiberMap_bijective_of_stalkIdeal_eq_map: the fibre map of a compatible pair of ideal sheaves is bijective at a point where the stalk map is bijective and the target ideal is the image of the source ideal — fiberMap_comap_bijective of Hironaka/AnalyticSpace/QuotientMap.lean with the stalkwise hypothesis in place of J' = comap φ J (for a strict transform, equal to the pullback only off the exceptional locus).

Routine (general topology and the two criteria). Used by Hironaka/AnalyticSpace/IsoOverCover.lean, Hironaka/Resolution/Analytic/Kol07Thm45/IsoOverLemmas.lean, Hironaka/Resolution/Analytic/Kol07Thm45/RestrictSetIncl.lean and Hironaka/Manifold/Sequence/.

theorem AnalyticSpace.QuotientSpace.fiberMap_bijective_of_stalkIdeal_eq_map {X' X : AlgebraicGeometry.LocallyRingedSpace} (φ : X' ⟶ X) (J' : Manifold.IdealSheaf X'.𝒪) (J : Manifold.IdealSheaf X.𝒪) (h : Compat φ J' J) (z' : ↑(support X' J')) (hb : Function.Bijective ⇑(CommRingCat.Hom.hom (AlgebraicGeometry.LocallyRingedSpace.Hom.stalkMap φ ↑z'))) (heq : stalkIdeal X' J' ↑z' = Ideal.map (CommRingCat.Hom.hom (AlgebraicGeometry.LocallyRingedSpace.Hom.stalkMap φ ↑z')) (stalkIdeal X J ((CategoryTheory.ConcreteCategory.hom φ.base) ↑z'))) : Function.Bijective ⇑(fiberMap φ J' J h z')

The induced map of fibres 𝒪_{X,φ z'}/𝒥_{φ z'} → 𝒪_{X',z'}/𝒥'_{z'} of a compatible pair is bijective at a point where the stalk map of φ is bijective and 𝒥'_{z'} is the image of 𝒥_{φ z'} (the proof of fiberMap_comap_bijective, with the stalkwise hypothesis).

theorem AnalyticSpace.Hom.mapsTo_openOf {K : Type} [RCLike K] {X Y : AnalyticSpace K} (f : X ⟶ Y) (V : Set ↑↑Y.toPresheafedSpace) (a : ↑↑X.toPresheafedSpace) : a ∈ X.openOf (KLocallyRingedSpace.Hom.toFun f ⁻¹' V) → KLocallyRingedSpace.Hom.toFun f a ∈ Y.openOf V

The lift condition of the restriction Hom.restrictSet, in the form Hom.restrictTo takes it: f maps openOf X (f⁻¹V) into openOf Y V.

theorem AnalyticSpace.Hom.restrictSet_eq_restrictTo {K : Type} [RCLike K] {X Y : AnalyticSpace K} (f : X ⟶ Y) (V : Set ↑↑Y.toPresheafedSpace) : restrictSet f V = KLocallyRingedSpace.Hom.restrictTo f (X.openOf (KLocallyRingedSpace.Hom.toFun f ⁻¹' V)) (Y.openOf V) ⋯

The restriction f.restrictSet V : X | f⁻¹V ⟶ Y | V is Hom.restrictTo at the opens openOf: both are the lift of f through the open immersion Y | V ⟶ Y.

theorem AnalyticSpace.isIso_restrictTo_of_bijOn_of_bijective_stalkMap {K : Type} [RCLike K] {X Y : AnalyticSpace K} (φ : X ⟶ Y) (U : TopologicalSpace.Opens ↑↑X.toPresheafedSpace) (V : TopologicalSpace.Opens ↑↑Y.toPresheafedSpace) (hUV : ∀ u ∈ U, KLocallyRingedSpace.Hom.toFun φ u ∈ V) (hbij : Set.BijOn (KLocallyRingedSpace.Hom.toFun φ) ↑U ↑V) (hs : ∀ u ∈ U, Function.Bijective ⇑(CommRingCat.Hom.hom (AlgebraicGeometry.LocallyRingedSpace.Hom.stalkMap (↑φ) u))) : CategoryTheory.IsIso (KLocallyRingedSpace.Hom.restrictTo φ U V hUV)

A morphism of analytic K-spaces which is bijective from the open U onto the open V and has bijective stalk maps at the points of U restricts to a K-isomorphism X | U ≅ Y | V: the restricted base map is a continuous bijection which is open — at every point of U the morphism is a local isomorphism (exists_isIso_restrictTo_of_bijective_stalkMap), and a local isomorphism maps opens to opens (isOpen_image_of_isIso_restrictTo) — hence a homeomorphism; the stalk maps of the restriction are those of φ; the criterion isIso_of_isIso_base_of_stalkMap_bijective concludes.