The part of a glued space over a base open subset is the part of the piece

Over V_i the glued space Ṽ of [Wlo09, §4] is Ṽ_i: for a gluing datum G : GlueOver X R π dom and an open subset P ≤ dom i, the open immersion ιGlued i carries the part of the i-th piece over P onto the part of the glued space over P (range_ofRestrict_comp_ιGlued, from mem_range_toFun_ιGlued_iff of Hironaka.AnalyticSpace.Glue.OverProper), hence partIso : (R i)|π_i⁻¹P ≅ Ṽ|des⁻¹P, an isomorphism over X (partIso_over, partIso_inv_comp_over). Through it, statements about a glued local resolution over a base open subset are read on the piece (Hironaka.Resolution.Analytic.Kol07Thm45.PieceGlueIndep, ResolutionOnMembers, LocalModel, AmbientLift, AmbientFactorization).

theorem AnalyticSpace.GlueOver.range_ofRestrict_comp_ιGlued {K : Type} [RCLike K] {X : AnalyticSpace K} {ι : Type u} {R : ι → AnalyticSpace K} {π : (i : ι) → (R i).toKLocallyRingedSpace ⟶ X.toKLocallyRingedSpace} {dom : ι → TopologicalSpace.Opens ↑↑X.toPresheafedSpace} (G : X.GlueOver R π dom) [Countable ι] (i : ι) (P : TopologicalSpace.Opens ↑↑X.toPresheafedSpace) (hP : P ≤ dom i) : Set.range (KLocallyRingedSpace.Hom.toFun (CategoryTheory.CategoryStruct.comp ((R i).ofRestrict ((TopologicalSpace.Opens.comap { toFun := KLocallyRingedSpace.Hom.toFun (π i), continuous_toFun := ⋯ }) P)) (G.ιGlued i))) = Set.range (KLocallyRingedSpace.Hom.toFun (G.gluedOver.ofRestrict ((TopologicalSpace.Opens.comap { toFun := KLocallyRingedSpace.Hom.toFun G.descMap, continuous_toFun := ⋯ }) P)))

The part of the i-th piece over P ≤ dom i maps onto the part of the glued space over P under ιGlued i: a point of the glued space over P ⊆ dom i comes from the i-th piece (mem_range_toFun_ιGlued_iff), from a point over P.

theorem AnalyticSpace.GlueOver.isOpenImmersion_ofRestrict_comp_ιGlued {K : Type} [RCLike K] {X : AnalyticSpace K} {ι : Type u} {R : ι → AnalyticSpace K} {π : (i : ι) → (R i).toKLocallyRingedSpace ⟶ X.toKLocallyRingedSpace} {dom : ι → TopologicalSpace.Opens ↑↑X.toPresheafedSpace} (G : X.GlueOver R π dom) [Countable ι] (i : ι) (P : TopologicalSpace.Opens ↑↑X.toPresheafedSpace) : AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion ↑(CategoryTheory.CategoryStruct.comp ((R i).ofRestrict ((TopologicalSpace.Opens.comap { toFun := KLocallyRingedSpace.Hom.toFun (π i), continuous_toFun := ⋯ }) P)) (G.ιGlued i))

The open immersion of the part of the i-th piece over P into the glued space.

noncomputable def AnalyticSpace.GlueOver.partIso {K : Type} [RCLike K] {X : AnalyticSpace K} {ι : Type u} {R : ι → AnalyticSpace K} {π : (i : ι) → (R i).toKLocallyRingedSpace ⟶ X.toKLocallyRingedSpace} {dom : ι → TopologicalSpace.Opens ↑↑X.toPresheafedSpace} (G : X.GlueOver R π dom) [Countable ι] (i : ι) (P : TopologicalSpace.Opens ↑↑X.toPresheafedSpace) (hP : P ≤ dom i) : (R i).restrictOpen ((TopologicalSpace.Opens.comap { toFun := KLocallyRingedSpace.Hom.toFun (π i), continuous_toFun := ⋯ }) P) ≅ G.gluedOver.restrictOpen ((TopologicalSpace.Opens.comap { toFun := KLocallyRingedSpace.Hom.toFun G.descMap, continuous_toFun := ⋯ }) P)

The part of the glued space over P ≤ dom i is the part of the i-th piece over P (isoOfRangeEq on ofRestrict ≫ ιGlued i; [Wlo09, §4]).

Equations

• One or more equations did not get rendered due to their size.

