The completed restricted power-series algebra A⟨X₁,…,Xₖ⟩

For a nonarchimedean commutative ring A, the separated completion of the ring of restricted power series in k variables — the weighted ring TauCeti.Huber.weightedRestrictedSubring at the trivial weight family Tᵢ = {1} (Wedhorn Adic Spaces, arXiv:1910.05934v1, Example 5.54). A is not assumed complete or Hausdorff; for k = 0 the construction is the separated completion of A itself.

Being a completion, A⟨X₁,…,Xₖ⟩ is a complete Hausdorff topological A-algebra with all of that structure found by instance search. It is also again nonarchimedean, since the completion of a nonarchimedean group is one, so it is itself a legal coefficient ring for the construction: the iterated algebra A⟨X₁,…,Xₖ⟩⟨Y₁,…,Y_m⟩ is well-formed, and A⟨X₁,…,Xₖ⟩ is a legal target of the universal property in TauCeti.RingTheory.Huber.WeightedEval.Completion, whose targets must be complete, Hausdorff and nonarchimedean. That instance is Mathlib's, and is available here only because this module imports it.

This module fixes the notation and records what instance search does not supply: continuity of the structure map, joint continuity of the A-scalar action — so that A⟨X₁,…,Xₖ⟩ is a topological A-algebra and results about topological A-modules apply to it — and, at k = 0, where the construction degenerates to the separated completion of A, the identification of A⟨⟩ with Â together with its topological API.

The predicate that every A⟨X₁,…,Xₖ⟩ is noetherian is TauCeti.Huber.IsStronglyNoetherian, in TauCeti.RingTheory.Huber.StronglyNoetherian; the comparison with the plain restricted-series ring, whenever that ring is itself complete and Hausdorff — over a complete Hausdorff base, and over a discrete one — is TauCeti.Huber.restrictedMvPowerSeriesCompletionEquiv, in TauCeti.RingTheory.Huber.WeightedRestrictedSeries.Complete.

Main definitions

• TauCeti.Huber.restrictedMvPowerSeriesCompletion: the completed restricted power-series algebra A⟨X₁,…,Xₖ⟩.
• TauCeti.Huber.weightedMapCompletion: the map A⟨X⟩_T → B⟨X⟩_S on completions induced by a continuous ring map carrying each weight into the corresponding one — the completion-level companion of TauCeti.Huber.weightedMap.
• TauCeti.Huber.weightedMapCompletionEquiv: the RingEquiv A⟨X⟩_T ≃+* B⟨X⟩_S on completions induced by a bicontinuous ring isomorphism carrying the weights into one another in both directions.
• TauCeti.Huber.restrictedMvPowerSeriesCompletionFinZeroEquiv: at k = 0, the identification of A⟨⟩ with the separated completion Â, carried across the completions from the ring-level TauCeti.Huber.weightedRestrictedSubringFinZeroEquiv.

Main results

• TauCeti.Huber.continuous_algebraMap_completion_weightedRestrictedSubring: the structure map A → A⟨X⟩_T into the completion is continuous, for an arbitrary weight family; TauCeti.Huber.continuous_algebraMap_restrictedMvPowerSeriesCompletion is the trivial-weight case, the structure map A → A⟨X₁,…,Xₖ⟩.
• TauCeti.Huber.continuousSMul_completion_weightedRestrictedSubring: scalar multiplication on the completion is jointly continuous, so it is a topological A-algebra.
• TauCeti.Huber.weightedMapCompletion_coe and TauCeti.Huber.continuous_weightedMapCompletion: the induced map on the image of A⟨X⟩_T, and its continuity.
• TauCeti.Huber.weightedMapCompletion_id and TauCeti.Huber.weightedMapCompletion_comp: the functor laws.
• TauCeti.Huber.weightedMapCompletionEquiv_apply and …_symm_apply: each direction of the equivalence is the corresponding TauCeti.Huber.weightedMapCompletion.
• TauCeti.Huber.continuous_weightedMapCompletionEquiv and its _symm: the equivalence is one of topological rings.
• TauCeti.Huber.restrictedMvPowerSeriesCompletionFinZeroEquiv_coe, …_symm_coe, continuous_restrictedMvPowerSeriesCompletionFinZeroEquiv and its _symm: the zero-variable identification on canonical images, and its continuity in both directions.

Provenance

