The glued K-space

The locally ringed space glued from K-gluing data D (Hironaka.AnalyticSpace.Glue.Data) is a K-space (gluedK): the constants of the pieces (Hironaka.AnalyticSpace.Glue.Space), compatible on the overlaps (Hironaka.AnalyticSpace.Glue.Compat), glue to global sections by the sheaf condition (Mathlib's existsUnique_gluing'; glueConst), the ring-homomorphism laws follow from the uniqueness of the gluing (algebraMapGlued), and the open immersions ι i of the pieces become K-morphisms ιK i : Y i ⟶ gluedK, each piece being K-isomorphic to its image (imageIso). With a countable index type, Hausdorffness (the criterion of Hironaka.AnalyticSpace.Glue.Topology, transported along the comparison isomorphism topIso: t2Space_of_isClosed_transitionGraph) and analytic pieces, the glued K-space is an analytic K-space (gluedAnalytic, through AnalyticSpace.ofOpenCover of Hironaka.AnalyticSpace.Glue.OfCover).

Conventions. glueConst c is the unique global section restricting to constOn c i on every image; gluedK is an abbrev, so that its underlying locally ringed space is glued definitionally. The Hausdorff hypothesis is stated on the topological gluing data topGlueData (closed transition graphs for i ≠ j). With one piece the glued K-space is K-isomorphic to the piece; with an empty index type it is the empty analytic space.

This is the assembly step of the gluing of local complexifications [BW59, Proposition 1] and of the gluing of local resolutions over a base (Hironaka.AnalyticSpace.Glue.Over).

The glued constants

theorem AnalyticSpace.Glue.KGlueData.top_le_iSup_pieceOpens {K : Type} [RCLike K] (D : KGlueData K) : ⊤ ≤ ⨆ (i : D.J), D.pieceOpens i

theorem AnalyticSpace.Glue.KGlueData.existsUnique_glueConst {K : Type} [RCLike K] (D : KGlueData K) (c : K) : ∃! s : ↑(D.glued.presheaf.obj (Opposite.op ⊤)), ∀ (i : D.J), (CommRingCat.Hom.hom (D.glued.presheaf.map (CategoryTheory.homOfLE ⋯).op)) s = D.constOn c i

The unique gluing of the constants of the pieces.

noncomputable def AnalyticSpace.Glue.KGlueData.glueConst {K : Type} [RCLike K] (D : KGlueData K) (c : K) : ↑(D.glued.presheaf.obj (Opposite.op ⊤))

The constant c of the glued space: the gluing of the constants of the pieces.

Equations

• D.glueConst c = Classical.choose ⋯

theorem AnalyticSpace.Glue.KGlueData.map_glueConst {K : Type} [RCLike K] (D : KGlueData K) (c : K) (i : D.J) : (CommRingCat.Hom.hom (D.glued.presheaf.map (CategoryTheory.homOfLE ⋯).op)) (D.glueConst c) = D.constOn c i

theorem AnalyticSpace.Glue.KGlueData.glueConst_unique {K : Type} [RCLike K] (D : KGlueData K) (c : K) (s : ↑(D.glued.presheaf.obj (Opposite.op ⊤))) (hs : ∀ (i : D.J), (CommRingCat.Hom.hom (D.glued.presheaf.map (CategoryTheory.homOfLE ⋯).op)) s = D.constOn c i) : s = D.glueConst c

theorem AnalyticSpace.Glue.KGlueData.constOn_add {K : Type} [RCLike K] (D : KGlueData K) (c c' : K) (i : D.J) : D.constOn (c + c') i = D.constOn c i + D.constOn c' i

theorem AnalyticSpace.Glue.KGlueData.constOn_mul {K : Type} [RCLike K] (D : KGlueData K) (c c' : K) (i : D.J) : D.constOn (c * c') i = D.constOn c i * D.constOn c' i

theorem AnalyticSpace.Glue.KGlueData.constOn_one {K : Type} [RCLike K] (D : KGlueData K) (i : D.J) : D.constOn 1 i = 1

theorem AnalyticSpace.Glue.KGlueData.constOn_zero {K : Type} [RCLike K] (D : KGlueData K) (i : D.J) : D.constOn 0 i = 0

noncomputable def AnalyticSpace.Glue.KGlueData.algebraMapGlued {K : Type} [RCLike K] (D : KGlueData K) : K →+* ↑(D.glued.presheaf.obj (Opposite.op ⊤))

The K-structure of the glued space.

Equations

