Coordinates on Weierstrass quotients #
For a multiplicatively distinguished restricted series g of degree s, taking the
Weierstrass remainder identifies the quotient by g with polynomials of degree less than s
as a module over the coefficient ring. The classes of 1, X, …, X^(s-1) therefore give a
basis of powers. Its coordinates are the coefficients of the remainder, and multiplication is
computed by taking the remainder of the product of the polynomial representatives. For a monic
polynomial divisor this is ordinary polynomial remainder; the structure constants are the
coefficients of X^(i+j) %ₘ p.
The coefficient ring may be any complete ultrametric normed commutative ring, and the radius any positive real number. No globally multiplicative norm is assumed. This applies in particular to series over the Tate algebra in the remaining variables. Distinguished degree zero gives an empty basis of the zero quotient.
The construction uses Mathlib's Polynomial.degreeLT.basis for the polynomial coordinates.
References #
- Bosch, Güntzer, Remmert, Non-Archimedean Analysis, §§5.2.1–5.2.2.
A restricted series and its Weierstrass remainder represent the same quotient class.
Taking the Weierstrass remainder identifies the quotient by a multiplicatively distinguished series with the coefficient module of polynomials of degree less than its distinguished degree.
Instances For
The inverse remainder equivalence includes the polynomial representative in the quotient.
The representative selected from a series class is its Weierstrass remainder.
The polynomial selected from a quotient class represents that class.
Multiplication in a Weierstrass quotient is multiplication of its polynomial representatives followed by taking the Weierstrass remainder.
The classes of the first s powers of the variable form a basis of the quotient by a
multiplicatively distinguished series of degree s. At degree zero this is the empty basis.
Instances For
The quotient by a multiplicatively distinguished restricted series is finite over the coefficient ring, without requiring a multiplicative coefficient norm.
The quotient by a multiplicatively distinguished restricted series is free over the coefficient ring, without requiring a multiplicative coefficient norm.
The i-th basis vector is the class of X^i.
The quotient by a multiplicatively distinguished series is generated by the class of X,
with its first s powers forming the remainder-coordinate basis.
Instances For
The generator of the quotient power basis is the class of the variable.
The dimension of the quotient power basis is the distinguished degree.
The underlying basis of the quotient power basis is the remainder-coordinate basis.
Basis coordinates are coefficients of the polynomial representative selected by division.
Multiplication coordinates are obtained by reducing the product of the two remainders.
For a monic polynomial divisor the multiplication table of the power basis is given by
reducing X^(i+j) modulo the divisor.