Weierstrass division for restricted power series #
Let f be a power series which is distinguished of degree s at the radius c: its
Gauss norm is attained in degree s, and every later coefficient is strictly smaller. A
Weierstrass division by f writes a power series as
q * f + r, q restricted, r vanishing in every degree ≥ s
— that is, with r a polynomial of degree less than s. This file first proves the two facts
about such a decomposition which need no completeness: the norm identity
‖q * f + r‖ = max (‖q‖ * ‖f‖) ‖r‖
for the Gauss norm at c, and, as a consequence, that q and r are determined by the series
they sum to.
It then proves existence for restricted f whose coefficient in degree s is a unit, over a
complete ultrametric normed commutative ring whose norm is multiplicative. Over a field the unit
condition is automatic. Over a ring it is what makes the polynomial part f⁻ = f.trunc (s + 1) a
unit multiple of a monic polynomial, so that a truncation of the dividend can be divided by it as
an ordinary division of polynomials. The division leaves a defect built from the tail f - f⁻,
whose Gauss norm is strictly smaller than that of f. Each step therefore shrinks the dividend by
a fixed factor, and the resulting series of quotients and remainders converges coefficientwise.
The coefficient ring is allowed to be a ring, rather than a field, for the noetherianity of Tate
algebras in several variables: the Tate algebra in n variables is a ring of restricted series in
one variable over the Tate algebra in n - 1 variables, whose Gauss norm is multiplicative, and
Bosch–Güntzer–Remmert divide there by series whose dominant coefficient is a unit.
Since the quotient and the remainder are themselves restricted at c, the division is also
recorded inside the subring PowerSeries.IsRestricted.subring c of R⟦X⟧, which is the form
its ideal-theoretic consequences use.
Main results #
TauCeti.PowerSeries.IsDistinguished.gaussNorm_mul_add_eq_max: the norm identity.TauCeti.PowerSeries.IsDistinguished.eq_and_eq_of_mul_add_eq_mul_add: the quotient and the remainder of a Weierstrass division are unique.TauCeti.PowerSeries.IsDistinguished.exists_mul_add_eqandTauCeti.PowerSeries.IsDistinguished.existsUnique_mul_add_eq: over a complete ultrametric normed commutative ring with multiplicative norm, every restricted power series has a unique Weierstrass division byf, provided the coefficient offin degreesis a unit.TauCeti.PowerSeries.IsDistinguished.exists_mul_add_eq_subringandTauCeti.PowerSeries.IsDistinguished.existsUnique_mul_add_eq_subring: the same division read inside the subringPowerSeries.IsRestricted.subring cof series restricted atc, where quotient and remainder are elements of that subring.
References #
- Bosch, Güntzer, Remmert, Non-Archimedean Analysis, §5.2.1, Theorem 2, whose norm identity, uniqueness assertion and existence assertion these are; the statements there are for the unit radius.
Mathlib's PowerSeries.IsWeierstrassDivisionAt is a different division theorem, for a different
notion of divisor: there the divisor is measured by the order of its image modulo an ideal I of an
I-adically complete coefficient ring, and both dividend and quotient range over all of R⟦X⟧.
Here the divisor is measured by a Gauss norm at a radius, and the quotient is restricted at that
radius; the resulting series q * f + r need not be restricted. Neither statement implies the
other.
The Weierstrass lower bound for the quotient. In a decomposition q * f + r by a
distinguished series f of degree s, with r vanishing in every degree ≥ s, the Gauss norm of
the sum is at least the Gauss norm of q * f.
The Weierstrass lower bound for the remainder. In a decomposition q * f + r by a
distinguished series f of degree s, with r vanishing in every degree ≥ s, the Gauss norm of
the sum is at least the Gauss norm of r.
The Weierstrass division estimate (Bosch–Güntzer–Remmert §5.2.1, Theorem 2). If f is
distinguished of degree s at the radius c, q is restricted, and r vanishes in
every degree ≥ s, then
‖q * f + r‖ = max (‖q‖ * ‖f‖) ‖r‖
for the Gauss norm at c. No cancellation occurs in a Weierstrass decomposition.
Uniqueness in Weierstrass division (Bosch–Güntzer–Remmert §5.2.1, Theorem 2). A restricted
series has at most one decomposition q * f + r with q restricted and r vanishing in every
degree ≥ s, for f distinguished of degree s.
Weierstrass division (Bosch–Güntzer–Remmert §5.2.1, Theorem 2). Over a complete
ultrametric normed commutative ring with multiplicative norm, a restricted series f
distinguished of degree s at a positive radius c, whose coefficient in degree s is a unit,
divides every restricted series g:
g = q * f + r, q restricted, r a polynomial of degree less than s.
Over a field the unit condition is automatic, since a distinguished series has a nonzero
coefficient in its distinguished degree (TauCeti.PowerSeries.IsDistinguished.coeff_ne_zero).
Over a ring it cannot be dropped: a series distinguished of degree 0 whose constant coefficient
is not a unit does not divide 1 with zero remainder. The coefficient ring of interest is the
Tate algebra in fewer variables, over which the Tate algebra in one more variable is a ring of
restricted series. The decomposition is unique by
TauCeti.PowerSeries.IsDistinguished.eq_and_eq_of_mul_add_eq_mul_add.
Weierstrass division (Bosch–Güntzer–Remmert §5.2.1, Theorem 2), in its unique-existence
form: over a complete ultrametric normed commutative ring with multiplicative norm, a restricted
series f distinguished of degree s at a positive radius, whose coefficient in degree s is a
unit, divides every restricted series g in exactly one way, with a restricted quotient and a
remainder that is a polynomial of degree less than s.
Weierstrass division inside the ring of restricted power series. Over a complete
ultrametric normed commutative ring with multiplicative norm, a member f of the ring of series
restricted at a positive radius c which is distinguished of degree s, with a unit coefficient
in degree s, divides every member g with remainder:
g = q * f + r, r a polynomial of degree less than s,
with q and r again restricted at c; the remainder r is in general nonzero. This is
TauCeti.PowerSeries.IsDistinguished.exists_mul_add_eq read in the ring of restricted series,
which is the form ideal-theoretic arguments use. The pair (q, r) is unique, by
TauCeti.PowerSeries.IsDistinguished.existsUnique_mul_add_eq_subring.
Weierstrass division inside the ring of restricted power series is unique. The quotient and
remainder of TauCeti.PowerSeries.IsDistinguished.exists_mul_add_eq_subring are the only ones: a
member g of the ring of series restricted at a positive radius c is written as q * f + r,
with r a polynomial of degree less than the distinguished degree s of f, in exactly one way.
This is TauCeti.PowerSeries.IsDistinguished.existsUnique_mul_add_eq read in that ring.