Morphisms of pre-adic spaces

A morphism of pre-adic spaces is a morphism of the underlying presheafed spaces of complete separated topological rings which, on the stalk at every point, pulls the stalk valuation of that point back to the stalk valuation of its image. With these morphisms, pre-adic spaces form Wedhorn's category 𝒱^pre.

Wedhorn requires only compatibility of the stalk valuations: locality of the induced stalk maps follows, because the support of each stalk valuation is the maximal ideal of the stalk. This is PreAdicSpace.isLocalHom_stalkMap, and the corresponding compatibility of the residue-field valuations is PreAdicSpace.Hom.valuation_eq_comap.

Main definitions

• TauCeti.PreAdicSpace.Hom: morphisms of pre-adic spaces, making PreAdicSpace a category.
• TauCeti.PreAdicSpace.Hom.stalkMap: the ring homomorphism induced on stalks.
• TauCeti.PreAdicSpace.Hom.residueFieldMap: the homomorphism induced on residue fields.
• TauCeti.PreAdicSpace.Hom.ofFac: a morphism of presheafed spaces factoring a morphism of pre-adic spaces through one whose stalk maps over its image are isomorphisms is a morphism of pre-adic spaces.
• TauCeti.PreAdicSpace.forgetToPresheafedSpace, TauCeti.PreAdicSpace.forgetToTop: the forgetful functors to presheafed spaces and to topological spaces. The first is faithful and reflects isomorphisms: the inverse of an isomorphism of presheafed spaces is automatically compatible with the stalk valuations, as the case of Hom.ofFac in which it factors the identity through the isomorphism.

The design follows AlgebraicGeometry.LocallyRingedSpace, with the valuation compatibility in place of the locality condition.

References

• T. Wedhorn, Adic Spaces, arXiv:1910.05934v1, §8.1.

@[reducible, inline]

noncomputable abbrev TauCeti.PreAdicSpace.toRingPresheafedSpaceHom {X Y : PreAdicSpace} (f : X.toPresheafedSpace ⟶ Y.toPresheafedSpace) : X.toRingPresheafedSpace ⟶ Y.toRingPresheafedSpace

The morphism of presheafed spaces of rings obtained from a morphism of presheafed spaces of complete separated topological rings by forgetting the topology on sections.

Equations

• TauCeti.PreAdicSpace.toRingPresheafedSpaceHom f = (TauCeti.TopCommRingCat.isCompleteSeparated.ι.comp (CategoryTheory.forget₂ TopCommRingCat CommRingCat)).mapPresheaf.map f

structure TauCeti.PreAdicSpace.Hom (X Y : PreAdicSpace) extends X.toPresheafedSpace.Hom Y.toPresheafedSpace : Type u

A morphism of pre-adic spaces is a morphism of presheafed spaces of complete separated topological rings whose induced map on the stalk at every point x pulls the stalk valuation at x back to the stalk valuation at the image of x.

• base : ↑X.toPresheafedSpace ⟶ ↑Y.toPresheafedSpace
• c : Y.toPresheafedSpace.presheaf ⟶ (TopCat.Presheaf.pushforward TauCeti.CompleteSeparatedTopCommRingCat self.base).obj X.toPresheafedSpace.presheaf
• stalkValuation_eq (x : ↑↑X.toRingPresheafedSpace) : Y.stalkValuation ((CategoryTheory.ConcreteCategory.hom (toRingPresheafedSpaceHom self.toHom).base) x) = ValuationSpectrum.comap (CommRingCat.Hom.hom (AlgebraicGeometry.PresheafedSpace.Hom.stalkMap (toRingPresheafedSpaceHom self.toHom) x)) (X.stalkValuation x)

  The stalk valuation at the image of x is the pullback of the stalk valuation at x along the induced map on stalks. The point ranges over the presheafed space of rings so that both sides have the same type without unfolding Functor.mapPresheaf; the form with a point of X is PreAdicSpace.Hom.stalkValuation_eq_comap.