AINTLIB (github.com/CBirkbeck/AINTLIB, Apache-2.0) at commit 2baa76f742bdb4fb8ee323fabba41203bd390e08 formalises restricted power series in projects/AdicSpaces/Adic spaces/RestrictedPowerSeries.lean. It was consulted and not ported: everything there is stated for the uncompleted restricted-series subring, which matches Wedhorn only for complete Hausdorff rings, whereas the roadmap — and this file — define A⟨X₁,…,Xₖ⟩ through the separated completion, so that the object is the intended one for an arbitrary Tate ring. The two descriptions are identified, where they agree, by TauCeti.Huber.restrictedMvPowerSeriesCompletionEquiv. Nothing was copied.

References

• T. Wedhorn, Adic Spaces, Remark and Definition 5.48, and Example 5.54 for the case Tᵢ = {1}.

@[reducible, inline]

noncomputable abbrev TauCeti.Huber.restrictedMvPowerSeriesCompletion (k : ℕ) (A : Type u_1) [CommRing A] [TopologicalSpace A] [NonarchimedeanRing A] : Type u_1

The completed restricted power-series algebra A⟨X₁,…,Xₖ⟩ of a nonarchimedean commutative ring A: the separated completion of the ring of restricted power series in k variables — the weighted ring TauCeti.Huber.weightedRestrictedSubring at the trivial weight family Tᵢ = {1} — with respect to the uniformity of its ring topology. For k = 0 this is the separated completion of A itself.

Equations

• TauCeti.Huber.restrictedMvPowerSeriesCompletion k A = UniformSpace.Completion ↥(TauCeti.Huber.weightedRestrictedSubring (fun (x : Fin k) => {1}) ⋯)

theorem TauCeti.Huber.continuous_algebraMap_completion_weightedRestrictedSubring (k : ℕ) (A : Type u_1) [CommRing A] [TopologicalSpace A] [NonarchimedeanRing A] {T : Fin k → Set A} (hT : IsWeightFamily T) : Continuous ⇑(algebraMap A (UniformSpace.Completion ↥(weightedRestrictedSubring T hT)))

The structure map A → A⟨X⟩_T into the completion of a weighted restricted power-series ring is continuous. Nothing in the argument uses the shape of the weights, so it is stated for an arbitrary weight family; continuous_algebraMap_restrictedMvPowerSeriesCompletion is the trivial one.

@[simp]

theorem TauCeti.Huber.algebraMap_completion_weightedRestrictedSubring_apply (k : ℕ) (A : Type u_1) [CommRing A] [TopologicalSpace A] [NonarchimedeanRing A] {T : Fin k → Set A} (hT : IsWeightFamily T) (a : A) : (algebraMap A (UniformSpace.Completion ↥(weightedRestrictedSubring T hT))) a = ↑((weightedC T hT) a)

The structure map into the completion is the constant series, read in the completion.

This is what lets a statement about the generators — phrased with weightedC — meet one about the A-algebra structure, phrased with algebraMap.

instance TauCeti.Huber.continuousSMul_completion_weightedRestrictedSubring (k : ℕ) (A : Type u_1) [CommRing A] [TopologicalSpace A] [NonarchimedeanRing A] {T : Fin k → Set A} {hT : IsWeightFamily T} : ContinuousSMul A (UniformSpace.Completion ↥(weightedRestrictedSubring T hT))

Scalar multiplication on the completion of a weighted restricted power-series ring is jointly continuous: A⟨X⟩_T is a topological A-algebra. Results about topological modules over A therefore apply to it.

theorem TauCeti.Huber.continuous_algebraMap_restrictedMvPowerSeriesCompletion (k : ℕ) (A : Type u_1) [CommRing A] [TopologicalSpace A] [NonarchimedeanRing A] : Continuous ⇑(algebraMap A (restrictedMvPowerSeriesCompletion k A))

The structure map A → A⟨X₁,…,Xₖ⟩ is continuous.

Functoriality in the coefficient ring

noncomputable def TauCeti.Huber.weightedMapCompletion {k : ℕ} {A : Type u_1} [CommRing A] [TopologicalSpace A] [NonarchimedeanRing A] {B : Type u_2} [CommRing B] [TopologicalSpace B] [NonarchimedeanRing B] {φ : A →+* B} {T : Fin k → Set A} {S : Fin k → Set B} (hφ : Continuous ⇑φ) (hT : IsWeightFamily T) (hS : IsWeightFamily S) (hTS : ∀ (i : Fin k), ⇑φ '' T i ⊆ S i) : UniformSpace.Completion ↥(weightedRestrictedSubring T hT) →+* UniformSpace.Completion ↥(weightedRestrictedSubring S hS)

