Isomorphisms over an open cover of the target

The predicate f.IsIsoOver U := IsIso (f.restrictSet U) (f restricts to an isomorphism f⁻¹U → U; condition (2) of a resolution in [Hir64, Introduction], clause (2) of [Kol07, Theorem 45], "Π is an isomorphism over X^ns") is local on the target:

• the point-level readings of IsIsoOver over an open V — through the bridge Hom.restrictSet_eq_restrictTo (Hironaka/AnalyticSpace/IsoOverOpen.lean) and the readings of a local isomorphism in Hironaka/AnalyticSpace/RestrictToIso.lean: f is injective on f⁻¹V (injOn_of_isIso_restrictSet), maps f⁻¹V onto V (surjOn_of_isIso_restrictSet), maps opens inside f⁻¹V to opens (isOpen_image_inter_preimage_of_isIso_restrictSet) and has bijective stalk maps over V (bijective_stalkMap_of_isIso_restrictSet);
• isIso_of_isIso_restrictSet_cover / Hom.isIso_of_isIsoOver_cover: a morphism which is an isomorphism over each member of an open cover of the target is an isomorphism — its base map is a continuous open bijection, hence a homeomorphism, and the criterion isIso_of_isIso_base_of_stalkMap_bijective (Hironaka/AnalyticSpace/IsoCriterion.lean) applies;
• isIso_restrictSet_iUnion_of_isIso_restrictSet / Hom.isIsoOver_iUnion: an isomorphism over each member of a family of opens is an isomorphism over their union — isIso_restrictTo_of_bijOn_of_bijective_stalkMap at f⁻¹(⋃ Vᵢ), ⋃ Vᵢ;
• isIso_toKLocallyRingedSpace_of_isIso: the converse of isIso_of_isIso_toKLocallyRingedSpace (Hironaka/AnalyticSpace/SigmaLemmas.lean): an isomorphism of An/K is one of ℜ/K.

In the gluing of local desingularizations of [Wlo09, §4] the glued morphism inherits its properties from the pieces. Routine; used by Hironaka/Resolution/Analytic/Kol07Thm45/AmbientFactorizationTransport.lean, Hironaka/AnalyticSpace/SncFamilyTransport.lean and Hironaka/Resolution/Analytic/Kol07Thm45/IsoOverLemmas.lean.

theorem AnalyticSpace.isIso_toKLocallyRingedSpace_of_isIso {K : Type} [RCLike K] {Y Z : AnalyticSpace K} (f : Y ⟶ Z) [h : CategoryTheory.IsIso f] : CategoryTheory.IsIso f

A morphism of An/K which is an isomorphism is an isomorphism in ℜ/K (the converse of isIso_of_isIso_toKLocallyRingedSpace; the morphisms and compositions are the same).

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

The restriction over V, as the local isomorphism Hom.restrictTo at the opens openOf.

