Descending a pre-adic structure along a jointly surjective family #

Let X i be a family of pre-adic spaces, Z a presheafed space of complete separated topological rings and π i : X i ⟶ Z morphisms of presheafed spaces which are jointly surjective on points and induce isomorphisms on all stalks. Then every stalk of Z is local, being isomorphic to a stalk of some X i, and each point π i x of Z receives a valuation, the pullback of the stalk valuation of X i at x along the stalk map. If these valuations agree for any two points with the same image, they make Z a pre-adic space descend X π, and every π i a morphism of pre-adic spaces X i ⟶ descend X π.

The agreement hypothesis holds as soon as any two points with the same image come from a common point w of a pre-adic space W, through morphisms of pre-adic spaces g₁ : W ⟶ X i and g₂ : W ⟶ X j with g₁ ≫ π i = g₂ ≫ π j (comap_stalkMap_base_eq_of_comp_eq). Two cases of this are the following.

A single surjection π : X ⟶ Z, the family indexed by Unit, with a group of automorphisms g of X acting transitively on the fibres of π and satisfying g ≫ π = π. This is how a quotient of a pre-adic space by a group acting with wandering neighbourhoods, such as the adic Fargues–Fontaine curve, becomes a pre-adic space.
The charts U i ⟶ Z of a presheafed space glued from pre-adic spaces along open immersions, where two points with the same image come from a point of an overlap V i j. This is how glued pre-adic spaces are constructed (TauCeti.PreAdicSpace.GlueData).

Main definitions #

TauCeti.PreAdicSpace.descend: the pre-adic space with underlying presheafed space Z.
TauCeti.PreAdicSpace.toDescend: π i as a morphism of pre-adic spaces X i ⟶ descend X π.

Main results #

TauCeti.PreAdicSpace.stalkValuation_descend_base: the stalk valuation of descend X π at π i x is the pullback of the stalk valuation of X i at x.
TauCeti.PreAdicSpace.comap_stalkMap_base_eq_of_comp_eq: points with the same image under π that come from a common point through morphisms of pre-adic spaces induce the same valuation.

References #

T. Wedhorn, Adic Spaces, arXiv:1910.05934v1, §8.1, for the category 𝒱^pre.

source

noncomputable def TauCeti.PreAdicSpace.descendStalkIso {ι : Type v} {X : ι → PreAdicSpace} {Z : AlgebraicGeometry.PresheafedSpace CompleteSeparatedTopCommRingCat} {π : (i : ι) → (X i).toPresheafedSpace ⟶ Z} (hsurj : ∀ (z : ↑↑Z), ∃ (i : ι) (x : ↑(X i).toTopCat), (CategoryTheory.ConcreteCategory.hom (π i).base) x = z) (hiso : ∀ (i : ι) (x : ↑(X i).toTopCat), CategoryTheory.IsIso (AlgebraicGeometry.PresheafedSpace.Hom.stalkMap (toRingPresheafedSpaceHom (π i)) x)) (z : ↑↑Z) :

((TopCommRingCat.isCompleteSeparated.ι.comp (CategoryTheory.forget₂ TopCommRingCat CommRingCat)).mapPresheaf.obj Z).presheaf.stalk z ≅ (X ⋯.choose).toRingPresheafedSpace.presheaf.stalk ⋯.choose

The stalk of Z at z is identified with the stalk of X i at a chosen preimage x of z, π i x = z, through the stalk map of π i. This is the identification through which descend transports local rings and valuations.

Instances For

source

noncomputable def TauCeti.PreAdicSpace.descend {ι : Type v} (X : ι → PreAdicSpace) {Z : AlgebraicGeometry.PresheafedSpace CompleteSeparatedTopCommRingCat} (π : (i : ι) → (X i).toPresheafedSpace ⟶ Z) (hsurj : ∀ (z : ↑↑Z), ∃ (i : ι) (x : ↑(X i).toTopCat), (CategoryTheory.ConcreteCategory.hom (π i).base) x = z) (hiso : ∀ (i : ι) (x : ↑(X i).toTopCat), CategoryTheory.IsIso (AlgebraicGeometry.PresheafedSpace.Hom.stalkMap (toRingPresheafedSpaceHom (π i)) x)) :