theorem TauCeti.PreAdicSpace.Hom.ext {X Y : PreAdicSpace} {f g : X.Hom Y} (h : f.toHom = g.toHom) : f = g

Morphisms of pre-adic spaces are determined by their underlying morphisms of presheafed spaces.

theorem TauCeti.PreAdicSpace.Hom.ext_iff {X Y : PreAdicSpace} {f g : X.Hom Y} : f = g ↔ f.toHom = g.toHom

def TauCeti.PreAdicSpace.id (X : PreAdicSpace) : X.Hom X

The identity morphism of a pre-adic space.

Equations

• X.id = { toHom := CategoryTheory.CategoryStruct.id X.toPresheafedSpace, stalkValuation_eq := ⋯ }

@[instance_reducible]

instance TauCeti.PreAdicSpace.instInhabitedHom (X : PreAdicSpace) : Inhabited (X.Hom X)

Equations

• X.instInhabitedHom = { default := X.id }

def TauCeti.PreAdicSpace.comp {X Y Z : PreAdicSpace} (f : X.Hom Y) (g : Y.Hom Z) : X.Hom Z

Composition of morphisms of pre-adic spaces.

Equations

• TauCeti.PreAdicSpace.comp f g = { toHom := CategoryTheory.CategoryStruct.comp f.toHom g.toHom, stalkValuation_eq := ⋯ }

@[instance_reducible]

instance TauCeti.PreAdicSpace.instCategory : CategoryTheory.Category.{u, u + 1} PreAdicSpace

The category 𝒱^pre of pre-adic spaces.

Equations

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

theorem TauCeti.PreAdicSpace.Hom.ext' {X Y : PreAdicSpace} {f g : X ⟶ Y} (h : f.toHom = g.toHom) : f = g

theorem TauCeti.PreAdicSpace.Hom.ext'_iff {X Y : PreAdicSpace} {f g : X ⟶ Y} : f = g ↔ f.toHom = g.toHom

@[simp]

theorem TauCeti.PreAdicSpace.id_toHom (X : PreAdicSpace) : (CategoryTheory.CategoryStruct.id X).toHom = CategoryTheory.CategoryStruct.id X.toPresheafedSpace

@[simp]

theorem TauCeti.PreAdicSpace.comp_toHom {X Y Z : PreAdicSpace} (f : X ⟶ Y) (g : Y ⟶ Z) : (CategoryTheory.CategoryStruct.comp f g).toHom = CategoryTheory.CategoryStruct.comp f.toHom g.toHom

theorem TauCeti.PreAdicSpace.comp_base {X Y Z : PreAdicSpace} (f : X ⟶ Y) (g : Y ⟶ Z) : (CategoryTheory.CategoryStruct.comp f g).base = CategoryTheory.CategoryStruct.comp f.base g.base

theorem TauCeti.PreAdicSpace.comp_c_app {X Y Z : PreAdicSpace} (f : X ⟶ Y) (g : Y ⟶ Z) (U : (TopologicalSpace.Opens ↑Z.toTopCat)ᵒᵖ) : (CategoryTheory.CategoryStruct.comp f g).c.app U = CategoryTheory.CategoryStruct.comp (g.c.app U) (f.c.app (Opposite.op ((TopologicalSpace.Opens.map g.base).obj (Opposite.unop U))))

def TauCeti.PreAdicSpace.forgetToPresheafedSpace : CategoryTheory.Functor PreAdicSpace (AlgebraicGeometry.PresheafedSpace CompleteSeparatedTopCommRingCat)

The forgetful functor to presheafed spaces of complete separated topological rings.

Equations

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

@[simp]

theorem TauCeti.PreAdicSpace.forgetToPresheafedSpace_map {X✝ Y✝ : PreAdicSpace} (f : X✝ ⟶ Y✝) : forgetToPresheafedSpace.map f = f.toHom

