The Monsky–Washnitzer algebra of overconvergent power series #
Let R be an ultrametric normed commutative ring. A formal power series f = ∑ aᵥ Xᵛ in the
variables σ is overconvergent if it is restricted at some constant radius ρ > 1, that is,
‖aᵥ‖ ρ^|ν| → 0. The overconvergent series form the R-subalgebra
W = R⟨X⟩† = ⋃_{ρ > 1} R{X/ρ} ⊆ R[[X]],
the algebra of Monsky and Washnitzer. Over a complete field K it is the basic object of
Grosse-Klönne's dagger geometry, playing the role that the Tate algebra K⟨X⟩ plays in rigid
geometry: the overconvergent series are those converging on some polydisc strictly larger than
the closed unit polydisc. Every overconvergent series is restricted at radius 1, so W lies in
the Tate algebra T = R{X/1} and carries the restricted Gauss norm.
Main definitions #
TauCeti.Dagger.washnitzerAlgebra σ R: the subalgebra of series restricted at some constant radiusρ > 1.TauCeti.Dagger.washnitzerAlgebra.X: the variables, andTauCeti.Dagger.washnitzerAlgebra.ofMvPolynomial: the inclusion of the polynomials, withTauCeti.Dagger.washnitzerAlgebra.ofPolynomialfor one variable.TauCeti.Dagger.washnitzerAlgebra.toTate: the inclusion ofWinto the unit-radius Tate algebra.TauCeti.Dagger.washnitzerAlgebra.ofRestricted: the inclusion intoWof the series restricted at a polyradius bounded below by someρ > 1.TauCeti.Dagger.washnitzerAlgebra.renameEquiv: renaming the variables along an equivalence.TauCeti.Dagger.washnitzerAlgebra.isEmptyAlgEquiv: with no variables,Wis the coefficient ring, via the constant coefficient.
Main results #
TauCeti.Dagger.mem_washnitzerAlgebra_iff_norm_coeff_le: for finitely many variables,f ∈ Wiff‖aᵥ‖ ≤ C ρ^{-|ν|}for someρ > 1andC.TauCeti.Dagger.mem_washnitzerAlgebra_iff_exists_pow_eq_norm: over a nontrivially normed field the radii may be taken in the divisible hull√|K^×|of the value group.TauCeti.Dagger.washnitzerAlgebra.denseRange_toTate:Wis dense in the Tate algebra;TauCeti.Dagger.washnitzerAlgebra_toSubring_lt: over a nontrivially normed field it is a proper subring as soon as there is a variable, whileWis everything when there is none (TauCeti.Dagger.washnitzerAlgebra_eq_top), and then every series is a constant (TauCeti.Dagger.washnitzerAlgebra.algebraMap_surjective).TauCeti.Dagger.eventually_isRestricted_of_mem_washnitzerAlgebra: an overconvergent series is restricted at every radiusρ > 1close enough to1, so finitely many overconvergent series share such a radius.TauCeti.Dagger.exists_isRestricted_forall_norm_coeff_mul_pow_lt: strict coefficient bounds on an overconvergent series persist to some radiusρ > 1; byTauCeti.Dagger.exists_isRestricted_forall_mem_norm_coeff_mul_pow_ltthis holds for the coefficients at any set of exponents, and byTauCeti.Dagger.eventually_isRestricted_forall_norm_coeff_mul_pow_ltat every radius close enough to1.TauCeti.Dagger.isUnit_washnitzerAlgebra_iffandTauCeti.Dagger.washnitzerAlgebra.isUnit_toTate_iff: over a complete ultrametric field an overconvergent series is a unit ofWiff it is a unit of the Tate algebra, iff its constant coefficient is nonzero and strictly dominates all others, sotoTateis a local homomorphism (TauCeti.Dagger.washnitzerAlgebra.isLocalHom_toTate). In Gauss norm form,TauCeti.Dagger.isUnit_washnitzerAlgebra_iff_norm_sub_ltreads|f - f(0)| < |f(0)|. Consequently1 + c • fis a unit for all scalarscnear0(TauCeti.Dagger.washnitzerAlgebra.eventually_isUnit_one_add_smul).TauCeti.Dagger.primitive_mem_washnitzerAlgebraandTauCeti.Dagger.washnitzerAlgebra.primitive: over a field of characteristic zero, termwise primitives∑ aᵥ Xᵛ ↦ ∑ aᵥ Xᵛ⁺ᵉⁱ / (νᵢ + 1)of overconvergent series are overconvergent.
References #
- E. Grosse-Klönne, Rigid analytic spaces with overconvergent structure sheaf, J. reine angew. Math. 519 (2000), §1.2.
- P. Monsky and G. Washnitzer, Formal cohomology. I, Ann. of Math. 88 (1968).
The Monsky–Washnitzer algebra R⟨X⟩† of overconvergent power series: the series
restricted at some constant radius ρ > 1.
Instances For
A series is overconvergent iff it is restricted at some constant radius ρ > 1.
An overconvergent series is restricted at every constant radius in [0, 1]; in particular
it lies in the unit-radius Tate algebra.
Constant series are overconvergent.
An overconvergent series is restricted at every constant radius ρ > 1 close enough to 1.
This allows one radius to be chosen for finitely many overconvergent series at once.
Polynomials are overconvergent.
Overconvergence by coefficient bounds. For finitely many variables, a series is
overconvergent iff its coefficients satisfy ‖aᵥ‖ ≤ C ρ^{-|ν|} for some ρ > 1 and C.
With no variables every power series is a constant, so every series is overconvergent.
The Monsky–Washnitzer algebra lies in the unit-radius Tate algebra.
With no variables, every overconvergent series comes from the coefficient ring.
Renaming variables along an equivalence preserves overconvergence.
Instances For
The renaming equivalence acts on the underlying formal power series by renaming.
The variable Xᵢ as an element of the Monsky–Washnitzer algebra.
Instances For
The variable Xᵢ ∈ W is the formal variable Xᵢ.
A variable in the Monsky–Washnitzer algebra over a nontrivial ring is nonzero.
A variable in the Monsky–Washnitzer algebra over a nontrivial ring is not a unit.
The inclusion of the polynomial algebra into the Monsky–Washnitzer algebra.
Instances For
A polynomial viewed in W is the polynomial viewed as a power series.
The inclusion of one-variable polynomials into the Monsky–Washnitzer algebra.
Instances For
A one-variable polynomial in the Monsky–Washnitzer algebra has its usual power series.
The one-variable polynomial inclusion sends Polynomial.X to the variable of W.
Distinct one-variable polynomials are distinct overconvergent series.
The polynomial inclusion sends the polynomial variables to the variables of W.
Distinct polynomials are distinct overconvergent series.
The inclusion of the Monsky–Washnitzer algebra into the unit-radius Tate algebra R{X/1},
through which W carries the Gauss norm.
Instances For
The inclusion into the Tate algebra does not change the underlying series.
The inclusion into the Tate algebra is injective.
The inclusion into the Tate algebra sends the variable Xᵢ to the variable Xᵢ.
The Monsky–Washnitzer algebra is dense in the Tate algebra for the Gauss norm.
For a polyradius c bounded below by some ρ > 1, the inclusion of the series restricted at
c into the Monsky–Washnitzer algebra.
Instances For
The inclusion of a restricted subring does not change the underlying series.
Renaming the variables of overconvergent series. Renaming along an equivalence
e : σ ≃ τ is an R-algebra isomorphism R⟨X_σ⟩† ≃ R⟨X_τ⟩†.
Instances For
The renaming isomorphism of overconvergent series is MvPowerSeries.renameEquiv on the
underlying series.
Renaming the variables commutes with the inclusion of the polynomials.
Overconvergent series in no variables. With no variables every series is a constant, so
the constant coefficient is an R-algebra isomorphism R⟨⟩† ≃ R.
Instances For
The isomorphism R⟨⟩† ≃ R is the constant coefficient.
The inverse of R⟨⟩† ≃ R sends a scalar to the constant series.
Radius selection on a set of exponents. If the coefficients of an overconvergent series at
the exponents in S all have norm strictly less than r, then for some radius ρ > 1 at which
the series is restricted, the weighted coefficient norms ‖aᵥ‖ ρ^|ν| with ν ∈ S are still
strictly less than r.
Radius selection. If every coefficient of an overconvergent series has norm strictly less
than r, then for some radius ρ > 1 at which the series is restricted, every weighted
coefficient norm ‖aᵥ‖ ρ^|ν| is still strictly less than r.
Radius selection near 1. If every coefficient of an overconvergent series has norm
strictly less than r, then at every radius ρ > 1 close enough to 1 the series is restricted
and every weighted coefficient norm ‖aᵥ‖ ρ^|ν| is still strictly less than r. Unlike
exists_isRestricted_forall_norm_coeff_mul_pow_lt, this allows one radius to be chosen for
finitely many series at once.
Radii in the divisible hull of the value group suffice. Over a nontrivially normed field
K, a series is overconvergent iff it is restricted at some radius ρ > 1 with ρ^m = ‖a‖ for
some m ≠ 0 and a ∈ K.
Over a nontrivially normed field, the Monsky–Washnitzer algebra in at least one variable is a proper subring of the Tate algebra.
Units of the Monsky–Washnitzer algebra. Over a complete ultrametric normed field, an
overconvergent series is a unit of W iff its constant coefficient is nonzero and strictly
dominates the norm of every other coefficient.
An overconvergent series is a unit of the Tate algebra iff it is a unit of the Monsky–Washnitzer algebra: the inverse of an overconvergent series is overconvergent.
The inclusion of the Monsky–Washnitzer algebra into the Tate algebra is a local homomorphism.
The unit criterion in Gauss norm form. An overconvergent series f is a unit of W iff
|f - f(0)| < |f(0)| for the Gauss norm of the Tate algebra.
Small perturbations of 1 are units. Over a complete ultrametric normed field, for every
overconvergent series f, 1 + c • f is a unit of the Monsky–Washnitzer algebra for all scalars
c near 0.
Primitives of overconvergent series are overconvergent. Over an ultrametric normed field
of characteristic zero, the termwise primitive with respect to Xᵢ of an overconvergent series is
overconvergent. See MvPowerSeries.IsRestricted.primitive for the radius-by-radius version.
The termwise primitive with respect to Xᵢ, as a K-linear endomorphism of the
Monsky–Washnitzer algebra.
Instances For
The primitive in W is the termwise primitive of the underlying series.