PreAdicSpace

The pre-adic structure descended along π. For morphisms of presheafed spaces π i : X i ⟶ Z from pre-adic spaces, jointly surjective on points and with invertible stalk maps, the presheafed space Z with its stalks, local through descendStalkIso, and the valuation at z descended from a chosen preimage of z. When two points with the same image induce the same valuation on the stalk of Z (hcompat), the valuation at π i x is the one descended from x (stalkValuation_descend_base), and every π i is a morphism of pre-adic spaces (toDescend).

Instances For

source

theorem TauCeti.PreAdicSpace.descendStalkIso_hom {ι : Type v} {X : ι → PreAdicSpace} {Z : AlgebraicGeometry.PresheafedSpace CompleteSeparatedTopCommRingCat} {π : (i : ι) → (X i).toPresheafedSpace ⟶ Z} (hsurj : ∀ (z : ↑↑Z), ∃ (i : ι) (x : ↑(X i).toTopCat), (CategoryTheory.ConcreteCategory.hom (π i).base) x = z) (hiso : ∀ (i : ι) (x : ↑(X i).toTopCat), CategoryTheory.IsIso (AlgebraicGeometry.PresheafedSpace.Hom.stalkMap (toRingPresheafedSpaceHom (π i)) x)) (z : ↑↑Z) :

(descendStalkIso hsurj hiso z).hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (AlgebraicGeometry.PresheafedSpace.Hom.stalkMap (toRingPresheafedSpaceHom (π ⋯.choose)) ⋯.choose)

descendStalkIso is the identification of the stalks at z and at π i of its chosen preimage, followed by the stalk map of π i.

source

@[simp]

theorem TauCeti.PreAdicSpace.descend_toPresheafedSpace {ι : Type v} {X : ι → PreAdicSpace} {Z : AlgebraicGeometry.PresheafedSpace CompleteSeparatedTopCommRingCat} {π : (i : ι) → (X i).toPresheafedSpace ⟶ Z} (hsurj : ∀ (z : ↑↑Z), ∃ (i : ι) (x : ↑(X i).toTopCat), (CategoryTheory.ConcreteCategory.hom (π i).base) x = z) (hiso : ∀ (i : ι) (x : ↑(X i).toTopCat), CategoryTheory.IsIso (AlgebraicGeometry.PresheafedSpace.Hom.stalkMap (toRingPresheafedSpaceHom (π i)) x)) :

(descend X π hsurj hiso).toPresheafedSpace = Z

The presheafed space underlying the descended pre-adic space is Z.

source

theorem TauCeti.PreAdicSpace.comap_stalkMap_base_eq_of_comp_eq {ι : Type v} {X : ι → PreAdicSpace} {Z : AlgebraicGeometry.PresheafedSpace CompleteSeparatedTopCommRingCat} {π : (i : ι) → (X i).toPresheafedSpace ⟶ Z} {W : PreAdicSpace} {i j : ι} (g₁ : W ⟶ X i) (g₂ : W ⟶ X j) (hg : CategoryTheory.CategoryStruct.comp g₁.toHom (π i) = CategoryTheory.CategoryStruct.comp g₂.toHom (π j)) (w : ↑W.toTopCat) (h : (CategoryTheory.ConcreteCategory.hom (π i).base) ((CategoryTheory.ConcreteCategory.hom g₁.base) w) = (CategoryTheory.ConcreteCategory.hom (π j).base) ((CategoryTheory.ConcreteCategory.hom g₂.base) w)) :

Points coming from a common point induce the same valuation. If morphisms of pre-adic spaces g₁ : W ⟶ X i and g₂ : W ⟶ X j satisfy g₁ ≫ π i = g₂ ≫ π j, then for every point w of W the valuations on the stalk of Z at π i (g₁ w) = π j (g₂ w) descended from g₁ w and from g₂ w agree. This supplies the compatibility hypothesis of descend: for a group of automorphisms of a single X over Z with g₁ = 𝟙, and for glued spaces with W an overlap.