Sections on the images of the pieces of a glued space

Building blocks for the K-structure of the glued space of K-gluing data (Hironaka.AnalyticSpace.Glue.Space): the sheaf component (ι i).c.app O of the open immersion of a piece is an isomorphism for every open subset O inside the image of the piece (Mathlib's c_iso on the image of its preimage), hence injective on sections there (c_app_injective_of_le); and the points of the glued space are described through the pieces: Mathlib describes the points of a topological gluing (TopCat.GlueData.ι_eq_iff_rel), and the glued locally ringed space differs from the topological gluing by the comparison isomorphisms of the three gluing layers, composed here into one homeomorphism topIso and transported pointwise, so that two points of pieces with the same image come from a point of the overlap piece (exists_of_ι_base_eq) and the preimage in the i-th piece of the image of the j-th is W i j (map_pieceOpens_eq).

Conventions. D.ι i, D.pieceOpens, D.constOn are those of Hironaka.AnalyticSpace.Glue.Space; opensFunctor is Mathlib's image functor of an open immersion. For O = pieceOpens i the sheaf component is the isomorphism c_iso ⊤.

theorem AnalyticSpace.Glue.KGlueData.pieceOpens_map_eq_of_le {K : Type} [RCLike K] (D : KGlueData K) {i : D.J} (O : TopologicalSpace.Opens ↑D.glued.toTopCat) (hO : O ≤ D.pieceOpens i) : (AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.opensFunctor (D.ι i)).obj ((TopologicalSpace.Opens.map (D.ι i).base).obj O) = O

An open of the glued space inside the image of the i-th piece is the image of its preimage.

theorem AnalyticSpace.Glue.KGlueData.isIso_c_app_of_le {K : Type} [RCLike K] (D : KGlueData K) {i : D.J} (O : TopologicalSpace.Opens ↑D.glued.toTopCat) (hO : O ≤ D.pieceOpens i) : CategoryTheory.IsIso ((D.ι i).c.app (Opposite.op O))

The sheaf component of the open immersion of a piece is an isomorphism on the opens inside the image of the piece.

theorem AnalyticSpace.Glue.KGlueData.c_app_injective_of_le {K : Type} [RCLike K] (D : KGlueData K) {i : D.J} (O : TopologicalSpace.Opens ↑D.glued.toTopCat) (hO : O ≤ D.pieceOpens i) : Function.Injective ⇑(CommRingCat.Hom.hom ((D.ι i).c.app (Opposite.op O)))

The sheaf component of the open immersion of a piece is injective on the sections of an open inside the image of the piece.

Points of the glued space: the overlaps come from the pieces V (i, j)

Mathlib describes the points of a topological gluing (TopCat.GlueData.ι_eq_iff_rel); the glued locally ringed space differs from the topological gluing by the comparison isomorphisms of the three gluing layers, composed here into one homeomorphism and transported pointwise.

instance AnalyticSpace.Glue.KGlueData.instPreservesLimitPresheafedSpaceCommRingCatTopCatWalkingCospanCospanFToPresheafedSpaceGlueDataToSheafedSpaceGlueDataToLRSGlueDataForget {K : Type} [RCLike K] (D : KGlueData K) (i j k : D.toLRSGlueData.toSheafedSpaceGlueData.toPresheafedSpaceGlueData.J) : CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.cospan (D.toLRSGlueData.toSheafedSpaceGlueData.toPresheafedSpaceGlueData.f i j) (D.toLRSGlueData.toSheafedSpaceGlueData.toPresheafedSpaceGlueData.f i k)) (AlgebraicGeometry.PresheafedSpace.forget CommRingCat)

noncomputable def AnalyticSpace.Glue.KGlueData.topIso {K : Type} [RCLike K] (D : KGlueData K) : D.toLRSGlueData.toSheafedSpaceGlueData.toPresheafedSpaceGlueData.toTopGlueData.glued ≅ D.glued.toTopCat

The comparison between the topological gluing and the underlying space of the glued locally ringed space: the composite of Mathlib's gluedIso (presheafed → topological), isoPresheafedSpace and isoSheafedSpace.

Equations

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

theorem AnalyticSpace.Glue.KGlueData.ι_base_eq_topIso {K : Type} [RCLike K] (D : KGlueData K) (i : D.J) : (D.ι i).base = CategoryTheory.CategoryStruct.comp (D.toLRSGlueData.toSheafedSpaceGlueData.toPresheafedSpaceGlueData.toTopGlueData.ι i) D.topIso.hom

The base map of a piece's open immersion is the topological gluing's structure map followed by the comparison.

theorem AnalyticSpace.Glue.KGlueData.exists_of_ι_base_eq {K : Type} [RCLike K] (D : KGlueData K) {i j : D.J} {x : ↑↑(D.Y i).toPresheafedSpace} {y : ↑↑(D.Y j).toPresheafedSpace} (h : (CategoryTheory.ConcreteCategory.hom (D.ι i).base) x = (CategoryTheory.ConcreteCategory.hom (D.ι j).base) y) : ∃ (v : ↑↑((D.Y i).restrictOpen (D.W i j)).toPresheafedSpace), (CategoryTheory.ConcreteCategory.hom (D.f i j).base) v = x ∧ (CategoryTheory.ConcreteCategory.hom (D.f j i).base) ((CategoryTheory.ConcreteCategory.hom (↑(D.t i j)).base) v) = y

Two points of pieces with the same image in the glued space come from a point of the overlap piece V (i, j): x = f i j v and y = f j i (t i j v).

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

The preimage in the i-th piece of the image of the j-th piece is the open W i j.