The presentation-limit presheaf and its stalks as rings

The presentation-limit presheaf is naturally valued in complete separated topological commutative rings. Stalks, however, are algebraic colimits: their topology is discarded. This file forgets the topology on sections, packages the result as a CommRingCat-valued presheafed space, and constructs the canonical germ map from the coordinate ring of every rational neighbourhood to the stalk.

Main definitions

• TauCeti.ValuationSpectrum.presentationLimitPresheafInCommRingCat is the underlying commutative-ring presheaf.
• TauCeti.ValuationSpectrum.presentationLimitPresheafedSpace packages it on Spa(A,A⁺).
• TauCeti.ValuationSpectrum.presentationLimitRationalGerm maps the coordinate ring of a rational neighbourhood to the stalk at a point.

Main result

TauCeti.ValuationSpectrum.presentationLimitRationalGerm_res says that these rational germ maps are compatible with the comparison morphisms between rational coordinate rings. exists_presentationLimitRationalGerm_eq says every germ comes from a rational coordinate ring, and exists_map_homOfRationalSubsetSubset_eq_zero says a zero germ restricts to zero on some smaller rational neighbourhood.

References

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

noncomputable def TauCeti.ValuationSpectrum.presentationLimitPresheafInCommRingCat {A : Type v} [CommRing A] [TopologicalSpace A] [IsTopologicalRing A] (P : Huber.PairOfDefinition A) (Aplus : Subring A) : TopCat.Presheaf CommRingCat ↧↑(spa Aplus)

The presentation-limit presheaf after forgetting the topology on its section rings.

This is the presheaf whose stalks are the ring colimits used in the locally ringed-space structure. The topology is forgotten only after taking the limits that define sections.

Equations

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

@[simp]

theorem TauCeti.ValuationSpectrum.presentationLimitPresheafInCommRingCat_def {A : Type v} [CommRing A] [TopologicalSpace A] [IsTopologicalRing A] (P : Huber.PairOfDefinition A) (Aplus : Subring A) : presentationLimitPresheafInCommRingCat P Aplus = (presentationLimitPresheaf P Aplus).comp (TopCommRingCat.isCompleteSeparated.ι.comp (CategoryTheory.forget₂ TopCommRingCat CommRingCat))

Forgetting the topology of the presentation-limit presheaf gives its ring presheaf.

theorem TauCeti.ValuationSpectrum.presentationLimitPresheafInCommRingCat_obj {A : Type v} [CommRing A] [TopologicalSpace A] [IsTopologicalRing A] (P : Huber.PairOfDefinition A) (Aplus : Subring A) (V : (TopologicalSpace.Opens ↑(spa Aplus))ᵒᵖ) : (presentationLimitPresheafInCommRingCat P Aplus).obj V = (TopCommRingCat.isCompleteSeparated.ι.comp (CategoryTheory.forget₂ TopCommRingCat CommRingCat)).obj (presentationLimit Aplus (Opposite.unop V))

Evaluating the underlying ring presheaf on an open gives the underlying ring of the presentation limit over that open.

theorem TauCeti.ValuationSpectrum.presentationLimitPresheafInCommRingCat_map {A : Type v} [CommRing A] [TopologicalSpace A] [IsTopologicalRing A] (P : Huber.PairOfDefinition A) (Aplus : Subring A) {V W : (TopologicalSpace.Opens ↑(spa Aplus))ᵒᵖ} (h : V ⟶ W) : CategoryTheory.CategoryStruct.comp ((presentationLimitPresheafInCommRingCat P Aplus).map h) (CategoryTheory.eqToHom ⋯) = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) ((TopCommRingCat.isCompleteSeparated.ι.comp (CategoryTheory.forget₂ TopCommRingCat CommRingCat)).map (presentationLimitMap ⋯))

Restriction in the underlying ring presheaf is the underlying morphism of the reindexing map between presentation limits. The equality transports account for the sealed evaluation theorem presentationLimitPresheaf_obj.

noncomputable def TauCeti.ValuationSpectrum.presentationLimitPresheafedSpace {A : Type v} [CommRing A] [TopologicalSpace A] [IsTopologicalRing A] (P : Huber.PairOfDefinition A) (Aplus : Subring A) : AlgebraicGeometry.PresheafedSpace CommRingCat