The completed weighted series ring is functorial in the coefficient ring. A continuous ring map φ : A → B carrying each weight T i into S i induces A⟨X⟩_T → B⟨X⟩_S by TauCeti.Huber.weightedMap; that map is continuous, so it extends to the completions.

This is the completion-level companion of TauCeti.Huber.weightedMap. The subring-level map is not enough on its own: TauCeti.Huber.restrictedMvPowerSeriesCompletion — the object IsStronglyNoetherian is stated over, and the one the roadmap writes A⟨X₁,…,Xₖ⟩ — is a completion, so any statement natural in A has to live here.

Equations

• TauCeti.Huber.weightedMapCompletion hφ hT hS hTS = UniformSpace.Completion.mapRingHom (TauCeti.Huber.weightedMap hφ hT hS hTS) ⋯

@[simp]

theorem TauCeti.Huber.weightedMapCompletion_coe {k : ℕ} {A : Type u_1} [CommRing A] [TopologicalSpace A] [NonarchimedeanRing A] {B : Type u_2} [CommRing B] [TopologicalSpace B] [NonarchimedeanRing B] {φ : A →+* B} {T : Fin k → Set A} {S : Fin k → Set B} (hφ : Continuous ⇑φ) (hT : IsWeightFamily T) (hS : IsWeightFamily S) (hTS : ∀ (i : Fin k), ⇑φ '' T i ⊆ S i) (f : ↥(weightedRestrictedSubring T hT)) : (weightedMapCompletion hφ hT hS hTS) ↑f = ↑((weightedMap hφ hT hS hTS) f)

The value of TauCeti.Huber.weightedMapCompletion on the canonical image of a weighted restricted series: it agrees with TauCeti.Huber.weightedMap.

theorem TauCeti.Huber.continuous_weightedMapCompletion {k : ℕ} {A : Type u_1} [CommRing A] [TopologicalSpace A] [NonarchimedeanRing A] {B : Type u_2} [CommRing B] [TopologicalSpace B] [NonarchimedeanRing B] {φ : A →+* B} {T : Fin k → Set A} {S : Fin k → Set B} (hφ : Continuous ⇑φ) (hT : IsWeightFamily T) (hS : IsWeightFamily S) (hTS : ∀ (i : Fin k), ⇑φ '' T i ⊆ S i) : Continuous ⇑(weightedMapCompletion hφ hT hS hTS)

TauCeti.Huber.weightedMapCompletion is continuous, so it is a morphism of topological rings.

@[simp]

theorem TauCeti.Huber.weightedMapCompletion_id {k : ℕ} {A : Type u_1} [CommRing A] [TopologicalSpace A] [NonarchimedeanRing A] {T : Fin k → Set A} (hT : IsWeightFamily T) : weightedMapCompletion ⋯ hT hT ⋯ = RingHom.id (UniformSpace.Completion ↥(weightedRestrictedSubring T hT))

The identity law: the map induced by RingHom.id is the identity.

@[simp]

theorem TauCeti.Huber.weightedMapCompletion_comp {k : ℕ} {A : Type u_1} [CommRing A] [TopologicalSpace A] [NonarchimedeanRing A] {B : Type u_2} [CommRing B] [TopologicalSpace B] [NonarchimedeanRing B] {φ : A →+* B} {T : Fin k → Set A} {S : Fin k → Set B} {C : Type u_3} [CommRing C] [TopologicalSpace C] [NonarchimedeanRing C] {ψ : B →+* C} {R : Fin k → Set C} (hφ : Continuous ⇑φ) (hψ : Continuous ⇑ψ) (hT : IsWeightFamily T) (hS : IsWeightFamily S) (hR : IsWeightFamily R) (hTS : ∀ (i : Fin k), T i ⊆ ⇑φ ⁻¹' S i) (hSR : ∀ (i : Fin k), S i ⊆ ⇑ψ ⁻¹' R i) : (weightedMapCompletion hψ hS hR ⋯).comp (weightedMapCompletion hφ hT hS ⋯) = weightedMapCompletion ⋯ hT hR ⋯

The composition law: composing the maps induced by φ and ψ gives the map induced by ψ ∘ φ. Stated in the collapsing direction, matching UniformSpace.Completion.mapRingHom_comp, so that a composite normalizes to a single induced map. With TauCeti.Huber.weightedMapCompletion_id this is what makes A⟨X⟩_T functorial in the pair (A, T) at the level of completions — the §0.4 weighted restricted-series functoriality.