• D.algebraMapGlued = { toFun := D.glueConst, map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ }

@[reducible, inline]

noncomputable abbrev AnalyticSpace.Glue.KGlueData.gluedK {K : Type} [RCLike K] (D : KGlueData K) : KLocallyRingedSpace K

The glued K-space.

Equations

• D.gluedK = { toLocallyRingedSpace := D.glued, algebraMap := D.algebraMapGlued }

The pieces map into the glued K-space by K-morphisms

theorem AnalyticSpace.Glue.KGlueData.map_pieceOpens_self {K : Type} [RCLike K] (D : KGlueData K) (i : D.J) : (TopologicalSpace.Opens.map (D.ι i).base).obj (D.pieceOpens i) = ⊤

The preimage in a piece of its own image is everything.

theorem AnalyticSpace.Glue.KGlueData.c_app_top_glueConst {K : Type} [RCLike K] (D : KGlueData K) (c : K) (i : D.J) : (CommRingCat.Hom.hom ((D.ι i).c.app (Opposite.op ⊤))) (D.glueConst c) = globalConst (D.Y i) c

Pulling the glued constant back to a piece gives the constant of the piece.

noncomputable def AnalyticSpace.Glue.KGlueData.ιK {K : Type} [RCLike K] (D : KGlueData K) (i : D.J) : D.Y i ⟶ D.gluedK

The open immersion of a piece, as a K-morphism into the glued K-space.

Equations

• D.ιK i = ⟨D.ι i, ⋯⟩

instance AnalyticSpace.Glue.KGlueData.instIsOpenImmersionValHomLocallyRingedSpaceYGluedKEqRingHomCarrierObjOppositeCommRingCatΓOpCompHomMapOpAlgebraMapιK {K : Type} [RCLike K] (D : KGlueData K) (i : D.J) : AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion ↑(D.ιK i)

theorem AnalyticSpace.Glue.KGlueData.toFun_ιK {K : Type} [RCLike K] (D : KGlueData K) (i : D.J) : KLocallyRingedSpace.Hom.toFun (D.ιK i) = ⇑(CategoryTheory.ConcreteCategory.hom (D.ι i).base)

noncomputable def AnalyticSpace.Glue.KGlueData.imageIso {K : Type} [RCLike K] (D : KGlueData K) (i : D.J) : (D.Y i).KIso (D.gluedK.restrictOpen (D.pieceOpens i))

A piece is K-isomorphic to its image in the glued K-space.

Equations

• D.imageIso i = AnalyticSpace.KLocallyRingedSpace.isoOfRangeEq (D.ιK i) (D.gluedK.ofRestrict (D.pieceOpens i)) ⋯

Hausdorffness and the analytic structure

@[reducible, inline]

noncomputable abbrev AnalyticSpace.Glue.KGlueData.topGlueData {K : Type} [RCLike K] (D : KGlueData K) : TopCat.GlueData

The topological gluing data underlying D.

Equations

• D.topGlueData = D.toLRSGlueData.toSheafedSpaceGlueData.toPresheafedSpaceGlueData.toTopGlueData

theorem AnalyticSpace.Glue.KGlueData.t2Space_of_isClosed_transitionGraph {K : Type} [RCLike K] (D : KGlueData K) (hT2 : ∀ (i : D.J), T2Space ↑↑(D.Y i).toPresheafedSpace) (hgraph : ∀ (i j : D.topGlueData.J), i ≠ j → IsClosed (transitionGraph D.topGlueData i j)) : T2Space ↑D.glued.toTopCat

The glued space is Hausdorff when the pieces are and the transition graphs are closed (the criterion of Hironaka.AnalyticSpace.Glue.Topology, transported along topIso).

noncomputable def AnalyticSpace.Glue.KGlueData.gluedAnalytic {K : Type} [RCLike K] (D : KGlueData K) [Countable D.J] (hT2 : T2Space ↑D.glued.toTopCat) (Z : D.J → AnalyticSpace K) (e : (i : D.J) → (D.Y i).KIso (Z i).toKLocallyRingedSpace) : AnalyticSpace K

The glued K-space is an analytic K-space when it is Hausdorff, the index type is countable and every piece is K-isomorphic to an analytic space.

Equations

• D.gluedAnalytic hT2 Z e = AnalyticSpace.ofOpenCover D.gluedK D.pieceOpens ⋯ Z fun (i : D.J) => CategoryTheory.Iso.symm (D.imageIso i) ≪≫ e i