Spa(A,A⁺) equipped with the underlying commutative-ring presentation-limit presheaf.

Equations

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

@[simp]

theorem TauCeti.ValuationSpectrum.presentationLimitPresheafedSpace_carrier {A : Type v} [CommRing A] [TopologicalSpace A] [IsTopologicalRing A] (P : Huber.PairOfDefinition A) (Aplus : Subring A) : ↑(presentationLimitPresheafedSpace P Aplus) = ↧↑(spa Aplus)

@[simp]

theorem TauCeti.ValuationSpectrum.presentationLimitPresheafedSpace_presheaf {A : Type v} [CommRing A] [TopologicalSpace A] [IsTopologicalRing A] (P : Huber.PairOfDefinition A) (Aplus : Subring A) : (presentationLimitPresheafedSpace P Aplus).presheaf ≍ (presentationLimitPresheaf P Aplus).comp (TopCommRingCat.isCompleteSeparated.ι.comp (CategoryTheory.forget₂ TopCommRingCat CommRingCat))

noncomputable def TauCeti.ValuationSpectrum.presentationLimitRationalIsoInCommRingCat {A : Type v} [CommRing A] [TopologicalSpace A] [IsTopologicalRing A] {P : Huber.PairOfDefinition A} {Aplus : Subring A} (hAplus : ∀ ⦃a : A⦄, a ∈ Aplus → Huber.IsPowerBounded a) (p : P.Presentation) (hp : IsOpen ↑(Ideal.span ↑p.num)) : (presentationLimitPresheafInCommRingCat P Aplus).obj (Opposite.op (spaBasicOpen Aplus p.num p.den)) ≅ (TopCommRingCat.isCompleteSeparated.ι.comp (CategoryTheory.forget₂ TopCommRingCat CommRingCat)).obj p.completionLocObj

On a rational open, the underlying ring of the presentation limit is the underlying ring of its rational coordinate ring.

Equations

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

@[simp]

theorem TauCeti.ValuationSpectrum.presentationLimitRationalIsoInCommRingCat_hom {A : Type v} [CommRing A] [TopologicalSpace A] [IsTopologicalRing A] {P : Huber.PairOfDefinition A} {Aplus : Subring A} (hAplus : ∀ ⦃a : A⦄, a ∈ Aplus → Huber.IsPowerBounded a) (p : P.Presentation) (hp : IsOpen ↑(Ideal.span ↑p.num)) : (presentationLimitRationalIsoInCommRingCat hAplus p hp).hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) ((TopCommRingCat.isCompleteSeparated.ι.comp (CategoryTheory.forget₂ TopCommRingCat CommRingCat)).map (presentationLimitRationalIso Aplus hAplus p hp).hom)

The rational comparison isomorphism is the underlying ring map of the comparison presentationLimitRationalIso, after transporting along presentationLimitPresheaf_obj.

@[simp]

theorem TauCeti.ValuationSpectrum.presentationLimitRationalIsoInCommRingCat_inv {A : Type v} [CommRing A] [TopologicalSpace A] [IsTopologicalRing A] {P : Huber.PairOfDefinition A} {Aplus : Subring A} (hAplus : ∀ ⦃a : A⦄, a ∈ Aplus → Huber.IsPowerBounded a) (p : P.Presentation) (hp : IsOpen ↑(Ideal.span ↑p.num)) : (presentationLimitRationalIsoInCommRingCat hAplus p hp).inv = CategoryTheory.CategoryStruct.comp ((TopCommRingCat.isCompleteSeparated.ι.comp (CategoryTheory.forget₂ TopCommRingCat CommRingCat)).map (presentationLimitRationalIso Aplus hAplus p hp).inv) (CategoryTheory.eqToHom ⋯)

The inverse rational comparison is the underlying inverse comparison followed by transport along presentationLimitPresheafInCommRingCat_obj.