This is not Remark 8.29's naturality, which varies the module with the coefficient ring fixed.

A caller holding a weight hypothesis in the form φ '' T i ⊆ S i converts it with Set.image_subset_iff.

noncomputable def TauCeti.Huber.weightedMapCompletionEquiv {k : ℕ} {A : Type u_1} [CommRing A] [TopologicalSpace A] [NonarchimedeanRing A] {B : Type u_2} [CommRing B] [TopologicalSpace B] [NonarchimedeanRing B] {T : Fin k → Set A} {S : Fin k → Set B} (e : A ≃+* B) (he : Continuous ⇑e) (he' : Continuous ⇑e.symm) (hT : IsWeightFamily T) (hS : IsWeightFamily S) (hTS : ∀ (i : Fin k), ⇑↑e '' T i ⊆ S i) (hST : ∀ (i : Fin k), ⇑↑e.symm '' S i ⊆ T i) : UniformSpace.Completion ↥(weightedRestrictedSubring T hT) ≃+* UniformSpace.Completion ↥(weightedRestrictedSubring S hS)

The isomorphism A⟨X⟩_T ≃+* B⟨X⟩_S induced by a bicontinuous ring isomorphism. On the canonical image of A⟨X⟩_T it acts coefficientwise, by TauCeti.Huber.weightedMapCompletion_coe; on a general element of the completion it is the induced map and nothing more.

Continuity of e and of e.symm are separate hypotheses: a RingEquiv is not assumed to be a homeomorphism, so continuity of e.symm does not follow from continuity of e. Both are then consumed, because TauCeti.Huber.weightedMapCompletion goes through UniformSpace.Completion.mapRingHom, which induces nothing from a discontinuous map.

This is the RingEquiv packaging of TauCeti.Huber.weightedMapCompletion: the two induced maps are mutually inverse by TauCeti.Huber.weightedMapCompletion_comp and TauCeti.Huber.weightedMapCompletion_id.

Equations

• TauCeti.Huber.weightedMapCompletionEquiv e he he' hT hS hTS hST = RingEquiv.ofRingHom (TauCeti.Huber.weightedMapCompletion he hT hS hTS) (TauCeti.Huber.weightedMapCompletion he' hS hT hST) ⋯ ⋯

@[simp]

theorem TauCeti.Huber.weightedMapCompletionEquiv_apply {k : ℕ} {A : Type u_1} [CommRing A] [TopologicalSpace A] [NonarchimedeanRing A] {B : Type u_2} [CommRing B] [TopologicalSpace B] [NonarchimedeanRing B] {T : Fin k → Set A} {S : Fin k → Set B} (e : A ≃+* B) (he : Continuous ⇑e) (he' : Continuous ⇑e.symm) (hT : IsWeightFamily T) (hS : IsWeightFamily S) (hTS : ∀ (i : Fin k), ⇑↑e '' T i ⊆ S i) (hST : ∀ (i : Fin k), ⇑↑e.symm '' S i ⊆ T i) (x : UniformSpace.Completion ↥(weightedRestrictedSubring T hT)) : (weightedMapCompletionEquiv e he he' hT hS hTS hST) x = (weightedMapCompletion he hT hS hTS) x

The forward direction of TauCeti.Huber.weightedMapCompletionEquiv is the induced map TauCeti.Huber.weightedMapCompletion; combined with TauCeti.Huber.weightedMapCompletion_coe this describes its action on canonical images of A⟨X⟩_T.

@[simp]

