Separating a variable in overconvergent power series #
Separating Y = X none in an overconvergent series in Option σ gives a formal univariate
series whose coefficients are overconvergent in σ. The map washnitzerAlgebra.optionSeries
is injective and agrees with MvPowerSeries.optionEquivLeft on underlying formal series.
It provides the coefficient ring for polynomial remainders in overconvergent Weierstrass
division. Conversely, washnitzerAlgebra.optionC views an overconvergent series in σ as one in
Option σ that is constant in Y; along it, washnitzerAlgebra.polynomialToOption evaluates
polynomials over the coefficient ring at Y. No claim is made that an arbitrary series of
overconvergent coefficients is itself overconvergent: the coefficients must satisfy a common
radius bound. The split polyradius MvPowerSeries.splitRadius r ρ, with radius r in Y and
ρ elsewhere, is the unequal-radius setting in which overconvergent preparation and division
are carried out. By MvPowerSeries.isRestricted_of_map_subtype_eq_optionEquivLeft, separating Y
in a series restricted at r gives a series in Y restricted at r over the series restricted
at ρ ≤ r.
The Gauss norm of a series in Option σ is the unit-radius Gauss norm of its separated series over
the Tate algebra, so optionC preserves Gauss norms.
References #
- E. Grosse-Klönne, Rigid analytic spaces with overconvergent structure sheaf, J. reine angew. Math. 519 (2000), §1.3.
Every coefficient slice of an overconvergent series is overconvergent.
An overconvergent series in σ, viewed as a series in Option σ constant in the separated
variable Y = X none, is overconvergent.
Forgetting overconvergence coefficientwise is injective on formal power series.
Separate Y = X none, retaining overconvergent coefficients in the other variables.
Instances For
The separated coefficients are the formal coefficient slices.
Forgetting overconvergence of the coefficients recovers the formal variable separation.
Variable separation is injective.
The separated variable becomes the univariate variable.
A remaining variable becomes a constant coefficient.
An overconvergent series in σ as an overconvergent series in Option σ, constant in the
separated variable Y = X none.
Instances For
The series underlying optionC f is f, constant in the separated variable.
Separating Y from optionC f gives the constant univariate series f.
optionC sends the variable Xᵢ to the variable X (some i).
On polynomials, optionC is renaming the variables along some.
optionC is injective.
Evaluation of polynomials over R⟨X⟩† at the separated variable Y = X none, as a ring map
R⟨X⟩†[Y] → R⟨X, Y⟩†.
Instances For
Constant polynomials evaluate to series constant in Y.
The variable of the polynomial ring evaluates to Y = X none.
Separating Y from the evaluation of a polynomial at Y recovers the polynomial.
Evaluation at Y is injective: a polynomial is recovered by separating Y again.
Mapping the separated coefficients into the unit-radius Tate algebra agrees with the restricted-series iteration.
In the unit-radius Tate algebra, the evaluation of p at Y is p with coefficients mapped
along toTate.
The Gauss norm of a series in R⟨X, Y⟩† is the Gauss norm at unit radius of its separated
series in Y, with coefficients in the Tate algebra in the variables X.
Adjoining the variable Y preserves Gauss norms.