theorem TauCeti.ValuationSpectrum.presentationLimitRationalIsoInCommRingCat_inv_comp_map_comp_hom {A : Type v} [CommRing A] [TopologicalSpace A] [IsTopologicalRing A] {P : Huber.PairOfDefinition A} {Aplus : Subring A} (hAplus : ∀ ⦃a : A⦄, a ∈ Aplus → Huber.IsPowerBounded a) (p q : P.Presentation) (hp : IsOpen ↑(Ideal.span ↑p.num)) (hq : IsOpen ↑(Ideal.span ↑q.num)) (h : spaBasicOpen Aplus q.num q.den ≤ spaBasicOpen Aplus p.num p.den) : CategoryTheory.CategoryStruct.comp (presentationLimitRationalIsoInCommRingCat hAplus p hp).inv (CategoryTheory.CategoryStruct.comp ((presentationLimitPresheafInCommRingCat P Aplus).map (CategoryTheory.homOfLE h).op) (presentationLimitRationalIsoInCommRingCat hAplus q hq).hom) = (TopCommRingCat.isCompleteSeparated.ι.comp (CategoryTheory.forget₂ TopCommRingCat CommRingCat)).map (homOfRationalSubsetSubset Aplus hAplus ⋯)

The rational-open comparison isomorphisms identify restriction with the comparison map of rational coordinate rings, after forgetting topology.

noncomputable def TauCeti.ValuationSpectrum.presentationLimitRationalGerm {A : Type v} [CommRing A] [TopologicalSpace A] [IsTopologicalRing A] {P : Huber.PairOfDefinition A} {Aplus : Subring A} (hAplus : ∀ ⦃a : A⦄, a ∈ Aplus → Huber.IsPowerBounded a) (p : P.Presentation) (hp : IsOpen ↑(Ideal.span ↑p.num)) (x : ↑(spa Aplus)) (hx : x ∈ spaBasicOpen Aplus p.num p.den) : (TopCommRingCat.isCompleteSeparated.ι.comp (CategoryTheory.forget₂ TopCommRingCat CommRingCat)).obj p.completionLocObj ⟶ (presentationLimitPresheafInCommRingCat P Aplus).stalk x

The germ map from a rational coordinate ring to the stalk at a point of the corresponding rational open. It first identifies the coordinate ring with the presentation-limit sections and then applies the ordinary presheaf germ map.

Equations

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

@[simp]

theorem TauCeti.ValuationSpectrum.presentationLimitRationalGerm_def {A : Type v} [CommRing A] [TopologicalSpace A] [IsTopologicalRing A] {P : Huber.PairOfDefinition A} {Aplus : Subring A} (hAplus : ∀ ⦃a : A⦄, a ∈ Aplus → Huber.IsPowerBounded a) (p : P.Presentation) (hp : IsOpen ↑(Ideal.span ↑p.num)) (x : ↑(spa Aplus)) (hx : x ∈ spaBasicOpen Aplus p.num p.den) : presentationLimitRationalGerm hAplus p hp x hx = CategoryTheory.CategoryStruct.comp (presentationLimitRationalIsoInCommRingCat hAplus p hp).inv ((presentationLimitPresheafInCommRingCat P Aplus).germ (spaBasicOpen Aplus p.num p.den) x hx)

The rational germ map is the inverse comparison isomorphism followed by the presheaf germ map on the rational open.

theorem TauCeti.ValuationSpectrum.presentationLimitRationalGerm_res {A : Type v} [CommRing A] [TopologicalSpace A] [IsTopologicalRing A] {P : Huber.PairOfDefinition A} {Aplus : Subring A} (hAplus : ∀ ⦃a : A⦄, a ∈ Aplus → Huber.IsPowerBounded a) (p q : P.Presentation) (hp : IsOpen ↑(Ideal.span ↑p.num)) (hq : IsOpen ↑(Ideal.span ↑q.num)) (h : spaBasicOpen Aplus q.num q.den ≤ spaBasicOpen Aplus p.num p.den) (x : ↑(spa Aplus)) (hx : x ∈ spaBasicOpen Aplus q.num q.den) : CategoryTheory.CategoryStruct.comp ((TopCommRingCat.isCompleteSeparated.ι.comp (CategoryTheory.forget₂ TopCommRingCat CommRingCat)).map (homOfRationalSubsetSubset Aplus hAplus ⋯)) (presentationLimitRationalGerm hAplus q hq x hx) = presentationLimitRationalGerm hAplus p hp x ⋯

Rational germ maps commute with restriction: passing from a rational neighbourhood to a smaller one does not change the resulting germ in the stalk.

