Gluing pre-adic spaces

Compatibility with stalk valuations can be checked after precomposition with a jointly surjective family of morphisms. In particular it can be checked on an open cover. This lets a morphism of presheafed spaces obtained by gluing chartwise morphisms lift uniquely to a morphism of pre-adic spaces. Consequently, a cocone of pre-adic spaces with jointly surjective legs is a colimit whenever its underlying cocone of presheafed spaces is a colimit.

This gives gluing in the category 𝒱^pre of pre-adic spaces. Glue data in 𝒱^pre (TauCeti.PreAdicSpace.GlueData) consist of pre-adic spaces U i, open immersions f i j : V i j ⟶ U i and transition morphisms t i j : V i j ⟶ V j i of pre-adic spaces satisfying the cocycle condition. Their underlying presheafed spaces of complete separated topological rings glue (AlgebraicGeometry.PresheafedSpace.GlueData), and the charts of the glued presheafed space are open immersions, so its stalks are those of the U i. Two points of the charts with the same image come from a point of an overlap V i j, where the transition morphisms are compatible with the stalk valuations; so the stalk valuations of the U i descend to the glued space (TauCeti.PreAdicSpace.descend). The resulting pre-adic space, with the charts as legs, is a colimit in 𝒱^pre by the lifting statement above. As for schemes, the glued object is then CategoryTheory.GlueData.glued, its charts ι i are open immersions which are jointly surjective, and V i j is the intersection of the images of U i and U j.

Gluing adic spaces gives an adic space. The glued space is sheafy because a colimit of presheafed spaces with sheaf structure presheaves has a sheaf structure presheaf (AlgebraicGeometry.PresheafedSpace.isSheaf_of_isColimit). It is locally affinoid because its charts are open immersions covering it. Conversely its charts are open adic subspaces, so the glued space is adic exactly when every piece is (TauCeti.PreAdicSpace.GlueData.isAdic_glued_iff). Since (Adic) is a full subcategory of 𝒱^pre, the glued adic space is then a colimit of the gluing diagram in (Adic).

Main definitions

• TauCeti.PreAdicSpace.Hom.ofCover: lift a presheafed-space morphism from its chartwise lifts, for a jointly surjective family.
• TauCeti.PreAdicSpace.isColimitOfIsColimitForgetToPresheafedSpace: lift an underlying colimit cocone with jointly surjective legs.
• TauCeti.PreAdicSpace.GlueData: glue data of pre-adic spaces along open immersions.
• TauCeti.PreAdicSpace.GlueData.isoPresheafedSpace: the underlying presheafed space of the glued pre-adic space is the glued presheafed space.
• TauCeti.PreAdicSpace.GlueData.vPullbackConeIsLimit: V i j is the pullback of the charts U i and U j of the glued space.
• TauCeti.PreAdicSpace.GlueData.gluedAdicι: for adic pieces, the charts of the glued adic space, as a natural transformation out of the gluing diagram in (Adic).
• TauCeti.PreAdicSpace.GlueData.isColimitGluedAdicCocone: the universal property of the glued adic space in (Adic).

Main results

• The HasMulticoequalizer instance for TauCeti.PreAdicSpace.GlueData: glue data of pre-adic spaces have a glued pre-adic space CategoryTheory.GlueData.glued, and the forgetful functor to presheafed spaces preserves it.
• TauCeti.PreAdicSpace.GlueData.ι_isOpenImmersion: the charts of the glued space are open immersions.
• TauCeti.PreAdicSpace.GlueData.ι_jointly_surjective: the charts of the glued space are jointly surjective.
• TauCeti.PreAdicSpace.GlueData.ι_eq_iff_rel: two points of the charts have the same image in the glued space exactly when they come from a common point of an overlap.
• TauCeti.PreAdicSpace.GlueData.isSheafy_glued_iff, TauCeti.PreAdicSpace.GlueData.isLocallyAffinoid_glued_iff, TauCeti.PreAdicSpace.GlueData.isAdic_glued_iff: the glued space is sheafy, locally affinoid, or adic exactly when every piece is.

