Gluing analytic spaces over a base along the overlaps of their base open subsets

Włodarczyk builds the canonical desingularization of an analytic space by gluing the desingularizations of the pieces of a cover along their overlaps: Ṽ is the manifold "obtained by gluing Ṽ_i along Ṽ_i ∩ Ṽ_j", and the desingularization morphism des_V : Ṽ → V is bimeromorphic and proper [Wlo09, §4], and for a whole analytic space Ỹ is the manifold obtained by gluing the Ũ_i along the Ũ_ij [Wlo09, §4.3]; Kollár globalizes likewise, from neighbourhoods of compact sets to an increasing union of them [Kol07, 44]. Both the finite gluing over a relatively compact open subset and the countable one along an exhaustion glue analytic K-spaces R i lying over a base X through maps π i : R i → X, the i-th piece living over an open subset dom i ⊆ X, along the overlaps dom i ∩ dom j of the base open subsets: the gluing open subsets are the preimages π i ⁻¹(dom i ∩ dom j), the transitions are K-isomorphisms between them compatible with the π i, and the glued space comes with the descended map to X. This module packages that shape once, over the gluing of K-spaces (KGlueData, gluedAnalytic, descK of Hironaka.AnalyticSpace.Glue.KSpace and Hironaka.AnalyticSpace.Glue.Desc):