@[simp]

theorem TauCeti.PreAdicSpace.forgetToPresheafedSpace_obj (X : PreAdicSpace) : forgetToPresheafedSpace.obj X = X.toPresheafedSpace

instance TauCeti.PreAdicSpace.instFaithfulPresheafedSpaceCompleteSeparatedTopCommRingCatForgetToPresheafedSpace : forgetToPresheafedSpace.Faithful

def TauCeti.PreAdicSpace.forgetToTop : CategoryTheory.Functor PreAdicSpace TopCat

The forgetful functor to topological spaces.

Equations

• TauCeti.PreAdicSpace.forgetToTop = TauCeti.PreAdicSpace.forgetToPresheafedSpace.comp (AlgebraicGeometry.PresheafedSpace.forget TauCeti.CompleteSeparatedTopCommRingCat)

@[simp]

theorem TauCeti.PreAdicSpace.forgetToTop_obj (X : PreAdicSpace) : forgetToTop.obj X = ↑X.toPresheafedSpace

@[simp]

theorem TauCeti.PreAdicSpace.forgetToTop_map {X✝ Y✝ : PreAdicSpace} (f : X✝ ⟶ Y✝) : forgetToTop.map f = f.base

noncomputable def TauCeti.PreAdicSpace.Hom.stalkMap {X Y : PreAdicSpace} (f : X ⟶ Y) (x : ↑X.toTopCat) : Y.toRingPresheafedSpace.presheaf.stalk ((CategoryTheory.ConcreteCategory.hom f.base) x) ⟶ X.toRingPresheafedSpace.presheaf.stalk x

The ring homomorphism induced on stalks by a morphism of pre-adic spaces.

Equations

• TauCeti.PreAdicSpace.Hom.stalkMap f x = AlgebraicGeometry.PresheafedSpace.Hom.stalkMap (TauCeti.PreAdicSpace.toRingPresheafedSpaceHom f.toHom) x

theorem TauCeti.PreAdicSpace.Hom.stalkMap_def {X Y : PreAdicSpace} (f : X ⟶ Y) (x : ↑X.toTopCat) : stalkMap f x = AlgebraicGeometry.PresheafedSpace.Hom.stalkMap (toRingPresheafedSpaceHom f.toHom) x

The stalk map is the stalk map of the underlying morphism of presheafed spaces of rings.

theorem TauCeti.PreAdicSpace.Hom.stalkValuation_eq_comap {X Y : PreAdicSpace} (f : X ⟶ Y) (x : ↑X.toTopCat) : Y.stalkValuation ((CategoryTheory.ConcreteCategory.hom f.base) x) = ValuationSpectrum.comap (CommRingCat.Hom.hom (stalkMap f x)) (X.stalkValuation x)

The stalk valuation at the image of x is the pullback of the stalk valuation at x.

@[simp]

theorem TauCeti.PreAdicSpace.stalkMap_id (X : PreAdicSpace) (x : ↑X.toTopCat) : Hom.stalkMap (CategoryTheory.CategoryStruct.id X) x = CategoryTheory.CategoryStruct.id (X.toRingPresheafedSpace.presheaf.stalk x)

The stalk maps of the identity are identities.

theorem TauCeti.PreAdicSpace.stalkMap_comp {X Y Z : PreAdicSpace} (f : X ⟶ Y) (g : Y ⟶ Z) (x : ↑X.toTopCat) : Hom.stalkMap (CategoryTheory.CategoryStruct.comp f g) x = CategoryTheory.CategoryStruct.comp (Hom.stalkMap g ((CategoryTheory.ConcreteCategory.hom f.base) x)) (Hom.stalkMap f x)

The stalk maps of a composite are the composites of the stalk maps.