theorem TauCeti.ValuationSpectrum.presentationLimitRationalGerm_res_assoc {A : Type v} [CommRing A] [TopologicalSpace A] [IsTopologicalRing A] {P : Huber.PairOfDefinition A} {Aplus : Subring A} (hAplus : ∀ ⦃a : A⦄, a ∈ Aplus → Huber.IsPowerBounded a) (p q : P.Presentation) (hp : IsOpen ↑(Ideal.span ↑p.num)) (hq : IsOpen ↑(Ideal.span ↑q.num)) (h : spaBasicOpen Aplus q.num q.den ≤ spaBasicOpen Aplus p.num p.den) (x : ↑(spa Aplus)) (hx : x ∈ spaBasicOpen Aplus q.num q.den) {Z : CommRingCat} (h✝ : (presentationLimitPresheafInCommRingCat P Aplus).stalk x ⟶ Z) : CategoryTheory.CategoryStruct.comp ((CategoryTheory.forget₂ TopCommRingCat CommRingCat).map (TopCommRingCat.isCompleteSeparated.ι.map (homOfRationalSubsetSubset Aplus hAplus ⋯))) (CategoryTheory.CategoryStruct.comp (presentationLimitRationalGerm hAplus q hq x hx) h✝) = CategoryTheory.CategoryStruct.comp (presentationLimitRationalGerm hAplus p hp x ⋯) h✝

Rational germ maps commute with restriction: passing from a rational neighbourhood to a smaller one does not change the resulting germ in the stalk.

theorem TauCeti.ValuationSpectrum.exists_presentationLimitRationalGerm_eq {A : Type v} [CommRing A] [TopologicalSpace A] [IsTopologicalRing A] {P : Huber.PairOfDefinition A} {Aplus : Subring A} (hAplus : ∀ ⦃a : A⦄, a ∈ Aplus → Huber.IsPowerBounded a) (x : ↑(spa Aplus)) (t : ↑((presentationLimitPresheafInCommRingCat P Aplus).stalk x)) : ∃ (p : P.Presentation) (hp : IsOpen ↑(Ideal.span ↑p.num)) (hx : x ∈ spaBasicOpen Aplus p.num p.den) (a : ↑((TopCommRingCat.isCompleteSeparated.ι.comp (CategoryTheory.forget₂ TopCommRingCat CommRingCat)).obj p.completionLocObj)), (CommRingCat.Hom.hom (presentationLimitRationalGerm hAplus p hp x hx)) a = t

Every germ is a rational germ: each element of the stalk at x is the germ of an element of the coordinate ring A⟨p⟩ of some rational neighbourhood R(p) of x.

theorem TauCeti.ValuationSpectrum.exists_map_homOfRationalSubsetSubset_eq_zero {A : Type v} [CommRing A] [TopologicalSpace A] [IsTopologicalRing A] {P : Huber.PairOfDefinition A} {Aplus : Subring A} (hAplus : ∀ ⦃a : A⦄, a ∈ Aplus → Huber.IsPowerBounded a) {x : ↑(spa Aplus)} {p : P.Presentation} {hp : IsOpen ↑(Ideal.span ↑p.num)} {hx : x ∈ spaBasicOpen Aplus p.num p.den} {a : ↑((TopCommRingCat.isCompleteSeparated.ι.comp (CategoryTheory.forget₂ TopCommRingCat CommRingCat)).obj p.completionLocObj)} (ha : (CommRingCat.Hom.hom (presentationLimitRationalGerm hAplus p hp x hx)) a = 0) : ∃ (q : P.Presentation) (_ : IsOpen ↑(Ideal.span ↑q.num)) (_ : x ∈ spaBasicOpen Aplus q.num q.den) (h : spaBasicOpen Aplus q.num q.den ≤ spaBasicOpen Aplus p.num p.den), (CommRingCat.Hom.hom ((TopCommRingCat.isCompleteSeparated.ι.comp (CategoryTheory.forget₂ TopCommRingCat CommRingCat)).map (homOfRationalSubsetSubset Aplus hAplus ⋯))) a = 0

A rational germ vanishes only if a restriction does: if an element of A⟨p⟩ has zero germ at x, then its image in the coordinate ring of some smaller rational neighbourhood of x is already zero.