The stalks of the presentation-limit presheaf are local

Let x be a point of X = Spa(A,A⁺) and let v_x be the valuation on the stalk 𝒪_{X,x} of the presentation-limit presheaf constructed in Stalk.Valuation. This file proves that a germ is a unit exactly when v_x does not vanish on it. Since the support of v_x is a prime ideal, the nonunits of 𝒪_{X,x} then form an ideal: the stalk is a local ring whose maximal ideal is the support of v_x. Consequently v_x factors through the residue field of 𝒪_{X,x}, which is the form in which the valuations at the points of a pre-adic space are recorded.

The unit criterion is the concrete description of the local structure of 𝒪_{X,x}: a germ is invertible near x exactly when it does not vanish at x. The residue-field valuation presentationLimitStalkResidueValuation is the valuation on the residue field k(x) attached to x; it is the datum Wedhorn's category 𝒱^pre records at each point (Wedhorn §8.1).

As in Stalk.Valuation, A⁺ is assumed to consist of power-bounded elements and to contain the ring of definition of the chosen pair of definition.

Main results

• TauCeti.ValuationSpectrum.isUnit_iff_notMem_supp_presentationLimitStalkValuation: a germ is a unit exactly when it lies outside the support of the stalk valuation.
• TauCeti.ValuationSpectrum.isLocalRing_stalk_presentationLimitPresheafInCommRingCat: every stalk of the presentation-limit presheaf is a local ring.
• TauCeti.ValuationSpectrum.supp_presentationLimitStalkValuation: its maximal ideal is the support of the stalk valuation.

Main definitions

• TauCeti.ValuationSpectrum.presentationLimitStalkResidueValuation: the valuation on the residue field of the stalk through which the stalk valuation factors, characterised by comap_residue_presentationLimitStalkResidueValuation and eq_presentationLimitStalkResidueValuation.

References

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

theorem TauCeti.ValuationSpectrum.isUnit_iff_notMem_supp_presentationLimitStalkValuation {A : Type v} [CommRing A] [TopologicalSpace A] [IsTopologicalRing A] {P : Huber.PairOfDefinition A} {Aplus : Subring A} (hAplus : ∀ ⦃a : A⦄, a ∈ Aplus → Huber.IsPowerBounded a) (hP : P.ringOfDefinition ≤ Aplus) {x : ↑(spa Aplus)} (t : ↑((presentationLimitPresheafInCommRingCat P Aplus).stalk x)) : IsUnit t ↔ t ∉ (presentationLimitStalkValuation hAplus hP x).supp

A germ is a unit exactly when the stalk valuation does not vanish on it: an element of the stalk at x of the presentation-limit presheaf is a unit if and only if it lies outside the support of presentationLimitStalkValuation.

theorem TauCeti.ValuationSpectrum.isLocalRing_stalk_presentationLimitPresheafInCommRingCat {A : Type v} [CommRing A] [TopologicalSpace A] [IsTopologicalRing A] {P : Huber.PairOfDefinition A} {Aplus : Subring A} (hAplus : ∀ ⦃a : A⦄, a ∈ Aplus → Huber.IsPowerBounded a) (hP : P.ringOfDefinition ≤ Aplus) (x : ↑(spa Aplus)) : IsLocalRing ↑((presentationLimitPresheafInCommRingCat P Aplus).stalk x)

The stalks of the presentation-limit presheaf are local rings: its nonunits form the support of the stalk valuation, which is a proper ideal.

@[simp]

theorem TauCeti.ValuationSpectrum.supp_presentationLimitStalkValuation {A : Type v} [CommRing A] [TopologicalSpace A] [IsTopologicalRing A] {P : Huber.PairOfDefinition A} {Aplus : Subring A} (hAplus : ∀ ⦃a : A⦄, a ∈ Aplus → Huber.IsPowerBounded a) (hP : P.ringOfDefinition ≤ Aplus) (x : ↑(spa Aplus)) : (presentationLimitStalkValuation hAplus hP x).supp = IsLocalRing.maximalIdeal ↑((presentationLimitPresheafInCommRingCat P Aplus).stalk x)

The maximal ideal of the stalk is the support of the stalk valuation: the valuation v_x on the stalk at x vanishes exactly on the maximal ideal.

noncomputable def TauCeti.ValuationSpectrum.presentationLimitStalkResidueValuation {A : Type v} [CommRing A] [TopologicalSpace A] [IsTopologicalRing A] {P : Huber.PairOfDefinition A} {Aplus : Subring A} (hAplus : ∀ ⦃a : A⦄, a ∈ Aplus → Huber.IsPowerBounded a) (hP : P.ringOfDefinition ≤ Aplus) (x : ↑(spa Aplus)) : ValuationSpectrum (IsLocalRing.ResidueField ↑((presentationLimitPresheafInCommRingCat P Aplus).stalk x))

The stalk valuation on the residue field: the point of the valuation spectrum of the residue field of the stalk at x through which presentationLimitStalkValuation factors. It exists because the stalk valuation vanishes on the maximal ideal.

Equations

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

theorem TauCeti.ValuationSpectrum.comap_residue_presentationLimitStalkResidueValuation {A : Type v} [CommRing A] [TopologicalSpace A] [IsTopologicalRing A] {P : Huber.PairOfDefinition A} {Aplus : Subring A} (hAplus : ∀ ⦃a : A⦄, a ∈ Aplus → Huber.IsPowerBounded a) (hP : P.ringOfDefinition ≤ Aplus) (x : ↑(spa Aplus)) : comap (IsLocalRing.residue ↑((presentationLimitPresheafInCommRingCat P Aplus).stalk x)) (presentationLimitStalkResidueValuation hAplus hP x) = presentationLimitStalkValuation hAplus hP x

The stalk valuation factors through the residue field: pulled back along the residue map, presentationLimitStalkResidueValuation is the stalk valuation at x.

theorem TauCeti.ValuationSpectrum.eq_presentationLimitStalkResidueValuation {A : Type v} [CommRing A] [TopologicalSpace A] [IsTopologicalRing A] {P : Huber.PairOfDefinition A} {Aplus : Subring A} (hAplus : ∀ ⦃a : A⦄, a ∈ Aplus → Huber.IsPowerBounded a) (hP : P.ringOfDefinition ≤ Aplus) {x : ↑(spa Aplus)} (w : ValuationSpectrum (IsLocalRing.ResidueField ↑((presentationLimitPresheafInCommRingCat P Aplus).stalk x))) (hw : comap (IsLocalRing.residue ↑((presentationLimitPresheafInCommRingCat P Aplus).stalk x)) w = presentationLimitStalkValuation hAplus hP x) : w = presentationLimitStalkResidueValuation hAplus hP x

Uniqueness of the residue-field valuation: a point of the valuation spectrum of the residue field of the stalk at x which pulls back to the stalk valuation is presentationLimitStalkResidueValuation.