theorem AnalyticSpace.GlueOver.partIso_hom_comp_ofRestrict {K : Type} [RCLike K] {X : AnalyticSpace K} {ι : Type u} {R : ι → AnalyticSpace K} {π : (i : ι) → (R i).toKLocallyRingedSpace ⟶ X.toKLocallyRingedSpace} {dom : ι → TopologicalSpace.Opens ↑↑X.toPresheafedSpace} (G : X.GlueOver R π dom) [Countable ι] (i : ι) (P : TopologicalSpace.Opens ↑↑X.toPresheafedSpace) (hP : P ≤ dom i) : CategoryTheory.CategoryStruct.comp (G.partIso i P hP).hom (G.gluedOver.ofRestrict ((TopologicalSpace.Opens.comap { toFun := KLocallyRingedSpace.Hom.toFun G.descMap, continuous_toFun := ⋯ }) P)) = CategoryTheory.CategoryStruct.comp ((R i).ofRestrict ((TopologicalSpace.Opens.comap { toFun := KLocallyRingedSpace.Hom.toFun (π i), continuous_toFun := ⋯ }) P)) (G.ιGlued i)

The identification, followed by the open immersion of the part of the glued space, is the open immersion of the part of the piece followed by ιGlued i.

theorem AnalyticSpace.GlueOver.partIso_inv_comp_ofRestrict {K : Type} [RCLike K] {X : AnalyticSpace K} {ι : Type u} {R : ι → AnalyticSpace K} {π : (i : ι) → (R i).toKLocallyRingedSpace ⟶ X.toKLocallyRingedSpace} {dom : ι → TopologicalSpace.Opens ↑↑X.toPresheafedSpace} (G : X.GlueOver R π dom) [Countable ι] (i : ι) (P : TopologicalSpace.Opens ↑↑X.toPresheafedSpace) (hP : P ≤ dom i) : CategoryTheory.CategoryStruct.comp (G.partIso i P hP).inv (CategoryTheory.CategoryStruct.comp ((R i).ofRestrict ((TopologicalSpace.Opens.comap { toFun := KLocallyRingedSpace.Hom.toFun (π i), continuous_toFun := ⋯ }) P)) (G.ιGlued i)) = G.gluedOver.ofRestrict ((TopologicalSpace.Opens.comap { toFun := KLocallyRingedSpace.Hom.toFun G.descMap, continuous_toFun := ⋯ }) P)

Its inverse, followed by ofRestrict ≫ ιGlued i, is the open immersion of the part of the glued space.

theorem AnalyticSpace.GlueOver.partIso_over {K : Type} [RCLike K] {X : AnalyticSpace K} {ι : Type u} {R : ι → AnalyticSpace K} {π : (i : ι) → (R i).toKLocallyRingedSpace ⟶ X.toKLocallyRingedSpace} {dom : ι → TopologicalSpace.Opens ↑↑X.toPresheafedSpace} (G : X.GlueOver R π dom) [Countable ι] (i : ι) (P : TopologicalSpace.Opens ↑↑X.toPresheafedSpace) (hP : P ≤ dom i) : CategoryTheory.CategoryStruct.comp ((R i).ofRestrict ((TopologicalSpace.Opens.comap { toFun := KLocallyRingedSpace.Hom.toFun (π i), continuous_toFun := ⋯ }) P)) (π i) = CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp (G.partIso i P hP).hom (G.gluedOver.ofRestrict ((TopologicalSpace.Opens.comap { toFun := KLocallyRingedSpace.Hom.toFun G.descMap, continuous_toFun := ⋯ }) P))) G.descMap

The identification lies over X: π i on the part of the piece is des on the part of the glued space.

theorem AnalyticSpace.GlueOver.partIso_inv_comp_over {K : Type} [RCLike K] {X : AnalyticSpace K} {ι : Type u} {R : ι → AnalyticSpace K} {π : (i : ι) → (R i).toKLocallyRingedSpace ⟶ X.toKLocallyRingedSpace} {dom : ι → TopologicalSpace.Opens ↑↑X.toPresheafedSpace} (G : X.GlueOver R π dom) [Countable ι] (i : ι) (P : TopologicalSpace.Opens ↑↑X.toPresheafedSpace) (hP : P ≤ dom i) : CategoryTheory.CategoryStruct.comp (G.partIso i P hP).inv (CategoryTheory.CategoryStruct.comp ((R i).ofRestrict ((TopologicalSpace.Opens.comap { toFun := KLocallyRingedSpace.Hom.toFun (π i), continuous_toFun := ⋯ }) P)) (π i)) = CategoryTheory.CategoryStruct.comp (G.gluedOver.ofRestrict ((TopologicalSpace.Opens.comap { toFun := KLocallyRingedSpace.Hom.toFun G.descMap, continuous_toFun := ⋯ }) P)) G.descMap

The inverse identification lies over X.