• GlueOver.glueOpens X R π dom i j: the gluing open subset π i ⁻¹(dom i ∩ dom j) of the i-th piece towards the j-th (the embedding (V_i ∩ V_j)~ → Ṽ_i of [Wlo09, §4]), the points overOpens π i (dom i ⊓ dom j) over the overlap (overOpens_eq_comap: Mathlib's Opens.comap); glueOpens_self_eq_top is the W_id field of the gluing core once every π i lands in dom i;
• GlueOver X R π dom: the data: range_subset, the transitions t i j with t_id and t_inter (the fields of KGlueCore), their compatibility compat with the π i (the descent hypothesis of descK), the cocycle identity cocycle (KGlueData), and the Hausdorffness t2 of the glued space, which the sources take for granted with the manifold structure of Ṽ; it is discharged where the data are built, by the closed-graph criterion t2Space_of_isClosed_transitionGraph of Hironaka.AnalyticSpace.Glue.KSpace, applied in Hironaka.AnalyticSpace.Glue.OverLemmas;
• GlueOver.gluedOver: the glued analytic K-space, for a countable index type (gluedAnalytic, every piece being analytic); GlueOver.descMap : gluedOver ⟶ X, the descended map (des_V); GlueOver.ιGlued i, the open immersions of the pieces, with ιGlued_descMap : ιGlued i ≫ descMap = π i and range_toFun_descMap_subset : range descMap ⊆ ⋃ i, dom i.

The gluing data over a base are used to assemble the resolution of an analytic space from the local resolutions of the pieces of a cover, and along an exhaustion, in Hironaka.Manifold.Sequence.Restrict (PieceGlue, PieceGlueDatum, PieceGlueIndep, ResolutionClauses), which establish the clauses of the resolution theorem for analytic spaces.

@[reducible, inline]

abbrev AnalyticSpace.GlueOver.overOpens {K : Type} [RCLike K] {X : AnalyticSpace K} {ι : Type u} {R : ι → AnalyticSpace K} (π : (i : ι) → (R i).toKLocallyRingedSpace ⟶ X.toKLocallyRingedSpace) (i : ι) (O : TopologicalSpace.Opens ↑↑X.toPresheafedSpace) : TopologicalSpace.Opens ↑↑(R i).toPresheafedSpace

The points of the i-th piece over an open O of the base — the same open as Mathlib's Opens.comap (overOpens_eq_comap), spelled so that glueOpens i j is literally overOpens of the overlap.

Equations

• AnalyticSpace.GlueOver.overOpens π i O = { carrier := AnalyticSpace.KLocallyRingedSpace.Hom.toFun (π i) ⁻¹' ↑O, is_open' := ⋯ }

theorem AnalyticSpace.GlueOver.overOpens_eq_comap {K : Type} [RCLike K] {X : AnalyticSpace K} {ι : Type u} {R : ι → AnalyticSpace K} (π : (i : ι) → (R i).toKLocallyRingedSpace ⟶ X.toKLocallyRingedSpace) (i : ι) (O : TopologicalSpace.Opens ↑↑X.toPresheafedSpace) : overOpens π i O = (TopologicalSpace.Opens.comap { toFun := KLocallyRingedSpace.Hom.toFun (π i), continuous_toFun := ⋯ }) O

overOpens π i O is Mathlib's Opens.comap of O along π i.

def AnalyticSpace.GlueOver.glueOpens {K : Type} [RCLike K] (X : AnalyticSpace K) {ι : Type u} (R : ι → AnalyticSpace K) (π : (i : ι) → (R i).toKLocallyRingedSpace ⟶ X.toKLocallyRingedSpace) (dom : ι → TopologicalSpace.Opens ↑↑X.toPresheafedSpace) (i j : ι) : TopologicalSpace.Opens ↑↑(R i).toPresheafedSpace

The gluing open subset of the i-th piece towards the j-th: the points of R i lying over the overlap dom i ∩ dom j of the base open subsets (the piece (V_i ∩ V_j)~ of Ṽ_i in Wlo09, §4).

Equations

• AnalyticSpace.GlueOver.glueOpens X R π dom i j = AnalyticSpace.GlueOver.overOpens π i (dom i ⊓ dom j)

theorem AnalyticSpace.GlueOver.mem_glueOpens {K : Type} [RCLike K] (X : AnalyticSpace K) {ι : Type u} (R : ι → AnalyticSpace K) (π : (i : ι) → (R i).toKLocallyRingedSpace ⟶ X.toKLocallyRingedSpace) (dom : ι → TopologicalSpace.Opens ↑↑X.toPresheafedSpace) {i j : ι} {x : ↑↑(R i).toPresheafedSpace} : x ∈ glueOpens X R π dom i j ↔ KLocallyRingedSpace.Hom.toFun (π i) x ∈ dom i ∧ KLocallyRingedSpace.Hom.toFun (π i) x ∈ dom j

theorem AnalyticSpace.GlueOver.glueOpens_self_eq_top {K : Type} [RCLike K] (X : AnalyticSpace K) {ι : Type u} (R : ι → AnalyticSpace K) (π : (i : ι) → (R i).toKLocallyRingedSpace ⟶ X.toKLocallyRingedSpace) (dom : ι → TopologicalSpace.Opens ↑↑X.toPresheafedSpace) (hrange : ∀ (i : ι), Set.range (KLocallyRingedSpace.Hom.toFun (π i)) ⊆ ↑(dom i)) (i : ι) : glueOpens X R π dom i i = ⊤

The W_id field of the gluing core: a piece landing in its own base open is glued to itself along everything.

@[reducible, inline]

abbrev AnalyticSpace.GlueOver.overCore {K : Type} [RCLike K] (X : AnalyticSpace K) {ι : Type u} (R : ι → AnalyticSpace K) (π : (i : ι) → (R i).toKLocallyRingedSpace ⟶ X.toKLocallyRingedSpace) (dom : ι → TopologicalSpace.Opens ↑↑X.toPresheafedSpace) (hrange : ∀ (i : ι), Set.range (KLocallyRingedSpace.Hom.toFun (π i)) ⊆ ↑(dom i)) (t : (i j : ι) → (R i).restrictOpen (glueOpens X R π dom i j) ⟶ (R j).restrictOpen (glueOpens X R π dom j i)) (t_id : ∀ (i : ι), t i i = CategoryTheory.CategoryStruct.id ((R i).restrictOpen (glueOpens X R π dom i i))) (t_inter : ∀ (i j k : ι) (x : ↑↑((R i).restrictOpen (glueOpens X R π dom i j)).toPresheafedSpace), ↑x ∈ glueOpens X R π dom i k → ↑(KLocallyRingedSpace.Hom.toFun (t i j) x) ∈ glueOpens X R π dom j k) : Glue.KGlueCore K

The K-gluing core (KGlueCore) of the pieces R i over X with the given transitions: index type ι, pieces R i, gluing open subsets glueOpens, W_id from hrange.

Equations

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

@[reducible, inline]

abbrev AnalyticSpace.GlueOver.overData {K : Type} [RCLike K] (X : AnalyticSpace K) {ι : Type u} (R : ι → AnalyticSpace K) (π : (i : ι) → (R i).toKLocallyRingedSpace ⟶ X.toKLocallyRingedSpace) (dom : ι → TopologicalSpace.Opens ↑↑X.toPresheafedSpace) (hrange : ∀ (i : ι), Set.range (KLocallyRingedSpace.Hom.toFun (π i)) ⊆ ↑(dom i)) (t : (i j : ι) → (R i).restrictOpen (glueOpens X R π dom i j) ⟶ (R j).restrictOpen (glueOpens X R π dom j i)) (t_id : ∀ (i : ι), t i i = CategoryTheory.CategoryStruct.id ((R i).restrictOpen (glueOpens X R π dom i i))) (t_inter : ∀ (i j k : ι) (x : ↑↑((R i).restrictOpen (glueOpens X R π dom i j)).toPresheafedSpace), ↑x ∈ glueOpens X R π dom i k → ↑(KLocallyRingedSpace.Hom.toFun (t i j) x) ∈ glueOpens X R π dom j k) (cocycle : ∀ (i j k : (overCore X R π dom hrange t t_id t_inter).J), CategoryTheory.CategoryStruct.comp ((overCore X R π dom hrange t t_id t_inter).tRes i j k) (CategoryTheory.CategoryStruct.comp ((overCore X R π dom hrange t t_id t_inter).tRes j k i) ((overCore X R π dom hrange t t_id t_inter).tRes k i j)) = CategoryTheory.CategoryStruct.id (((overCore X R π dom hrange t t_id t_inter).Y i).restrictOpen ((overCore X R π dom hrange t t_id t_inter).W i j ⊓ (overCore X R π dom hrange t t_id t_inter).W i k))) : Glue.KGlueData K

The K-gluing data (KGlueData): the core with the cocycle identity.

Equations

• AnalyticSpace.GlueOver.overData X R π dom hrange t t_id t_inter cocycle = { toKGlueCore := AnalyticSpace.GlueOver.overCore X R π dom hrange t t_id t_inter, cocycle := cocycle }

structure AnalyticSpace.GlueOver {K : Type} [RCLike K] (X : AnalyticSpace K) {ι : Type u} (R : ι → AnalyticSpace K) (π : (i : ι) → (R i).toKLocallyRingedSpace ⟶ X.toKLocallyRingedSpace) (dom : ι → TopologicalSpace.Opens ↑↑X.toPresheafedSpace) : Type u

Gluing data over a base [Wlo09, §4 and §4.3]: analytic K-spaces R i lying over the base X through π i : R i → X, the i-th over the open subset dom i ⊆ X, glued along the overlaps of the base open subsets. The fields: every π i lands in dom i; the transitions t i j between the gluing open subsets π i ⁻¹(dom i ∩ dom j) and π j ⁻¹(dom j ∩ dom i), with t_id and t_inter (the fields of KGlueCore), compatible with the π i (compat, the descent hypothesis of descK); the cocycle identity; and the Hausdorffness of the glued space.

• range_subset (i : ι) : Set.range (KLocallyRingedSpace.Hom.toFun (π i)) ⊆ ↑(dom i)

  Every piece lies over its base open.

• t (i j : ι) : (R i).restrictOpen (glueOpens X R π dom i j) ⟶ (R j).restrictOpen (glueOpens X R π dom j i)

  The transition K-morphisms between the gluing opens.

• t_id (i : ι) : self.t i i = CategoryTheory.CategoryStruct.id ((R i).restrictOpen (glueOpens X R π dom i i))
• t_inter (i j k : ι) (x : ↑↑((R i).restrictOpen (glueOpens X R π dom i j)).toPresheafedSpace) : ↑x ∈ glueOpens X R π dom i k → ↑(KLocallyRingedSpace.Hom.toFun (self.t i j) x) ∈ glueOpens X R π dom j k

  The transition from i to j maps the points over dom k to points over dom k.

• compat (i j : ι) : CategoryTheory.CategoryStruct.comp ((R i).ofRestrict (glueOpens X R π dom i j)) (π i) = CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp (self.t i j) ((R j).ofRestrict (glueOpens X R π dom j i))) (π j)

  The transitions lie over X: π j ∘ t i j = π i on the gluing open.