References

• T. Wedhorn, Adic Spaces, arXiv:1910.05934v1, §8.1 and §8.3.
• Mathlib's AlgebraicGeometry.PresheafedSpace.GlueData provides the underlying gluing; CategoryTheory.Limits.IsColimit.ofFaithful lifts its universal property. The construction of the glued object follows AlgebraicGeometry.Scheme.GlueData.

def TauCeti.PreAdicSpace.Hom.ofCover {X Y : PreAdicSpace} {ι : Type v} {U : ι → PreAdicSpace} (j : (i : ι) → U i ⟶ X) (hcover : ∀ (x : ↑X.toTopCat), ∃ (i : ι) (y : ↑(U i).toTopCat), (CategoryTheory.ConcreteCategory.hom (j i).base) y = x) (g : X.toPresheafedSpace ⟶ Y.toPresheafedSpace) (f : (i : ι) → U i ⟶ Y) (hfac : ∀ (i : ι), CategoryTheory.CategoryStruct.comp (j i).toHom g = (f i).toHom) : X ⟶ Y

A presheafed-space morphism lifts to a morphism of pre-adic spaces if it lifts after precomposition with a jointly surjective family. No sheaf condition is needed: the underlying morphism is already given, and valuation compatibility is checked pointwise on stalks.

@[simp]

theorem TauCeti.PreAdicSpace.Hom.ofCover_toHom {X Y : PreAdicSpace} {ι : Type v} {U : ι → PreAdicSpace} (j : (i : ι) → U i ⟶ X) (hcover : ∀ (x : ↑X.toTopCat), ∃ (i : ι) (y : ↑(U i).toTopCat), (CategoryTheory.ConcreteCategory.hom (j i).base) y = x) (g : X.toPresheafedSpace ⟶ Y.toPresheafedSpace) (f : (i : ι) → U i ⟶ Y) (hfac : ∀ (i : ι), CategoryTheory.CategoryStruct.comp (j i).toHom g = (f i).toHom) : (ofCover j hcover g f hfac).toHom = g

The lift retains the given underlying morphism of presheafed spaces.

@[simp]

theorem TauCeti.PreAdicSpace.Hom.comp_ofCover {X Y : PreAdicSpace} {ι : Type v} {U : ι → PreAdicSpace} (j : (i : ι) → U i ⟶ X) (hcover : ∀ (x : ↑X.toTopCat), ∃ (i : ι) (y : ↑(U i).toTopCat), (CategoryTheory.ConcreteCategory.hom (j i).base) y = x) (g : X.toPresheafedSpace ⟶ Y.toPresheafedSpace) (f : (i : ι) → U i ⟶ Y) (hfac : ∀ (i : ι), CategoryTheory.CategoryStruct.comp (j i).toHom g = (f i).toHom) (i : ι) : CategoryTheory.CategoryStruct.comp (j i) (ofCover j hcover g f hfac) = f i

The lifted morphism agrees with the given morphism on each chart.

@[simp]

theorem TauCeti.PreAdicSpace.Hom.comp_ofCover_assoc {X Y : PreAdicSpace} {ι : Type v} {U : ι → PreAdicSpace} (j : (i : ι) → U i ⟶ X) (hcover : ∀ (x : ↑X.toTopCat), ∃ (i : ι) (y : ↑(U i).toTopCat), (CategoryTheory.ConcreteCategory.hom (j i).base) y = x) (g : X.toPresheafedSpace ⟶ Y.toPresheafedSpace) (f : (i : ι) → U i ⟶ Y) (hfac : ∀ (i : ι), CategoryTheory.CategoryStruct.comp (j i).toHom g = (f i).toHom) (i : ι) {Z : PreAdicSpace} (h : Y ⟶ Z) : CategoryTheory.CategoryStruct.comp (j i) (CategoryTheory.CategoryStruct.comp (ofCover j hcover g f hfac) h) = CategoryTheory.CategoryStruct.comp (f i) h

The lifted morphism agrees with the given morphism on each chart.