theorem AnalyticSpace.injOn_of_isIso_restrictSet {K : Type} [RCLike K] {X Y : AnalyticSpace K} (f : Y ⟶ X) {V : Set ↑↑X.toPresheafedSpace} (hV : IsOpen V) [CategoryTheory.IsIso (Hom.restrictSet f V)] : Set.InjOn (KLocallyRingedSpace.Hom.toFun f) (KLocallyRingedSpace.Hom.toFun f ⁻¹' V)

An isomorphism over the open V is injective on f⁻¹V.

theorem AnalyticSpace.surjOn_of_isIso_restrictSet {K : Type} [RCLike K] {X Y : AnalyticSpace K} (f : Y ⟶ X) {V : Set ↑↑X.toPresheafedSpace} (hV : IsOpen V) [CategoryTheory.IsIso (Hom.restrictSet f V)] : Set.SurjOn (KLocallyRingedSpace.Hom.toFun f) (KLocallyRingedSpace.Hom.toFun f ⁻¹' V) V

An isomorphism over the open V maps f⁻¹V onto V.

theorem AnalyticSpace.isOpen_image_inter_preimage_of_isIso_restrictSet {K : Type} [RCLike K] {X Y : AnalyticSpace K} (f : Y ⟶ X) {V : Set ↑↑X.toPresheafedSpace} (hV : IsOpen V) [CategoryTheory.IsIso (Hom.restrictSet f V)] {S : Set ↑↑Y.toPresheafedSpace} (hS : IsOpen S) : IsOpen (KLocallyRingedSpace.Hom.toFun f '' (S ∩ KLocallyRingedSpace.Hom.toFun f ⁻¹' V))

An isomorphism over the open V maps the opens inside f⁻¹V to opens.

theorem AnalyticSpace.bijective_stalkMap_of_isIso_restrictSet {K : Type} [RCLike K] {X Y : AnalyticSpace K} (f : Y ⟶ X) {V : Set ↑↑X.toPresheafedSpace} (hV : IsOpen V) [CategoryTheory.IsIso (Hom.restrictSet f V)] (y : ↑↑Y.toPresheafedSpace) (hy : KLocallyRingedSpace.Hom.toFun f y ∈ V) : Function.Bijective ⇑(CommRingCat.Hom.hom (AlgebraicGeometry.LocallyRingedSpace.Hom.stalkMap (↑f) y))

An isomorphism over the open V has bijective stalk maps at the points over V.

theorem AnalyticSpace.isIso_of_isIso_restrictSet_cover {K : Type} [RCLike K] {X Y : AnalyticSpace K} (f : Y ⟶ X) {ι : Type u_1} (V : ι → Set ↑↑X.toPresheafedSpace) (hV : ∀ (i : ι), IsOpen (V i)) (h : ∀ (i : ι), CategoryTheory.IsIso (Hom.restrictSet f (V i))) (hcov : ⋃ (i : ι), V i = Set.univ) : CategoryTheory.IsIso f

A morphism which is an isomorphism over each member of an open cover of the target is an isomorphism (IsIso f in AnalyticSpace): its base map is a bijection (injective on each f⁻¹Vᵢ, onto each Vᵢ) and open (the image of an open is the union of the images of its traces on the f⁻¹Vᵢ), hence a homeomorphism; its stalk maps are bijective; isIso_of_isIso_base_of_stalkMap_bijective concludes.

theorem AnalyticSpace.isIso_restrictSet_iUnion_of_isIso_restrictSet {K : Type} [RCLike K] {X Y : AnalyticSpace K} (f : Y ⟶ X) {ι : Type u_1} (V : ι → Set ↑↑X.toPresheafedSpace) (hV : ∀ (i : ι), IsOpen (V i)) (h : ∀ (i : ι), CategoryTheory.IsIso (Hom.restrictSet f (V i))) : CategoryTheory.IsIso (Hom.restrictSet f (⋃ (i : ι), V i))

A morphism which is an isomorphism over each member of a family of opens is an isomorphism over their union: isIso_restrictTo_of_bijOn_of_bijective_stalkMap at f⁻¹(⋃ Vᵢ), ⋃ Vᵢ — the base map is a bijection there and the stalk maps are bijective.

theorem AnalyticSpace.Hom.isIso_of_isIsoOver_cover {K : Type} [RCLike K] {X Y : AnalyticSpace K} (f : Y ⟶ X) {ι : Type u_1} (V : ι → Set ↑↑X.toPresheafedSpace) (hV : ∀ (i : ι), IsOpen (V i)) (hcov : ⋃ (i : ι), V i = Set.univ) (h : ∀ (i : ι), IsIsoOver f (V i)) : CategoryTheory.IsIso f

A morphism of analytic spaces that is an isomorphism over each member of an open cover of the target is an isomorphism (Hom.IsIsoOver, IsIso; [Kol07, Theorem 45 (2)] checked on the pieces).

theorem AnalyticSpace.Hom.isIsoOver_iUnion {K : Type} [RCLike K] {X Y : AnalyticSpace K} (f : Y ⟶ X) {ι : Type u_1} (V : ι → Set ↑↑X.toPresheafedSpace) (hV : ∀ (i : ι), IsOpen (V i)) (h : ∀ (i : ι), IsIsoOver f (V i)) : IsIsoOver f (⋃ (i : ι), V i)

IsIsoOver of a union of opens from IsIsoOver of each member ([Kol07, Theorem 45 (2)]: the isomorphism over X.regularLocus assembled from the pieces).