The comparison map of a containment of rational subsets is a map of Huber pairs

For a containment R(T'/s') ⊆ R(T/s) of rational subsets of Spa (A, A⁺), TauCeti.ValuationSpectrum.ringHomOfRationalSubsetSubset is the unique continuous ring homomorphism σ : A⟨T/s⟩ → A⟨T'/s'⟩ compatible with the structure maps from A. This file makes it a map of Huber pairs: σ carries A_U⁺ into A_U'⁺, so it induces a map of adic spectra

Spa (A⟨T'/s'⟩, A_U'⁺) → Spa (A⟨T/s⟩, A_U⁺)

in the other direction, and under the identifications of Wedhorn's Proposition 8.2(2) that map is the inclusion R(T'/s') ⊆ R(T/s).

Downstream, this is the stability of the plus structure under restriction to a smaller rational subset. The plus rings A_U⁺ are built one rational subset at a time, and the results here relate two of them along a containment: σ carries A_U⁺ into A_U'⁺. That is the form taken by the condition "power-bounded, with all values ≤ 1" on sections of the structure presheaf, whose restriction maps along R(T'/s') ⊆ R(T/s) land in the plus ring of the smaller subset, so that the sub-presheaf 𝒪_X⁺ they cut out is a presheaf of rings; and it is the upgrade of σ from a map of rings to a map of Huber pairs that makes comap σ a map of adic spectra.

Main definitions

All names below are in the TauCeti.ValuationSpectrum namespace.

• pairHomOfRationalSubsetSubset : the comparison map as a morphism of Huber pairs (A⟨T/s⟩, A_U⁺) → (A⟨T'/s'⟩, A_U'⁺). The map of adic spectra is TauCeti.Huber.Pair.Hom.spaComap of this morphism; that generic construction and its API are used directly, with no specialised wrapper.

Main results

• comap_mem_spa_completedPlusSubring : a continuous valuation pulled back along a continuous map out of A⟨T/s⟩ is a point of Spa (A⟨T/s⟩, A_U⁺) once it is sub-unit on the image of A⁺ and its pullback to A lies in R(T/s).
• comap_ringHomOfRationalSubsetSubset_mem_spa : pullback along the comparison map takes points of Spa (A⟨T'/s'⟩, A_U'⁺) to points of Spa (A⟨T/s⟩, A_U⁺).
• ringHomOfRationalSubsetSubset_mem_completedPlusSubring : the comparison map carries A_U⁺ into A_U'⁺, so it is a map of Huber pairs.
• pairHomOfRationalSubsetSubset_toRingHom : the underlying ring homomorphism of the morphism of Huber pairs is the comparison map.
• pairHomOfRationalSubsetSubset_self, pairHomOfRationalSubsetSubset_comp : the morphisms of Huber pairs are functorial in the containment — the morphism of a rational subset with itself is the identity, and the morphism of a composite containment is the composite of the two morphisms.
• spaCompletedLocalizationHomeomorph_spaComap_pairHomOfRationalSubsetSubset : across the homeomorphisms Spa (A⟨T/s⟩, A_U⁺) ≃ₜ R(T/s), the induced map of adic spectra is the inclusion R(T'/s') ⊆ R(T/s).

References

• T. Wedhorn, Adic Spaces (arXiv:1910.05934v1), Propositions 8.2 and 7.52.

theorem TauCeti.ValuationSpectrum.comap_mem_spa_completedPlusSubring {A : Type u_1} [CommRing A] [TopologicalSpace A] [IsTopologicalRing A] (P : Huber.PairOfDefinition A) (Aplus : Subring A) (T : Finset A) (s : A) (S : Type u_2) [CommRing S] [Algebra A S] [IsLocalization.Away s S] (hden : P.HasDenominatorPower T s S) {B : Type u_3} [CommRing B] [TopologicalSpace B] (σ : UniformSpace.Completion S →+* B) : Continuous ⇑σ → ∀ {w : ValuationSpectrum B}, w.IsContinuous → (∀ a ∈ Aplus, σ ((P.toCompletionLoc T s S hden) a) ≤ᵥ 1) → comap (σ.comp (P.toCompletionLoc T s S hden)) w ∈ rationalSubset Aplus T s → comap σ w ∈ spa (P.completedPlusSubring Aplus T s S hden)

A criterion for a pullback to lie in Spa (A⟨T/s⟩, A_U⁺). Let σ : A⟨T/s⟩ → B be a continuous ring homomorphism and w a continuous valuation on B that is sub-unit on the image of A⁺ under σ ∘ ρ, where ρ : A → A⟨T/s⟩ is the structure map, and whose pullback to A lies in R(T/s). Then the pullback of w along σ is a point of Spa (A⟨T/s⟩, A_U⁺). The sub-unit condition on A_U⁺ itself is not asked: it follows from the two conditions on A⁺ and on the fractions t/s, the latter being sub-unit because the pullback lies in R(T/s).

theorem TauCeti.ValuationSpectrum.comap_ringHomOfRationalSubsetSubset_mem_spa {A : Type u_1} [CommRing A] [TopologicalSpace A] [IsTopologicalRing A] (P : Huber.PairOfDefinition A) (Aplus : Subring A) (hAplus : ∀ ⦃a : A⦄, a ∈ Aplus → Huber.IsPowerBounded a) (T : Finset A) (s : A) (S : Type u_2) [CommRing S] [Algebra A S] [IsLocalization.Away s S] (hden : P.HasDenominatorPower T s S) (T' : Finset A) (s' : A) (S' : Type u_3) [CommRing S'] [Algebra A S'] [IsLocalization.Away s' S'] (hden' : P.HasDenominatorPower T' s' S') (hsub : rationalSubset Aplus T' s' ⊆ rationalSubset Aplus T s) (w : ValuationSpectrum (UniformSpace.Completion S')) : w ∈ spa (P.completedPlusSubring Aplus T' s' S' hden') → comap (ringHomOfRationalSubsetSubset P Aplus hAplus T s S hden T' s' S' hden' hsub) w ∈ spa (P.completedPlusSubring Aplus T s S hden)

Pullback along the comparison map lands in the adic spectrum of A⟨T/s⟩. For a containment R(T'/s') ⊆ R(T/s) of rational subsets, every point of Spa (A⟨T'/s'⟩, A_U'⁺) pulls back along the comparison map σ : A⟨T/s⟩ → A⟨T'/s'⟩ to a point of Spa (A⟨T/s⟩, A_U⁺).

theorem TauCeti.ValuationSpectrum.ringHomOfRationalSubsetSubset_mem_completedPlusSubring {A : Type u_1} [CommRing A] [TopologicalSpace A] [IsTopologicalRing A] (P : Huber.PairOfDefinition A) (Aplus : Subring A) (hIplus : ∀ j ∈ P.idealOfDefinition, ↑j ∈ Aplus) (hAplus : ∀ ⦃a : A⦄, a ∈ Aplus → Huber.IsPowerBounded a) (T : Finset A) (s : A) (S : Type u_2) [CommRing S] [Algebra A S] [IsLocalization.Away s S] (hden : P.HasDenominatorPower T s S) (T' : Finset A) (s' : A) (S' : Type u_3) [CommRing S'] [Algebra A S'] [IsLocalization.Away s' S'] (hden' : P.HasDenominatorPower T' s' S') (hsub : rationalSubset Aplus T' s' ⊆ rationalSubset Aplus T s) (f : UniformSpace.Completion S) : f ∈ P.completedPlusSubring Aplus T s S hden → (ringHomOfRationalSubsetSubset P Aplus hAplus T s S hden T' s' S' hden' hsub) f ∈ P.completedPlusSubring Aplus T' s' S' hden'

The comparison map is a map of Huber pairs (Wedhorn's Proposition 8.2(1)): for a containment R(T'/s') ⊆ R(T/s) of rational subsets, the comparison map σ : A⟨T/s⟩ → A⟨T'/s'⟩ carries A_U⁺ into A_U'⁺. Together with continuous_ringHomOfRationalSubsetSubset this makes σ a morphism of complete Huber pairs (A⟨T/s⟩, A_U⁺) → (A⟨T'/s'⟩, A_U'⁺).

noncomputable def TauCeti.ValuationSpectrum.pairHomOfRationalSubsetSubset {A : Type u_1} [CommRing A] [TopologicalSpace A] [IsTopologicalRing A] (P : Huber.PairOfDefinition A) (Aplus : Subring A) (hIplus : ∀ j ∈ P.idealOfDefinition, ↑j ∈ Aplus) (hAplus : ∀ ⦃a : A⦄, a ∈ Aplus → Huber.IsPowerBounded a) (T : Finset A) (s : A) (S : Type u_2) [CommRing S] [Algebra A S] [IsLocalization.Away s S] (hden : P.HasDenominatorPower T s S) (T' : Finset A) (s' : A) (S' : Type u_3) [CommRing S'] [Algebra A S'] [IsLocalization.Away s' S'] (hden' : P.HasDenominatorPower T' s' S') (hsub : rationalSubset Aplus T' s' ⊆ rationalSubset Aplus T s) : { plus := P.completedPlusSubring Aplus T s S hden, isRingOfIntegralElements := ⋯ }.Hom { plus := P.completedPlusSubring Aplus T' s' S' hden', isRingOfIntegralElements := ⋯ }

The comparison map as a morphism of Huber pairs (Wedhorn's Proposition 8.2(1)): the comparison map σ : A⟨T/s⟩ → A⟨T'/s'⟩ of a containment R(T'/s') ⊆ R(T/s), bundled with its continuity and with ringHomOfRationalSubsetSubset_mem_completedPlusSubring as a morphism (A⟨T/s⟩, A_U⁺) → (A⟨T'/s'⟩, A_U'⁺) of Huber pairs.

The two Huber pairs are the plus rings completedPlusSubring together with TauCeti.Huber.PairOfDefinition.isRingOfIntegralElements_completedPlusSubring; that is what hIplus pays for, since it is the hypothesis making A_U⁺ open. pairHomOfRationalSubsetSubset_toRingHom recovers σ, and TauCeti.Huber.Pair.Hom.spaComap of this morphism is the induced map Spa (A⟨T'/s'⟩, A_U'⁺) → Spa (A⟨T/s⟩, A_U⁺), with the generic spaComap API — its value, continuity and functoriality lemmas — applying to it unchanged.

Equations

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

@[simp]

theorem TauCeti.ValuationSpectrum.pairHomOfRationalSubsetSubset_toRingHom {A : Type u_1} [CommRing A] [TopologicalSpace A] [IsTopologicalRing A] (P : Huber.PairOfDefinition A) (Aplus : Subring A) (hIplus : ∀ j ∈ P.idealOfDefinition, ↑j ∈ Aplus) (hAplus : ∀ ⦃a : A⦄, a ∈ Aplus → Huber.IsPowerBounded a) (T : Finset A) (s : A) (S : Type u_2) [CommRing S] [Algebra A S] [IsLocalization.Away s S] (hden : P.HasDenominatorPower T s S) (T' : Finset A) (s' : A) (S' : Type u_3) [CommRing S'] [Algebra A S'] [IsLocalization.Away s' S'] (hden' : P.HasDenominatorPower T' s' S') (hsub : rationalSubset Aplus T' s' ⊆ rationalSubset Aplus T s) : (pairHomOfRationalSubsetSubset P Aplus hIplus hAplus T s S hden T' s' S' hden' hsub).toRingHom = ringHomOfRationalSubsetSubset P Aplus hAplus T s S hden T' s' S' hden' hsub

The underlying ring homomorphism of pairHomOfRationalSubsetSubset is the comparison map.

@[simp]

theorem TauCeti.ValuationSpectrum.pairHomOfRationalSubsetSubset_self {A : Type u_1} [CommRing A] [TopologicalSpace A] [IsTopologicalRing A] (P : Huber.PairOfDefinition A) (Aplus : Subring A) (hIplus : ∀ j ∈ P.idealOfDefinition, ↑j ∈ Aplus) (hAplus : ∀ ⦃a : A⦄, a ∈ Aplus → Huber.IsPowerBounded a) (T : Finset A) (s : A) (S : Type u_2) [CommRing S] [Algebra A S] [IsLocalization.Away s S] (hden : P.HasDenominatorPower T s S) : pairHomOfRationalSubsetSubset P Aplus hIplus hAplus T s S hden T s S hden ⋯ = Huber.Pair.Hom.id { plus := P.completedPlusSubring Aplus T s S hden, isRingOfIntegralElements := ⋯ }

The morphism of a rational subset with itself is the identity (Wedhorn's Proposition 8.2(1)): for the containment R(T/s) ⊆ R(T/s), the morphism of Huber pairs pairHomOfRationalSubsetSubset is TauCeti.Huber.Pair.Hom.id.

@[simp]

theorem TauCeti.ValuationSpectrum.pairHomOfRationalSubsetSubset_comp {A : Type u_1} [CommRing A] [TopologicalSpace A] [IsTopologicalRing A] (P : Huber.PairOfDefinition A) (Aplus : Subring A) (hIplus : ∀ j ∈ P.idealOfDefinition, ↑j ∈ Aplus) (hAplus : ∀ ⦃a : A⦄, a ∈ Aplus → Huber.IsPowerBounded a) (T : Finset A) (s : A) (S : Type u_2) [CommRing S] [Algebra A S] [IsLocalization.Away s S] (hden : P.HasDenominatorPower T s S) (T' : Finset A) (s' : A) (S' : Type u_3) [CommRing S'] [Algebra A S'] [IsLocalization.Away s' S'] (hden' : P.HasDenominatorPower T' s' S') (T'' : Finset A) (s'' : A) (S'' : Type u_4) [CommRing S''] [Algebra A S''] [IsLocalization.Away s'' S''] (hden'' : P.HasDenominatorPower T'' s'' S'') (hsub : rationalSubset Aplus T' s' ⊆ rationalSubset Aplus T s) (hsub' : rationalSubset Aplus T'' s'' ⊆ rationalSubset Aplus T' s') : (pairHomOfRationalSubsetSubset P Aplus hIplus hAplus T' s' S' hden' T'' s'' S'' hden'' hsub').comp (pairHomOfRationalSubsetSubset P Aplus hIplus hAplus T s S hden T' s' S' hden' hsub) = pairHomOfRationalSubsetSubset P Aplus hIplus hAplus T s S hden T'' s'' S'' hden'' ⋯

The composite morphism is the morphism of the composite containment (Wedhorn's Proposition 8.2(1)): for containments R(T''/s'') ⊆ R(T'/s') ⊆ R(T/s) of rational subsets, TauCeti.Huber.Pair.Hom.comp of the morphisms of the two containments is pairHomOfRationalSubsetSubset of the composite containment. Together with pairHomOfRationalSubsetSubset_self this makes the comparison morphisms a functorial system of restriction maps on rational subsets.

The composite is the left-hand side, matching Set.inclusion_comp_inclusion: that orientation collapses a composite to a single morphism, and it is the only one simp can use, since the intermediate presentation S' is visible on this side but occurs on the other only inside the containment proof hsub'.trans hsub.

theorem TauCeti.ValuationSpectrum.spaCompletedLocalizationHomeomorph_spaComap_pairHomOfRationalSubsetSubset {A : Type u_1} [CommRing A] [TopologicalSpace A] [IsTopologicalRing A] (P : Huber.PairOfDefinition A) (Aplus : Subring A) (hP : P.ringOfDefinition ≤ Aplus) (hAplus : ∀ ⦃a : A⦄, a ∈ Aplus → Huber.IsPowerBounded a) (T : Finset A) (s : A) (S : Type u_2) [CommRing S] [Algebra A S] [IsLocalization.Away s S] (hden : P.HasDenominatorPower T s S) (T' : Finset A) (s' : A) (S' : Type u_3) [CommRing S'] [Algebra A S'] [IsLocalization.Away s' S'] (hden' : P.HasDenominatorPower T' s' S') (hsub : rationalSubset Aplus T' s' ⊆ rationalSubset Aplus T s) (w : ↑(spa (P.completedPlusSubring Aplus T' s' S' hden'))) : (spaCompletedLocalizationHomeomorph P Aplus hP T s S hden) ((pairHomOfRationalSubsetSubset P Aplus ⋯ hAplus T s S hden T' s' S' hden' hsub).spaComap w) = Set.inclusion ⋯ ((spaCompletedLocalizationHomeomorph P Aplus hP T' s' S' hden') w)

The induced map of adic spectra is the inclusion of rational subsets. Across the homeomorphisms Spa (A⟨T/s⟩, A_U⁺) ≃ₜ R(T/s) of Wedhorn's Proposition 8.2(2), the map TauCeti.Huber.Pair.Hom.spaComap of pairHomOfRationalSubsetSubset is the inclusion R(T'/s') ⊆ R(T/s).