The glued space of K-gluing data: pieces, images, constants

For gluing data D : KGlueData K (Hironaka.AnalyticSpace.Glue.Data) the glued locally ringed space D.glued carries the open immersions D.ι i : Y i ⟶ D.glued, whose images D.pieceOpens i cover it, and on each image the constant sections D.constOn c i transported from the K-structure of Y i through the inverse of the open immersion on sections (IsOpenImmersion.invApp). This module sets up these objects; the compatibility of the constants on the overlaps (from the transitions being K-morphisms) is Hironaka.AnalyticSpace.Glue.Compat, and the resulting K-structure on D.glued is Hironaka.AnalyticSpace.Glue.KSpace.

Conventions. D.glued is Mathlib's GlueData.glued (a multicoequalizer); D.ι i are its structure morphisms, open immersions (LocallyRingedSpace.GlueData.ι_isOpenImmersion), jointly surjective on points (ι_jointly_surjective); pieceOpens i = ι i '' ⊤ through Mathlib's opensFunctor. With one piece, pieceOpens = ⊤ and constOn c is the constant of the piece; with an empty index type the glued space is empty.

@[reducible, inline]

noncomputable abbrev AnalyticSpace.Glue.KGlueData.glued {K : Type} [RCLike K] (D : KGlueData K) : AlgebraicGeometry.LocallyRingedSpace

The glued locally ringed space.

Equations

• D.glued = D.toLRSGlueData.glued

@[reducible, inline]

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

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

Equations

• D.ι i = D.toLRSGlueData.ι i

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

noncomputable def AnalyticSpace.Glue.KGlueData.pieceOpens {K : Type} [RCLike K] (D : KGlueData K) (i : D.J) : TopologicalSpace.Opens ↑D.glued.toTopCat

The image of the i-th piece, an open of the glued space.

Equations

• D.pieceOpens i = (AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.opensFunctor (D.ι i)).obj ⊤

theorem AnalyticSpace.Glue.KGlueData.mem_pieceOpens_iff {K : Type} [RCLike K] (D : KGlueData K) (i : D.J) (z : ↑D.glued.toTopCat) : z ∈ D.pieceOpens i ↔ ∃ (y : ↑↑(D.Y i).toPresheafedSpace), (CategoryTheory.ConcreteCategory.hom (D.ι i).base) y = z

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

The images of the pieces cover the glued space.

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

The constant c on the image of the i-th piece, transported from the K-structure of Y i.

Equations

• D.constOn c i = (CommRingCat.Hom.hom (AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.invApp (D.ι i) ⊤)) ((D.Y i).algebraMap c)