Weierstrass preparation for restricted power series #
The power series restricted at a radius c form a subring PowerSeries.IsRestricted.subring c
of R⟦X⟧; over a complete nonarchimedean field and at a positive radius it is the Tate algebra of
the closed disc of radius c. This file describes its units and factors a distinguished series
through a monic polynomial. The coefficients may lie in any complete ultrametric normed
commutative ring with multiplicative norm, such as a Tate algebra in fewer variables; the series
to be factored is then asked to have a unit coefficient in its distinguished degree, which is
automatic over a field.
Over such a ring, a restricted series is a unit of that subring exactly when it is distinguished
of degree 0, that is, when its constant coefficient strictly dominates every positive-degree
weighted coefficient and attains the Gauss norm, and its constant coefficient is a unit. Over a
field the second condition follows from the first. Weierstrass preparation then says that a
restricted series f distinguished of degree s, with a unit coefficient in degree s, factors as
f = e * ω, e a unit of the ring of restricted series, ω monic of degree s,
and that the pair (e, ω) is unique; the polynomial ω is again distinguished of degree s.
Both statements are consequences of Weierstrass division.
Since e is a unit, f and ω generate the same ideal, so the factorization presents the
quotient of the ring of restricted series by f as the quotient of R[X] by a monic polynomial of
degree s. This is the route to noetherianity of the Tate algebra.
Main results #
TauCeti.PowerSeries.isDistinguished_zero_of_isUnit,TauCeti.PowerSeries.isUnit_iff_isDistinguished_zero_and_isUnit_coeff_zeroand, over a field,TauCeti.PowerSeries.isUnit_iff_isDistinguished_zero: the units of the ring of restricted series.TauCeti.PowerSeries.IsDistinguished.of_isUnit_mul: multiplying by such a unit leaves the distinguished degree unchanged.TauCeti.PowerSeries.IsDistinguished.exists_isUnit_isMonicOfDegree_mul_eq,TauCeti.PowerSeries.IsDistinguished.eq_and_eq_of_mul_eq_mulandTauCeti.PowerSeries.IsDistinguished.existsUnique_isUnit_isMonicOfDegree_mul_eq: Weierstrass preparation, in its existence, uniqueness and unique-existence forms.
References #
- Bosch, Güntzer, Remmert, Non-Archimedean Analysis, §5.2.2, Theorem 1, whose statement this is;
the statement there is for the unit radius. The factor
ωis constructed as there; that the quotient is a unit is deduced here from a second Weierstrass division.
Mathlib's PowerSeries.exists_isWeierstrassFactorization is a different factorization theorem, for
the divisors of Mathlib.RingTheory.PowerSeries.WeierstrassPreparation: there the series lives over
an I-adically complete coefficient ring, the distinguished polynomial is one whose lower
coefficients lie in I, and the unit is a unit of the whole of A⟦X⟧. Here the coefficient ring
is complete for a multiplicative ultrametric norm, the polynomial is monic with its lower
coefficients bounded by the Gauss norm, and the unit is a unit of the subring of restricted series.
Neither statement implies the other.
A unit of the ring of restricted power series at a positive radius is distinguished of
degree 0: its constant coefficient strictly dominates every positive-degree weighted coefficient
and attains the Gauss norm.
Multiplying by a unit of the ring of restricted power series leaves the distinguished degree unchanged.
The units of the ring of restricted power series. Over a complete ultrametric normed
commutative ring with multiplicative norm, a restricted power series is a unit of the ring of
series restricted at a positive radius c exactly when it is distinguished of degree 0 at c
and its constant coefficient is a unit.
Weierstrass preparation (Bosch–Güntzer–Remmert §5.2.2, Theorem 1). 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,
is a unit of the ring of restricted series times a monic polynomial of degree s:
f = e * ω, e a unit, ω monic of degree s.
Over a field the unit condition is automatic, by
TauCeti.PowerSeries.IsDistinguished.coeff_ne_zero. The polynomial ω is then itself
distinguished of degree s, by TauCeti.PowerSeries.IsDistinguished.of_isUnit_mul, so no bound
on its lower coefficients needs stating separately. The factorization is unique by
TauCeti.PowerSeries.IsDistinguished.eq_and_eq_of_mul_eq_mul.
Uniqueness in Weierstrass preparation (Bosch–Güntzer–Remmert §5.2.2, Theorem 1). A
restricted series distinguished of degree s at a positive radius has at most one factorization
as a unit of the ring of restricted series times a monic polynomial of degree s.
Weierstrass preparation (Bosch–Güntzer–Remmert §5.2.2, Theorem 1), in its unique-existence
form: over a complete ultrametric normed commutative ring with multiplicative norm, a restricted
series distinguished of degree s at a positive radius, whose coefficient in degree s is a unit,
is in exactly one way a unit of the ring of restricted series times a monic polynomial of degree
s.
The units of the ring of restricted power series over a field. Over a complete
nonarchimedean field, a restricted power series is a unit of the ring of series restricted at a
positive radius c exactly when it is distinguished of degree 0 at c.