Power-bounded elements of A⟨X₁, …, Xₖ⟩_T

The variables Xᵢ and the power-bounded constants of a weighted restricted power-series ring are power-bounded in it. Together they exhibit the image of A°[X₁, …, Xₖ] inside A⟨X₁, …, Xₖ⟩°, the plus ring TauCeti.ValuationSpectrum.closedPolydisc designates for the closed polydisc; they exhibit elements of that plus ring rather than determining it.

Neither result needs the trivial weight family. The constant result holds for every weight family; the variable result needs only 1 ∈ T i, which the trivial family satisfies.

Main results

• TauCeti.Huber.isPowerBounded_weightedX: the variable Xᵢ is power-bounded whenever 1 ∈ T i, with TauCeti.Huber.isPowerBounded_weightedX_one_weight the trivial-weight case the closed polydisc uses.
• TauCeti.Huber.isPowerBounded_weightedC: a constant power-bounded in A is power-bounded in A⟨X⟩_T, for every weight family.
• TauCeti.Huber.closure_weightedC_weightedX_le_powerBoundedSubring: the inclusion itself, as a containment of subrings.

References

• T. Wedhorn, Adic Spaces (arXiv:1910.05934v1), Definition 7.56 and Example 7.57.

AINTLIB (github.com/CBirkbeck/AINTLIB, Apache-2.0) at commit 2baa76f742bdb4fb8ee323fabba41203bd390e08, projects/AdicSpaces/Adic spaces/Wedhorn828.lean, has the power-boundedness of Xᵢ under stronger hypotheses: there it follows from membership in a ring of definition, which needs A to be Huber. For that route in this repository, see TauCeti.Huber.IsBounded.isPowerBounded_of_mem.

theorem TauCeti.Huber.isPowerBounded_weightedX {k : ℕ} {A : Type u_1} [CommRing A] [TopologicalSpace A] [NonarchimedeanRing A] {T : Fin k → Set A} (hT : IsWeightFamily T) {i : Fin k} (hi : 1 ∈ T i) : IsPowerBounded (weightedX T hT i)

The variable Xᵢ is power-bounded whenever 1 ∈ T i.

Its use is to put the coordinates of the closed polydisc inside the plus ring A⟨T⟩° that TauCeti.ValuationSpectrum.closedPolydisc designates; there the weights are trivial, which is TauCeti.Huber.isPowerBounded_weightedX_one_weight.

@[simp]

theorem TauCeti.Huber.isPowerBounded_weightedX_one_weight {k : ℕ} {A : Type u_1} [CommRing A] [TopologicalSpace A] [NonarchimedeanRing A] (i : Fin k) : IsPowerBounded (weightedX (fun (x : Fin k) => {1}) ⋯ i)

The variable Xᵢ is power-bounded at the trivial weight family, the case TauCeti.ValuationSpectrum.closedPolydisc uses.

@[simp] because it is unconditional: simp closes the goal outright rather than rewriting it.

theorem TauCeti.Huber.isPowerBounded_weightedC {k : ℕ} {A : Type u_1} [CommRing A] [TopologicalSpace A] [NonarchimedeanRing A] {T : Fin k → Set A} (hT : IsWeightFamily T) {a : A} (ha : IsPowerBounded a) : IsPowerBounded ((weightedC T hT) a)

A power-bounded constant stays power-bounded, at any weight family — no hypothesis on T beyond TauCeti.Huber.IsWeightFamily. Contrast TauCeti.Huber.isPowerBounded_weightedX, which needs 1 ∈ T i.

With the variable case it places A°[X₁, …, Xₖ] inside A⟨X₁, …, Xₖ⟩°.

theorem TauCeti.Huber.closure_weightedC_weightedX_le_powerBoundedSubring {k : ℕ} {A : Type u_1} [CommRing A] [TopologicalSpace A] [NonarchimedeanRing A] {T : Fin k → Set A} (hT : IsWeightFamily T) (hi : ∀ (i : Fin k), 1 ∈ T i) : Subring.closure (⇑(weightedC T hT) '' ↑(powerBoundedSubring A) ∪ Set.range (weightedX T hT)) ≤ powerBoundedSubring ↥(weightedRestrictedSubring T hT)

A°[X₁, …, Xₖ] lands inside A⟨X₁, …, Xₖ⟩_T°. The subring generated by the power-bounded constants and the variables consists of power-bounded elements.

This is the inclusion the two results above are for, stated as a subring containment so that a consumer discharges membership for a whole polynomial expression at once rather than by induction on its shape.