The structure map into a family of rational localisations

For a finite set T of numerators, the rational localisations A⟨T/t⟩ for t ∈ T carry a single structure map out of A apiece. This file bundles them into one ring homomorphism A →+* ∀ t : T, A⟨T/t⟩ and records that it is continuous. No hypothesis relating the members of T is needed for either, so none is imposed: what is defined here is the product map for an arbitrary finite T.

The family (R(T/t))_{t ∈ T} is a cover of Spa(A,A⁺) — a standard rational cover — when T generates the unit ideal, by TauCeti.ValuationSpectrum.spa_eq_biUnion_rationalSubset_of_span_eq_top, which needs nothing of A. For a complete Hausdorff Huber pair the converse holds as well (TauCeti.ValuationSpectrum.span_eq_top_iff_spa_eq_biUnion_rationalSubset, Corollary 7.53). Under the spanning hypothesis this map is the comparison whose faithful flatness and injectivity Wedhorn's Corollary 8.32 asserts. Neither the hypothesis nor those conclusions appear below; this is the map they are about.

Implementation notes

The localisations are given as a family S : T → Type*, one type per numerator, because that is how the rest of this development takes a localisation — as a parameter satisfying IsLocalization.Away, not as a construction. Their uniform structures are likewise supplied, which is why the three letI families appear before the codomain: UniformSpace.Completion (S t) is not a ring until locUniformSpace, isUniformAddGroup_locUniformSpace and isTopologicalRing_locUniformSpace are in scope for that t, and the product type mentions them all.

Main results

• TauCeti.Huber.PairOfDefinition.rationalLocalizationPiHom, with TauCeti.Huber.PairOfDefinition.rationalLocalizationPiHom_apply its computation rule and TauCeti.Huber.PairOfDefinition.continuous_rationalLocalizationPiHom its continuity.

References

• T. Wedhorn, Adic Spaces (arXiv:1910.05934v1), Corollary 7.53 for the cover and Corollary 8.32 for what this map is for.

noncomputable def TauCeti.Huber.PairOfDefinition.rationalLocalizationPiHom {A : Type u_1} [CommRing A] [TopologicalSpace A] [IsTopologicalRing A] (P : PairOfDefinition A) (T : Finset A) (S : ↥T → Type u_2) [(t : ↥T) → CommRing (S t)] [(t : ↥T) → Algebra A (S t)] [∀ (t : ↥T), IsLocalization.Away (↑t) (S t)] (hden : ∀ (t : ↥T), P.HasDenominatorPower T (↑t) (S t)) : A →+* (t : ↥T) → UniformSpace.Completion (S t)

The structure map into a family of rational localisations: the tuple of the structure maps A → A⟨T/t⟩, one for each numerator t ∈ T. The family is a standard rational cover when Ideal.span (T : Set A) = ⊤, which nothing here requires.

Equations

• P.rationalLocalizationPiHom T S hden = RingHom.pi fun (t : ↥T) => P.toCompletionLoc T (↑t) (S t) ⋯

@[simp]

theorem TauCeti.Huber.PairOfDefinition.rationalLocalizationPiHom_apply {A : Type u_1} [CommRing A] [TopologicalSpace A] [IsTopologicalRing A] (P : PairOfDefinition A) (T : Finset A) (S : ↥T → Type u_2) [(t : ↥T) → CommRing (S t)] [(t : ↥T) → Algebra A (S t)] [∀ (t : ↥T), IsLocalization.Away (↑t) (S t)] (hden : ∀ (t : ↥T), P.HasDenominatorPower T (↑t) (S t)) (a : A) (t : ↥T) : (P.rationalLocalizationPiHom T S hden) a t = (P.toCompletionLoc T (↑t) (S t) ⋯) a

Each component of TauCeti.Huber.PairOfDefinition.rationalLocalizationPiHom is the structure map into that rational localisation. The body is not exported, so this is how a consumer computes with it.

theorem TauCeti.Huber.PairOfDefinition.continuous_rationalLocalizationPiHom {A : Type u_1} [CommRing A] [TopologicalSpace A] [IsTopologicalRing A] (P : PairOfDefinition A) (T : Finset A) (S : ↥T → Type u_2) [(t : ↥T) → CommRing (S t)] [(t : ↥T) → Algebra A (S t)] [∀ (t : ↥T), IsLocalization.Away (↑t) (S t)] (hden : ∀ (t : ↥T), P.HasDenominatorPower T (↑t) (S t)) : Continuous ⇑(P.rationalLocalizationPiHom T S hden)

The structure map into a family of rational localisations is continuous, the product topology on the codomain being the one each factor carries.