• cocycle (i j k : (overCore X R π dom ⋯ self.t ⋯ ⋯).J) : CategoryTheory.CategoryStruct.comp ((overCore X R π dom ⋯ self.t ⋯ ⋯).tRes i j k) (CategoryTheory.CategoryStruct.comp ((overCore X R π dom ⋯ self.t ⋯ ⋯).tRes j k i) ((overCore X R π dom ⋯ self.t ⋯ ⋯).tRes k i j)) = CategoryTheory.CategoryStruct.id (((overCore X R π dom ⋯ self.t ⋯ ⋯).Y i).restrictOpen ((overCore X R π dom ⋯ self.t ⋯ ⋯).W i j ⊓ (overCore X R π dom ⋯ self.t ⋯ ⋯).W i k))

  The cocycle identity of the gluing data.

• t2 : T2Space ↑(overData X R π dom ⋯ self.t ⋯ ⋯ ⋯).glued.toTopCat

  The glued space is Hausdorff.

@[reducible, inline]

abbrev AnalyticSpace.GlueOver.toKGlueData {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) : Glue.KGlueData K

The K-gluing data of the gluing over X.

Equations

• G.toKGlueData = AnalyticSpace.GlueOver.overData X R π dom ⋯ G.t ⋯ ⋯ ⋯

