Iteration of Gauss-normed Tate algebras #

Separating one variable identifies unit-radius restricted series in Option σ with univariate restricted series whose coefficients are unit-radius restricted series in σ. The comparison preserves the Gauss norm, so it identifies the Banach rings when the coefficient ring is complete. It allows Weierstrass division and preparation to be applied with a Tate algebra in the remaining variables as coefficient ring.

The construction restricts Mathlib's MvPowerSeries.optionEquivLeft; restrictedness of the coefficient slices and convergence of their Gauss norms are both required. Merely requiring each slice to be restricted would not characterize multivariate restricted series.

References #

Bosch, Güntzer, Remmert, Non-Archimedean Analysis, §§5.1.1 and 5.2.1.

source

theorem TauCeti.Huber.isRestricted_coeff_optionEquivLeft {σ : Type u_1} {R : Type u_2} [NormedCommRing R] {f : MvPowerSeries (Option σ) R} (hf : MvPowerSeries.IsRestricted (fun (x : Option σ) => 1) f) (n : ℕ) :

MvPowerSeries.IsRestricted (fun (x : σ) => 1) ((PowerSeries.coeff n) ((MvPowerSeries.optionEquivLeft σ R) f))

Each coefficient slice obtained by separating one variable is restricted.

source

noncomputable def TauCeti.Huber.restrictedOptionEquiv {σ : Type u_1} {R : Type u_2} [NormedCommRing R] [IsUltrametricDist R] :

↥(MvPowerSeries.IsRestricted.subring fun (x : Option σ) => 1) ≃+* ↥(PowerSeries.IsRestricted.subring 1)

The unit-radius Tate algebra with one extra variable is the univariate Tate algebra over its remaining-variable Tate algebra. No completeness or finiteness of the variable type is needed.

Equations