instance TauCeti.PreAdicSpace.isLocalHom_stalkMap {X Y : PreAdicSpace} (f : X ⟶ Y) (x : ↑X.toTopCat) : IsLocalHom (CommRingCat.Hom.hom (Hom.stalkMap f x))

The stalk maps of a morphism of pre-adic spaces are local homomorphisms. This is forced by compatibility with the stalk valuations, whose supports are the maximal ideals of the stalks.

noncomputable def TauCeti.PreAdicSpace.Hom.residueFieldMap {X Y : PreAdicSpace} (f : X ⟶ Y) (x : ↑X.toTopCat) : IsLocalRing.ResidueField ↑(Y.toRingPresheafedSpace.presheaf.stalk ((CategoryTheory.ConcreteCategory.hom f.base) x)) →+* IsLocalRing.ResidueField ↑(X.toRingPresheafedSpace.presheaf.stalk x)

The homomorphism induced on residue fields by a morphism of pre-adic spaces.

Equations

• TauCeti.PreAdicSpace.Hom.residueFieldMap f x = IsLocalRing.ResidueField.map (CommRingCat.Hom.hom (TauCeti.PreAdicSpace.Hom.stalkMap f x))

theorem TauCeti.PreAdicSpace.Hom.residueFieldMap_def {X Y : PreAdicSpace} (f : X ⟶ Y) (x : ↑X.toTopCat) : residueFieldMap f x = IsLocalRing.ResidueField.map (CommRingCat.Hom.hom (stalkMap f x))

The residue-field map is induced by the local stalk map.

theorem TauCeti.PreAdicSpace.Hom.residueFieldMap_comp_residue {X Y : PreAdicSpace} (f : X ⟶ Y) (x : ↑X.toTopCat) : (residueFieldMap f x).comp (IsLocalRing.residue ↑(Y.toRingPresheafedSpace.presheaf.stalk ((CategoryTheory.ConcreteCategory.hom f.base) x))) = (IsLocalRing.residue ↑(X.toRingPresheafedSpace.presheaf.stalk x)).comp (CommRingCat.Hom.hom (stalkMap f x))

The residue square: the residue-field map composed with the residue map at the image of x is the residue map at x composed with the stalk map.

theorem TauCeti.PreAdicSpace.Hom.residueFieldMap_residue {X Y : PreAdicSpace} (f : X ⟶ Y) (x : ↑X.toTopCat) (a : ↑(Y.toRingPresheafedSpace.presheaf.stalk ((CategoryTheory.ConcreteCategory.hom f.base) x))) : (residueFieldMap f x) ((IsLocalRing.residue ↑(Y.toRingPresheafedSpace.presheaf.stalk ((CategoryTheory.ConcreteCategory.hom f.base) x))) a) = (IsLocalRing.residue ↑(X.toRingPresheafedSpace.presheaf.stalk x)) ((CategoryTheory.ConcreteCategory.hom (stalkMap f x)) a)

The residue-field map sends the residue class of a stalk element to the residue class of its image under the stalk map.

@[simp]

theorem TauCeti.PreAdicSpace.residueFieldMap_id (X : PreAdicSpace) (x : ↑X.toTopCat) : Hom.residueFieldMap (CategoryTheory.CategoryStruct.id X) x = RingHom.id (IsLocalRing.ResidueField ↑(X.toRingPresheafedSpace.presheaf.stalk ((CategoryTheory.ConcreteCategory.hom (CategoryTheory.CategoryStruct.id X).base) x)))

The residue-field maps of the identity are identities.

@[simp]

theorem TauCeti.PreAdicSpace.residueFieldMap_comp {X Y Z : PreAdicSpace} (f : X ⟶ Y) (g : Y ⟶ Z) (x : ↑X.toTopCat) : Hom.residueFieldMap (CategoryTheory.CategoryStruct.comp f g) x = (Hom.residueFieldMap f x).comp (Hom.residueFieldMap g ((CategoryTheory.ConcreteCategory.hom f.base) x))

