Weierstrass division in several variables over Banach rings #
Let R be an ultrametric normed commutative ring and let c : Option σ → ℝ be positive
polyradii. Separating the variable X none identifies restricted series in Option σ at c
with univariate series restricted at the radius c none whose coefficients are restricted series
in σ at the polyradii c ∘ some (MvPowerSeries.restrictedOptionEquiv), and this
identification preserves the Gauss norms. Weierstrass division by a series g in the separated
variable is one-variable Weierstrass division over that coefficient ring.
The divisor hypothesis is that the iterated series of g is multiplicatively distinguished of
degree s at the radius c none (TauCeti.PowerSeries.IsMulDistinguished): its Gauss norm is
attained in degree s, every later weighted coefficient norm ‖aₙ‖ * c none ^ n is strictly
smaller (earlier ones may tie), and the coefficient in degree s, a restricted series in the
remaining variables, is a multiplicative unit of the ring of such series. A remainder is a series
of degree less than s in X none: every monomial in which X none occurs with exponent at
least s has coefficient zero. Its coefficients in the
remaining variables are arbitrary restricted series.
Over a complete coefficient ring every restricted series f then has a unique decomposition
f = g * q + r with q restricted and r a remainder, and
‖g * q + r‖ = max (‖g‖ * ‖q‖) ‖r‖
for the Gauss norms at c, so that ‖q‖ ≤ ‖f‖ / ‖g‖ and ‖r‖ ≤ ‖f‖. The norm of R need not
be multiplicative, and R may have nilpotents.
Main results #
TauCeti.MvPowerSeries.norm_mul_add_eq_max_of_isMulDistinguished: the norm identity.TauCeti.MvPowerSeries.eq_and_eq_of_mul_add_eq_mul_add_of_isMulDistinguished: the quotient and the remainder are unique.TauCeti.MvPowerSeries.exists_mul_add_eq_of_isMulDistinguishedandTauCeti.MvPowerSeries.existsUnique_mul_add_eq_of_isMulDistinguished: over a complete ultrametric normed commutative ring, every restricted series has a unique Weierstrass division, with quotient and remainder bounded by the dividend.
References #
- F. Martin, Overconvergent subanalytic subsets in the framework of Berkovich spaces, J. Eur. Math. Soc. 18 (2016), Proposition 1.27 and the remark following Corollary 1.28, for division by a multiplicatively distinguished series over a Banach ring and its several-variable form.
- Bosch, Güntzer, Remmert, Non-Archimedean Analysis, §5.2.1, Theorem 2, for the unit-radius case over a complete nonarchimedean field.
A series whose iterated series is multiplicatively distinguished has positive Gauss norm.
The Weierstrass division estimate in several variables. Over an ultrametric normed
commutative ring, let the iterated series of g in the separated variable X none be
multiplicatively distinguished of degree s. If r has degree less than s in X none, then
‖g * q + r‖ = max (‖g‖ * ‖q‖) ‖r‖
for the Gauss norms at the polyradii c. The norm of the coefficient ring need not be
multiplicative.
Uniqueness in several-variable Weierstrass division. Over an ultrametric normed
commutative ring, let the iterated series of g in the separated variable X none be
multiplicatively distinguished of degree s. A restricted series has at most one decomposition
g * q + r with q restricted and r of degree less than s in X none.
Weierstrass division in several variables over a Banach ring (Martin, Proposition 1.27,
iterated). Over a complete ultrametric normed commutative ring, let the iterated series of a
restricted series g in the separated variable X none be multiplicatively distinguished of
degree s at the radius c none. Then every restricted series f decomposes as
f = g * q + r, q restricted, r of degree less than s in X none,
with ‖q‖ ≤ ‖f‖ / ‖g‖ and ‖r‖ ≤ ‖f‖ for the Gauss norms at c. The norm of the coefficient ring
need not be multiplicative. The decomposition is unique by
TauCeti.MvPowerSeries.eq_and_eq_of_mul_add_eq_mul_add_of_isMulDistinguished.
Weierstrass division in several variables over a Banach ring, in its unique-existence
form: over a complete ultrametric normed commutative ring, if the iterated series of g in the
separated variable X none is multiplicatively distinguished of degree s, every restricted
series f is g * q + r for exactly one pair of restricted series q and r with r of
degree less than s in X none.