The adic spectrum of A⟨T/s⟩ is the rational subset

For a rational subset R(T/s) of Spa (A, A⁺), pullback along the structure map ρ : A → A⟨T/s⟩ is a homeomorphism

Spa (A⟨T/s⟩, A_U⁺) ≃ₜ R(T/s).

Here A_U⁺ is the plus ring completedPlusSubring puts on A⟨T/s⟩: the closure of the image of C, the integral closure of A⁺[T/s] in A(T/s). It agrees with the plus ring Proposition 7.48 puts on a completion, which is what completedPlusSubring_eq_completionPlus records.

Spa.Localization.Homeomorph treats the uncompleted topological localization A(T/s); this file supplies the completed coordinate ring, and with it the first assertion of Proposition 8.2 (2).

No completeness, Tate or Noetherian hypothesis is needed, and A⁺ is an arbitrary subring subject only to the hypothesis A₀ ≤ A⁺ that spaLocalizationHomeomorph already carries.

Main definitions

• TauCeti.ValuationSpectrum.spaCompletedLocalizationHomeomorph: the homeomorphism Spa (A⟨T/s⟩, A_U⁺) ≃ₜ R(T/s).

Main results

• TauCeti.ValuationSpectrum.completedPlusSubring_eq_completionPlus: A_U⁺ is the completion plus ring of C.
• TauCeti.ValuationSpectrum.spaCompletedLocalizationHomeomorph_apply and TauCeti.ValuationSpectrum.coe_spaCompletedLocalizationHomeomorph: the homeomorphism is the canonical map spaLocToRationalSubset, so it is that map which is a homeomorphism.
• TauCeti.ValuationSpectrum.val_comp_spaCompletedLocalizationHomeomorph: composing the homeomorphism with the inclusion of R(T/s) into Spa (A, A⁺) is spaComapLoc.

References

• T. Wedhorn, Adic Spaces (arXiv:1910.05934v1), Proposition 8.2 (2), first assertion, and Proposition 7.48.

theorem TauCeti.ValuationSpectrum.completedPlusSubring_eq_completionPlus {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) : P.completedPlusSubring Aplus T s S hden = completionPlus (integralClosure (↥(Algebra.adjoin (↥Aplus) (Set.range fun (t : ↥T) => Localization.divBy (↑t) s))) S).toSubring

A_U⁺ is the completion plus ring of C. Both are the closure, in A⟨T/s⟩, of the image of the integral closure C of A⁺[T/s] in A(T/s), so the plus ring that completedPlusSubring puts on the completed localization is the one completionPlus builds from C — the plus ring of Wedhorn's Proposition 7.48.

noncomputable def TauCeti.ValuationSpectrum.spaCompletedLocalizationHomeomorph {A : Type u_1} [CommRing A] [TopologicalSpace A] [IsTopologicalRing A] (P : Huber.PairOfDefinition A) (Aplus : Subring A) (hP : P.ringOfDefinition ≤ Aplus) (T : Finset A) (s : A) (S : Type u_2) [CommRing S] [Algebra A S] [IsLocalization.Away s S] (hden : P.HasDenominatorPower T s S) : ↑(spa (P.completedPlusSubring Aplus T s S hden)) ≃ₜ ↑(Subtype.val ⁻¹' rationalSubset Aplus T s)

The adic spectrum of A⟨T/s⟩ is the rational subset R(T/s) — Wedhorn Proposition 8.2 (2), first assertion. Pullback along the structure map A → A⟨T/s⟩ is a homeomorphism onto R(T/s).

Equations

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

@[simp]

theorem TauCeti.ValuationSpectrum.spaCompletedLocalizationHomeomorph_apply {A : Type u_1} [CommRing A] [TopologicalSpace A] [IsTopologicalRing A] (P : Huber.PairOfDefinition A) (Aplus : Subring A) (hP : P.ringOfDefinition ≤ Aplus) (T : Finset A) (s : A) (S : Type u_2) [CommRing S] [Algebra A S] [IsLocalization.Away s S] (hden : P.HasDenominatorPower T s S) (v : ↑(spa (P.completedPlusSubring Aplus T s S hden))) : (spaCompletedLocalizationHomeomorph P Aplus hP T s S hden) v = spaLocToRationalSubset P Aplus T s S hden v

The homeomorphism is the canonical map spaLocToRationalSubset: pullback along the structure map ρ : A → A⟨T/s⟩. This is what makes spaCompletedLocalizationHomeomorph a statement about A⟨T/s⟩ itself rather than about some homeomorphic replacement of it.

@[simp]

theorem TauCeti.ValuationSpectrum.coe_spaCompletedLocalizationHomeomorph {A : Type u_1} [CommRing A] [TopologicalSpace A] [IsTopologicalRing A] (P : Huber.PairOfDefinition A) (Aplus : Subring A) (hP : P.ringOfDefinition ≤ Aplus) (T : Finset A) (s : A) (S : Type u_2) [CommRing S] [Algebra A S] [IsLocalization.Away s S] (hden : P.HasDenominatorPower T s S) : ⇑(spaCompletedLocalizationHomeomorph P Aplus hP T s S hden) = spaLocToRationalSubset P Aplus T s S hden

The homeomorphism, as a function, is pullback along the structure map ρ : A → A⟨T/s⟩. This is the functional companion of the pointwise spaCompletedLocalizationHomeomorph_apply, in the form that rewrites under Set.preimage and Set.image.

theorem TauCeti.ValuationSpectrum.val_comp_spaCompletedLocalizationHomeomorph {A : Type u_1} [CommRing A] [TopologicalSpace A] [IsTopologicalRing A] (P : Huber.PairOfDefinition A) (Aplus : Subring A) (hP : P.ringOfDefinition ≤ Aplus) (T : Finset A) (s : A) (S : Type u_2) [CommRing S] [Algebra A S] [IsLocalization.Away s S] (hden : P.HasDenominatorPower T s S) : Subtype.val ∘ ⇑(spaCompletedLocalizationHomeomorph P Aplus hP T s S hden) = spaComapLoc P Aplus T s S hden

The homeomorphism, followed by the inclusion of R(T/s) into Spa (A, A⁺), is pullback along the structure map ρ : A → A⟨T/s⟩. This is the form that turns a statement about the homeomorphism into one about spaComapLoc, where the plus ring is visible and the map factors through the uncompleted localization.