The residue-field maps of a composite are the composites of the residue-field maps.

theorem TauCeti.PreAdicSpace.Hom.valuation_eq_comap {X Y : PreAdicSpace} (f : X ⟶ Y) (x : ↑X.toTopCat) : Y.valuation ((CategoryTheory.ConcreteCategory.hom f.base) x) = ValuationSpectrum.comap (residueFieldMap f x) (X.valuation x)

The residue-field valuation at the image of x is the pullback of the residue-field valuation at x along the induced map on residue fields.

instance TauCeti.PreAdicSpace.isIso_stalkMap {X Y : PreAdicSpace} (f : X ⟶ Y) [CategoryTheory.IsIso f.toHom] (x : ↑X.toTopCat) : CategoryTheory.IsIso (Hom.stalkMap f x)

The stalk maps of a morphism of pre-adic spaces whose underlying morphism of presheafed spaces is an isomorphism are isomorphisms.

def TauCeti.PreAdicSpace.Hom.ofFac {X Y Z : PreAdicSpace} (i : X ⟶ Z) (j : Y ⟶ Z) (g : X.toPresheafedSpace ⟶ Y.toPresheafedSpace) [hj : ∀ (x : ↑X.toTopCat), CategoryTheory.IsIso (stalkMap j ((CategoryTheory.ConcreteCategory.hom g.base) x))] (h : CategoryTheory.CategoryStruct.comp g j.toHom = i.toHom) : X ⟶ Y

A morphism of presheafed spaces g with g ≫ j = i, for morphisms i : X ⟶ Z and j : Y ⟶ Z of pre-adic spaces such that the stalk maps of j at the points of the image of g are isomorphisms, is a morphism of pre-adic spaces: pulling back along those invertible stalk maps recovers the compatibility of g with the stalk valuations from that of i and j.

Equations

• TauCeti.PreAdicSpace.Hom.ofFac i j g h = { toHom := g, stalkValuation_eq := ⋯ }

@[simp]

theorem TauCeti.PreAdicSpace.Hom.ofFac_toHom {X Y Z : PreAdicSpace} (i : X ⟶ Z) (j : Y ⟶ Z) (g : X.toPresheafedSpace ⟶ Y.toPresheafedSpace) [∀ (x : ↑X.toTopCat), CategoryTheory.IsIso (stalkMap j ((CategoryTheory.ConcreteCategory.hom g.base) x))] (h : CategoryTheory.CategoryStruct.comp g j.toHom = i.toHom) : (ofFac i j g h).toHom = g

instance TauCeti.PreAdicSpace.isIso_toHom {X Y : PreAdicSpace} (f : X ⟶ Y) [CategoryTheory.IsIso f] : CategoryTheory.IsIso f.toHom

The underlying morphism of presheafed spaces of an isomorphism of pre-adic spaces is an isomorphism. Instance search does not see forgetToPresheafedSpace.map f as f.toHom, so Mathlib's Functor.map_isIso does not supply this.

instance TauCeti.PreAdicSpace.instReflectsIsomorphismsPresheafedSpaceCompleteSeparatedTopCommRingCatForgetToPresheafedSpace : forgetToPresheafedSpace.ReflectsIsomorphisms

The forgetful functor to presheafed spaces reflects isomorphisms: the inverse of the underlying isomorphism of presheafed spaces factors the identity through f, whose stalk maps are isomorphisms, so it is a morphism of pre-adic spaces by Hom.ofFac.

theorem TauCeti.PreAdicSpace.isIso_of_isIso_toHom {X Y : PreAdicSpace} (f : X ⟶ Y) [hf : CategoryTheory.IsIso f.toHom] : CategoryTheory.IsIso f

A morphism of pre-adic spaces whose underlying morphism of presheafed spaces is an isomorphism is an isomorphism: the converse of isIso_toHom, by reflection of isomorphisms along the forgetful functor.