noncomputable def TauCeti.PreAdicSpace.isColimitOfIsColimitForgetToPresheafedSpace {J : Type v} [CategoryTheory.Category.{w, v} J] {F : CategoryTheory.Functor J PreAdicSpace} (c : CategoryTheory.Limits.Cocone F) (hcover : ∀ (x : ↑c.pt.toTopCat), ∃ (i : J) (y : ↑(F.obj i).toTopCat), (CategoryTheory.ConcreteCategory.hom (c.ι.app i).base) y = x) (hc : CategoryTheory.Limits.IsColimit (forgetToPresheafedSpace.mapCocone c)) : CategoryTheory.Limits.IsColimit c

The universal property of gluing lifts to pre-adic spaces. A cocone whose legs are jointly surjective is a colimit if its underlying cocone of presheafed spaces is a colimit. In particular, once the glued object and its chart inclusions have been equipped with their pre-adic structures, no further valuation condition is needed for the universal property. The diagram and the target of a descended morphism need not be sheafy.

@[simp]

theorem TauCeti.PreAdicSpace.isColimitOfIsColimitForgetToPresheafedSpace_desc_toHom {J : Type v} [CategoryTheory.Category.{w, v} J] {F : CategoryTheory.Functor J PreAdicSpace} (c : CategoryTheory.Limits.Cocone F) (hcover : ∀ (x : ↑c.pt.toTopCat), ∃ (i : J) (y : ↑(F.obj i).toTopCat), (CategoryTheory.ConcreteCategory.hom (c.ι.app i).base) y = x) (hc : CategoryTheory.Limits.IsColimit (forgetToPresheafedSpace.mapCocone c)) (s : CategoryTheory.Limits.Cocone F) : ((isColimitOfIsColimitForgetToPresheafedSpace c hcover hc).desc s).toHom = hc.desc (forgetToPresheafedSpace.mapCocone s)

The descended morphism in the lifted colimit is the underlying presheafed-space descent. Thus the colimit lift changes neither the continuous map nor the map of structure presheaves.

Glue data of pre-adic spaces

structure TauCeti.PreAdicSpace.GlueDataextends CategoryTheory.GlueData TauCeti.PreAdicSpace : Type (u + 1)

Glue data of pre-adic spaces: glue data in the category 𝒱^pre whose gluing maps f i j : V i j ⟶ U i are open immersions of pre-adic spaces.

