The two models of the one-variable restricted power-series ring

This file identifies the two models of the one-variable Tate algebra used in Tau Ceti. The Huber development uses restricted multivariate power series indexed by Fin 1, while Weierstrass division uses Mathlib's univariate PowerSeries, whose variable type is Unit. Renaming the variable along finOneEquiv identifies their restrictedness conditions and hence gives an equivalence between the two subrings.

Over a complete nonarchimedean normed ring, the Huber completion agrees with the plain restricted series ring. Composing that comparison with the variable-renaming equivalence identifies the completed Huber algebra with Mathlib's univariate restricted-series ring.

The comparison is stated over commutative normed rings because Mathlib packages variable renaming of power series, MvPowerSeries.rename, only over a commutative semiring. The ultrametric hypothesis is needed only for the target ring: Mathlib defines PowerSeries.IsRestricted.subring only under [IsUltrametricDist R].

Main results

• TauCeti.Huber.isRestricted_renameEquiv_finOne_iff: renaming the sole variable from Fin 1 to Unit identifies the Huber restrictedness predicate with Mathlib's radius-one one.
• TauCeti.Huber.restrictedMvPowerSeriesSubringOneEquiv: the two uncompleted one-variable restricted-series models are equivalent as rings.
• TauCeti.Huber.restrictedMvPowerSeriesCompletionOneEquiv: over a complete base, the completed Huber model is equivalent to Mathlib's univariate restricted-series ring.

References

• T. Wedhorn, Adic Spaces, §5.6, for restricted power series and their topology.

theorem TauCeti.Huber.isRestricted_renameEquiv_finOne_iff {R : Type u_1} [NormedCommRing R] {f : MvPowerSeries (Fin 1) R} : IsRestricted f ↔ PowerSeries.IsRestricted 1 ((MvPowerSeries.renameEquiv R finOneEquiv) f)

Renaming the sole variable preserves restrictedness. The Huber predicate asks directly that the coefficients tend to zero, while Mathlib's radius-one predicate asks the same of their norms. The exponent sets are identified by the unique-coordinate equivalence.

noncomputable def TauCeti.Huber.restrictedMvPowerSeriesSubringOneEquiv {R : Type u_1} [NormedCommRing R] [IsUltrametricDist R] [NonarchimedeanRing R] : ↥(restrictedMvPowerSeriesSubring 1 R) ≃+* ↥(PowerSeries.IsRestricted.subring 1)

The two one-variable restricted-series models are the same ring. The Huber model uses Fin 1 as its variable type; Mathlib's PowerSeries uses Unit. The equivalence is variable renaming along finOneEquiv, restricted to the subrings whose coefficients tend to zero.

Equations

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

@[simp]

theorem TauCeti.Huber.coe_restrictedMvPowerSeriesSubringOneEquiv {R : Type u_1} [NormedCommRing R] [IsUltrametricDist R] [NonarchimedeanRing R] (f : ↥(restrictedMvPowerSeriesSubring 1 R)) : ↑(restrictedMvPowerSeriesSubringOneEquiv f) = (MvPowerSeries.renameEquiv R finOneEquiv) ↑f

The one-variable equivalence is variable renaming on underlying power series.

@[simp]

theorem TauCeti.Huber.coe_restrictedMvPowerSeriesSubringOneEquiv_symm {R : Type u_1} [NormedCommRing R] [IsUltrametricDist R] [NonarchimedeanRing R] (f : ↥(PowerSeries.IsRestricted.subring 1)) : ↑(restrictedMvPowerSeriesSubringOneEquiv.symm f) = (MvPowerSeries.renameEquiv R finOneEquiv.symm) ↑f

The inverse one-variable equivalence renames the sole variable back from Unit to Fin 1 on underlying power series.

noncomputable def TauCeti.Huber.restrictedMvPowerSeriesCompletionOneEquiv {R : Type u_1} [NormedCommRing R] [IsUltrametricDist R] [NonarchimedeanRing R] [CompleteSpace R] : restrictedMvPowerSeriesCompletion 1 R ≃+* ↥(PowerSeries.IsRestricted.subring 1)

The completed one-variable Huber algebra is the univariate restricted-series ring. Completeness identifies the completion with the trivial-weight restricted-series subring; the trivial-weight comparison and variable renaming then give the displayed ring equivalence.

Equations

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

@[simp]

theorem TauCeti.Huber.restrictedMvPowerSeriesCompletionOneEquiv_coe {R : Type u_1} [NormedCommRing R] [IsUltrametricDist R] [NonarchimedeanRing R] [CompleteSpace R] (f : ↥(weightedRestrictedSubring (fun (x : Fin 1) => {1}) ⋯)) : restrictedMvPowerSeriesCompletionOneEquiv ↑f = restrictedMvPowerSeriesSubringOneEquiv ((RingEquiv.subringCongr ⋯) f)

The completed comparison sends a restricted series in the canonical dense subring to the same series, with its sole variable renamed from Fin 1 to Unit.

@[simp]

theorem TauCeti.Huber.restrictedMvPowerSeriesCompletionOneEquiv_symm_apply {R : Type u_1} [NormedCommRing R] [IsUltrametricDist R] [NonarchimedeanRing R] [CompleteSpace R] (f : ↥(PowerSeries.IsRestricted.subring 1)) : restrictedMvPowerSeriesCompletionOneEquiv.symm f = ↑((RingEquiv.subringCongr ⋯).symm (restrictedMvPowerSeriesSubringOneEquiv.symm f))

The inverse completed comparison renames the sole variable back from Unit to Fin 1 and then includes the resulting restricted series in the completion.