theorem AnalyticSpace.GlueOver.toKGlueData_J {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) : G.toKGlueData.J = ι

theorem AnalyticSpace.GlueOver.toKGlueData_Y {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) (i : ι) : G.toKGlueData.Y i = (R i).toKLocallyRingedSpace

theorem AnalyticSpace.GlueOver.toKGlueData_W {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) (i j : ι) : G.toKGlueData.W i j = glueOpens X R π dom i j

theorem AnalyticSpace.GlueOver.toKGlueData_t {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) (i j : ι) : G.toKGlueData.t i j = G.t i j

noncomputable def AnalyticSpace.GlueOver.gluedOver {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 ι] : AnalyticSpace K

The glued analytic K-space ("Ṽ obtained by gluing Ṽ_i along Ṽ_i ∩ Ṽ_j", Wlo09, §4), for a countable index type: gluedAnalytic of the K-gluing data, the pieces being the analytic spaces R i themselves.

Equations

• G.gluedOver = G.toKGlueData.gluedAnalytic ⋯ R fun (x : G.toKGlueData.J) => CategoryTheory.Iso.refl (G.toKGlueData.Y x)

theorem AnalyticSpace.GlueOver.gluedOver_toKLocallyRingedSpace {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 ι] : G.gluedOver.toKLocallyRingedSpace = G.toKGlueData.gluedK

noncomputable def AnalyticSpace.GlueOver.descMap {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 ι] : G.gluedOver.toKLocallyRingedSpace ⟶ X.toKLocallyRingedSpace

The descended map to the base (des_V : Ṽ → V of [Wlo09, §4]): the π i descend to the glued space by compat (descK).

Equations

• G.descMap = G.toKGlueData.descK π ⋯

noncomputable def AnalyticSpace.GlueOver.ι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 : ι) : (R i).toKLocallyRingedSpace ⟶ G.gluedOver.toKLocallyRingedSpace

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

Equations

• G.ιGlued i = G.toKGlueData.ιK i

instance AnalyticSpace.GlueOver.isOpenImmersion_ι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 : ι) : AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion ↑(G.ιGlued i)

theorem AnalyticSpace.GlueOver.ιGlued_descMap {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 : ι) : CategoryTheory.CategoryStruct.comp (G.ιGlued i) G.descMap = π i

The descended map restricts to π i on the i-th piece.

theorem AnalyticSpace.GlueOver.toFun_descMap_ι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 : ι) (y : ↑↑(R i).toPresheafedSpace) : KLocallyRingedSpace.Hom.toFun G.descMap (KLocallyRingedSpace.Hom.toFun (G.ιGlued i) y) = KLocallyRingedSpace.Hom.toFun (π i) y

theorem AnalyticSpace.GlueOver.exists_ιGlued_eq {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 ι] (z : ↑↑G.gluedOver.toPresheafedSpace) : ∃ (i : ι) (y : ↑↑(R i).toPresheafedSpace), KLocallyRingedSpace.Hom.toFun (G.ιGlued i) y = z

Every point of the glued space comes from a piece (exists_ι_base_eq, with the index and piece types of the gluing over X).

theorem AnalyticSpace.GlueOver.range_toFun_descMap_subset {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 ι] : Set.range (KLocallyRingedSpace.Hom.toFun G.descMap) ⊆ ⋃ (i : ι), ↑(dom i)

The glued space lies over the union of the base opens.