• J : Type u
• U : self.J → TauCeti.PreAdicSpace
• V : self.J × self.J → TauCeti.PreAdicSpace
• f (i j : self.J) : self.V (i, j) ⟶ self.U i
• f_mono (i j : self.J) : Mono (self.f i j)
• f_hasPullback (i j k : self.J) : Limits.HasPullback (self.f i j) (self.f i k)
• f_id (i : self.J) : IsIso (self.f i i)
• t (i j : self.J) : self.V (i, j) ⟶ self.V (j, i)
• t_id (i : self.J) : self.t i i = CategoryStruct.id (self.V (i, i))
• t' (i j k : self.J) : Limits.pullback (self.f i j) (self.f i k) ⟶ Limits.pullback (self.f j k) (self.f j i)
• t_fac (i j k : self.J) : CategoryStruct.comp (self.t' i j k) (Limits.pullback.snd (self.f j k) (self.f j i)) = CategoryStruct.comp (Limits.pullback.fst (self.f i j) (self.f i k)) (self.t i j)
• cocycle (i j k : self.J) : CategoryStruct.comp (self.t' i j k) (CategoryStruct.comp (self.t' j k i) (self.t' k i j)) = CategoryStruct.id (Limits.pullback (self.f i j) (self.f i k))
• f_open (i j : self.J) : IsOpenImmersion (self.f i j)

  The gluing maps are open immersions.

@[reducible, inline]

noncomputable abbrev TauCeti.PreAdicSpace.GlueData.toPresheafedSpaceGlueData (D : GlueData) : AlgebraicGeometry.PresheafedSpace.GlueData CompleteSeparatedTopCommRingCat

The glue data of presheafed spaces of complete separated topological rings underlying glue data of pre-adic spaces.

instance TauCeti.PreAdicSpace.GlueData.instHasMulticoequalizerDiagram (D : GlueData) : CategoryTheory.Limits.HasMulticoequalizer D.diagram

Glue data of pre-adic spaces glue: the gluing diagram has a colimit in 𝒱^pre. Its underlying presheafed space is the glued presheafed space, with the stalk valuations of the charts.

instance TauCeti.PreAdicSpace.GlueData.instPreservesColimitPresheafedSpaceCompleteSeparatedTopCommRingCatWalkingMultispanProdJMultispanDiagramForgetToPresheafedSpace (D : GlueData) : CategoryTheory.Limits.PreservesColimit D.diagram.multispan forgetToPresheafedSpace

The forgetful functor to presheafed spaces preserves the gluing of pre-adic spaces.

@[reducible, inline]

noncomputable abbrev TauCeti.PreAdicSpace.GlueData.isoPresheafedSpace (D : GlueData) : D.glued.toPresheafedSpace ≅ D.toPresheafedSpaceGlueData.glued

The underlying presheafed space of the glued pre-adic space is the glued presheafed space.

theorem TauCeti.PreAdicSpace.GlueData.ι_isoPresheafedSpace_inv (D : GlueData) (i : D.J) : CategoryTheory.CategoryStruct.comp (D.toPresheafedSpaceGlueData.ι i) D.isoPresheafedSpace.inv = (D.ι i).toHom

Under isoPresheafedSpace, the charts of the glued pre-adic space are those of the glued presheafed space.

theorem TauCeti.PreAdicSpace.GlueData.ι_isoPresheafedSpace_inv_assoc (D : GlueData) (i : D.J) {Z : AlgebraicGeometry.PresheafedSpace CompleteSeparatedTopCommRingCat} (h : D.glued.toPresheafedSpace ⟶ Z) : CategoryTheory.CategoryStruct.comp ((D.mapGlueData forgetToPresheafedSpace).ι i) (CategoryTheory.CategoryStruct.comp D.isoPresheafedSpace.inv h) = CategoryTheory.CategoryStruct.comp (D.ι i).toHom h

Under isoPresheafedSpace, the charts of the glued pre-adic space are those of the glued presheafed space.

instance TauCeti.PreAdicSpace.GlueData.ι_isOpenImmersion (D : GlueData) (i : D.J) : IsOpenImmersion (D.ι i)

The charts of a glued pre-adic space are open immersions.

theorem TauCeti.PreAdicSpace.GlueData.ι_jointly_surjective (D : GlueData) (x : ↑D.glued.toTopCat) : ∃ (i : D.J) (y : ↑(D.U i).toTopCat), (CategoryTheory.ConcreteCategory.hom (D.ι i).base) y = x

The charts of a glued pre-adic space are jointly surjective.

theorem TauCeti.PreAdicSpace.GlueData.ι_eq_iff_rel (D : GlueData) (i j : D.J) (x : ↑(D.U i).toTopCat) (y : ↑(D.U j).toTopCat) : (CategoryTheory.ConcreteCategory.hom (D.ι i).base) x = (CategoryTheory.ConcreteCategory.hom (D.ι j).base) y ↔ D.toPresheafedSpaceGlueData.toTopGlueData.Rel ⟨i, x⟩ ⟨j, y⟩

Points with the same image in a glued pre-adic space. Points x of U i and y of U j have the same image in the glued space if and only if there is a point z of V i j with f i j z = x and f j i (t i j z) = y.

noncomputable def TauCeti.PreAdicSpace.GlueData.vPullbackConeIsLimit (D : GlueData) (i j : D.J) : CategoryTheory.Limits.IsLimit (D.vPullbackCone i j)

V i j is the intersection of the charts U i and U j: the square formed by f i j : V i j ⟶ U i, t i j ≫ f j i : V i j ⟶ U j and the charts of the glued pre-adic space is a pullback in 𝒱^pre.

Gluing adic spaces

@[simp]

theorem TauCeti.PreAdicSpace.GlueData.isSheafy_glued_iff (D : GlueData) : D.glued.isSheafy ↔ ∀ (i : D.J), (D.U i).isSheafy

A glued pre-adic space is sheafy exactly when the pieces are. The overlaps V i j are sheafy as open subspaces of the U i, and the underlying presheafed space of the glued space is a colimit of the gluing diagram among presheafed spaces, whose structure presheaf is a limit of pushforwards of the structure sheaves of the U i and V i j. Conversely each U i is an open subspace of the glued space.

@[simp]

theorem TauCeti.PreAdicSpace.GlueData.isLocallyAffinoid_glued_iff (D : GlueData) : D.glued.isLocallyAffinoid ↔ ∀ (i : D.J), (D.U i).isLocallyAffinoid

A glued pre-adic space is locally affinoid exactly when the pieces are, since the charts of the glued space are open immersions covering it.

@[simp]

theorem TauCeti.PreAdicSpace.GlueData.isAdic_glued_iff (D : GlueData) : D.glued.isAdic ↔ ∀ (i : D.J), (D.U i).isAdic

A glued pre-adic space is an adic space exactly when the pieces are: gluing adic spaces gives an adic space, and conversely each U i is an open adic subspace of the glued space.

theorem TauCeti.PreAdicSpace.GlueData.isAdic_multispan_obj (D : GlueData) (hU : ∀ (i : D.J), (D.U i).isAdic) (j : CategoryTheory.Limits.WalkingMultispan (CategoryTheory.Limits.MultispanShape.prod D.J)) : (D.diagram.multispan.obj j).isAdic

The gluing diagram of adic pieces lies in (Adic): if every piece U i is an adic space, then so is every object of the gluing diagram, the overlaps V i j being open adic subspaces of the U i. So the gluing diagram lifts to (Adic) as isAdic.lift 𝖣.diagram.multispan (D.isAdic_multispan_obj hU).

noncomputable def TauCeti.PreAdicSpace.GlueData.gluedAdicι (D : GlueData) (hU : ∀ (i : D.J), (D.U i).isAdic) : isAdic.lift D.diagram.multispan ⋯ ⟶ (CategoryTheory.Functor.const (CategoryTheory.Limits.WalkingMultispan (CategoryTheory.Limits.MultispanShape.prod D.J))).obj { obj := D.glued, property := ⋯ }

The charts of the glued adic space of glue data of pre-adic spaces whose pieces are adic spaces, as a natural transformation from the gluing diagram in (Adic) to the constant diagram at the glued adic space. Its legs are described by gluedAdicι_app_right_hom and gluedAdicι_app_left_hom.

@[simp]

theorem TauCeti.PreAdicSpace.GlueData.gluedAdicι_app_right_hom (D : GlueData) (hU : ∀ (i : D.J), (D.U i).isAdic) (i : D.J) : ((D.gluedAdicι hU).app (CategoryTheory.Limits.WalkingMultispan.right i)).hom = D.ι i

The leg of gluedAdicι at U i is the chart ι i of the glued pre-adic space.

@[simp]

theorem TauCeti.PreAdicSpace.GlueData.gluedAdicι_app_left_hom (D : GlueData) (hU : ∀ (i : D.J), (D.U i).isAdic) (i j : D.J) : ((D.gluedAdicι hU).app (CategoryTheory.Limits.WalkingMultispan.left (i, j))).hom = CategoryTheory.CategoryStruct.comp (D.f i j) (D.ι i)

The leg of gluedAdicι at V i j is f i j ≫ ι i.

noncomputable def TauCeti.PreAdicSpace.GlueData.isColimitGluedAdicCocone (D : GlueData) (hU : ∀ (i : D.J), (D.U i).isAdic) : CategoryTheory.Limits.IsColimit { pt := { obj := D.glued, property := ⋯ }, ι := D.gluedAdicι hU }

The universal property of the glued adic space: gluing adic spaces along open immersions gives a colimit of the gluing diagram in the category (Adic) of adic spaces, with the charts gluedAdicι as legs.