The presentation-limit pre-adic space

The adic spectrum with its presentation-limit presheaf is a pre-adic space when the plus subring consists of power-bounded elements and contains a ring of definition. This packages the structure presheaf, local stalks, and residue valuations into a pre-adic-space object on the adic spectrum for later morphism and sheafiness constructions. Its stalk valuation at x is presentationLimitStalkValuation (presentationLimitPreAdicSpace_stalkValuation), so the characterisation of that valuation by its rational germs applies to it.

noncomputable def TauCeti.ValuationSpectrum.presentationLimitPreAdicSpace {A : Type u} [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) : PreAdicSpace

The pre-adic space of an adic spectrum with the completed rational-localisation presheaf. The valuation at a point is induced on the residue field of its local stalk.

Equations

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

@[simp]

theorem TauCeti.ValuationSpectrum.presentationLimitPreAdicSpace_carrier {A : Type u} [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) : ↑(presentationLimitPreAdicSpace P Aplus hAplus hP).toPresheafedSpace = ↧↑(spa Aplus)

The space underlying the presentation-limit pre-adic space is its adic spectrum.

@[simp]

theorem TauCeti.ValuationSpectrum.presentationLimitPreAdicSpace_presheaf {A : Type u} [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) : (presentationLimitPreAdicSpace P Aplus hAplus hP).toPresheafedSpace.presheaf ≍ presentationLimitPresheaf P Aplus

The sections of this pre-adic space form the presentation-limit presheaf.

@[simp]

theorem TauCeti.ValuationSpectrum.presentationLimitPreAdicSpace_ringPresheaf {A : Type u} [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) : CategoryTheory.Functor.comp (presentationLimitPreAdicSpace P Aplus hAplus hP).toPresheafedSpace.presheaf (TopCommRingCat.isCompleteSeparated.ι.comp (CategoryTheory.forget₂ TopCommRingCat CommRingCat)) ≍ (presentationLimitPresheaf P Aplus).comp (TopCommRingCat.isCompleteSeparated.ι.comp (CategoryTheory.forget₂ TopCommRingCat CommRingCat))

Forgetting the topology gives the presentation-limit presheaf of rings.

@[simp]

theorem TauCeti.ValuationSpectrum.presentationLimitPreAdicSpace_valuation {A : Type u} [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)) : (presentationLimitPreAdicSpace P Aplus hAplus hP).valuation (⋯ ▸ x) ≍ presentationLimitStalkResidueValuation hAplus hP x

The valuation of a presentation-limit pre-adic space is the stalk residue valuation.

theorem TauCeti.ValuationSpectrum.presentationLimitPreAdicSpace_stalkValuation {A : Type u} [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 : ↑(presentationLimitPreAdicSpace P Aplus hAplus hP).toTopCat) : (presentationLimitPreAdicSpace P Aplus hAplus hP).stalkValuation x = presentationLimitStalkValuation hAplus hP x

The stalk valuation of the presentation-limit pre-adic space at x is presentationLimitStalkValuation, the valuation v_x on the stalk glued from the points of the rational coordinate rings determined by x.