theorem TauCeti.Huber.weightedMapCompletionEquiv_symm_apply {k : ℕ} {A : Type u_1} [CommRing A] [TopologicalSpace A] [NonarchimedeanRing A] {B : Type u_2} [CommRing B] [TopologicalSpace B] [NonarchimedeanRing B] {T : Fin k → Set A} {S : Fin k → Set B} (e : A ≃+* B) (he : Continuous ⇑e) (he' : Continuous ⇑e.symm) (hT : IsWeightFamily T) (hS : IsWeightFamily S) (hTS : ∀ (i : Fin k), ⇑↑e '' T i ⊆ S i) (hST : ∀ (i : Fin k), ⇑↑e.symm '' S i ⊆ T i) (y : UniformSpace.Completion ↥(weightedRestrictedSubring S hS)) : (weightedMapCompletionEquiv e he he' hT hS hTS hST).symm y = (weightedMapCompletion he' hS hT hST) y

The inverse direction of TauCeti.Huber.weightedMapCompletionEquiv is the map induced by e.symm.

theorem TauCeti.Huber.continuous_weightedMapCompletionEquiv {k : ℕ} {A : Type u_1} [CommRing A] [TopologicalSpace A] [NonarchimedeanRing A] {B : Type u_2} [CommRing B] [TopologicalSpace B] [NonarchimedeanRing B] {T : Fin k → Set A} {S : Fin k → Set B} (e : A ≃+* B) (he : Continuous ⇑e) (he' : Continuous ⇑e.symm) (hT : IsWeightFamily T) (hS : IsWeightFamily S) (hTS : ∀ (i : Fin k), ⇑↑e '' T i ⊆ S i) (hST : ∀ (i : Fin k), ⇑↑e.symm '' S i ⊆ T i) : Continuous ⇑(weightedMapCompletionEquiv e he he' hT hS hTS hST)

TauCeti.Huber.weightedMapCompletionEquiv is continuous.

theorem TauCeti.Huber.continuous_weightedMapCompletionEquiv_symm {k : ℕ} {A : Type u_1} [CommRing A] [TopologicalSpace A] [NonarchimedeanRing A] {B : Type u_2} [CommRing B] [TopologicalSpace B] [NonarchimedeanRing B] {T : Fin k → Set A} {S : Fin k → Set B} (e : A ≃+* B) (he : Continuous ⇑e) (he' : Continuous ⇑e.symm) (hT : IsWeightFamily T) (hS : IsWeightFamily S) (hTS : ∀ (i : Fin k), ⇑↑e '' T i ⊆ S i) (hST : ∀ (i : Fin k), ⇑↑e.symm '' S i ⊆ T i) : Continuous ⇑(weightedMapCompletionEquiv e he he' hT hS hTS hST).symm

The inverse of TauCeti.Huber.weightedMapCompletionEquiv is continuous.

Zero variables

noncomputable def TauCeti.Huber.restrictedMvPowerSeriesCompletionFinZeroEquiv {A : Type u_1} [CommRing A] [TopologicalSpace A] [NonarchimedeanRing A] : restrictedMvPowerSeriesCompletion 0 A ≃+* UniformSpace.Completion A

A⟨⟩ is the separated completion of A, as topological rings: the ring isomorphism between the two completions induced by the zero-variable comparison weightedRestrictedSubringFinZeroEquiv, which is a homeomorphism, through UniformSpace.Completion.mapRingEquiv.

Equations

• TauCeti.Huber.restrictedMvPowerSeriesCompletionFinZeroEquiv = UniformSpace.Completion.mapRingEquiv (TauCeti.Huber.weightedRestrictedSubringFinZeroEquiv fun (x : Fin 0) => {1}) ⋯ ⋯

@[simp]

theorem TauCeti.Huber.restrictedMvPowerSeriesCompletionFinZeroEquiv_coe {A : Type u_1} [CommRing A] [TopologicalSpace A] [NonarchimedeanRing A] (f : ↥(weightedRestrictedSubring (fun (x : Fin 0) => {1}) ⋯)) : restrictedMvPowerSeriesCompletionFinZeroEquiv ↑f = ↑((weightedRestrictedSubringFinZeroEquiv fun (x : Fin 0) => {1}) f)

On the canonical image of a restricted series, the comparison of completions is the comparison of the rings underneath.

@[simp]

theorem TauCeti.Huber.restrictedMvPowerSeriesCompletionFinZeroEquiv_symm_coe {A : Type u_1} [CommRing A] [TopologicalSpace A] [NonarchimedeanRing A] (a : A) : restrictedMvPowerSeriesCompletionFinZeroEquiv.symm ↑a = ↑((weightedRestrictedSubringFinZeroEquiv fun (x : Fin 0) => {1}).symm a)

On the canonical image of an element of A, the inverse comparison is the canonical image of the inverse ring comparison.

theorem TauCeti.Huber.continuous_restrictedMvPowerSeriesCompletionFinZeroEquiv {A : Type u_1} [CommRing A] [TopologicalSpace A] [NonarchimedeanRing A] : Continuous ⇑restrictedMvPowerSeriesCompletionFinZeroEquiv

The comparison of completions is continuous.

theorem TauCeti.Huber.continuous_restrictedMvPowerSeriesCompletionFinZeroEquiv_symm {A : Type u_1} [CommRing A] [TopologicalSpace A] [NonarchimedeanRing A] : Continuous ⇑restrictedMvPowerSeriesCompletionFinZeroEquiv.symm

Its inverse is continuous.