Weierstrass preparation with a uniformiser power over a discrete valuation ring #
Let O be a discrete valuation ring with normalised additive valuation v = addVal O, and let
f = ∑ aₙ Xⁿ be a power series over O. Its μ-invariant is the least valuation of a
coefficient,
μ(f) = min_n v(aₙ),
which is ⊤ exactly for f = 0, and its λ-invariant is the first index attaining it,
λ(f) = min {n | v(aₙ) = μ(f)}.
Dividing out π ^ μ(f) for a uniformiser π leaves a series with a unit coefficient, whose
image in k⟦X⟧ over the residue field k is nonzero of order λ(f). When O is complete for
its maximal ideal, Mathlib's Weierstrass preparation theorem applies to that series, giving the
factorisation
f = C (π ^ μ(f)) * u * P, u a unit of O⟦X⟧, P distinguished of degree λ(f),
which underlies the structure theory of the Iwasawa algebra O⟦T⟧. The exponent, the unit and the
polynomial are unique. No finiteness of the residue field is needed, and O need not be the
valuation ring of a normed field; the valuation ring of a complete discretely valued field is the
special case O = Valuation.integer v.
Both invariants are additive on products of nonzero series: after dividing out the uniformiser
powers, this is additivity of the order on the domain k⟦X⟧.
Main definitions #
PowerSeries.muInvariant:μ(f) = ⨅ n, addVal O (coeff n f), inℕ∞.PowerSeries.lambdaInvariant: the leastnwithaddVal O (coeff n f) = μ(f).
Main results #
PowerSeries.C_dvd_iff_addVal_le_muInvariant:C a ∣ f ↔ v(a) ≤ μ(f); in particularPowerSeries.C_pow_dvd_iff_le_muInvariant:C (π ^ k) ∣ f ↔ k ≤ μ(f)for a uniformiserπ.PowerSeries.order_map_residue_eq_lambdaInvariant: ifμ(f) = 0, the reduction offmodulo the maximal ideal has orderλ(f).PowerSeries.exists_pow_mul_distinguished_mul_unit: Weierstrass preparation with a uniformiser power, with exponentμ(f)and polynomial degreeλ(f).PowerSeries.C_pow_mul_unit_mul_inj: uniqueness of the exponent, the unit and the distinguished polynomial.PowerSeries.muInvariant_mul,PowerSeries.lambdaInvariant_mul: additivity on products.
References #
- L. Washington, Introduction to Cyclotomic Fields, second edition, GTM 83, §7.1,
Theorem 7.3 and the discussion of
μandλfollowing it. - J. Neukirch, A. Schmidt and K. Wingberg, Cohomology of Number Fields, second edition, (5.3.1)–(5.3.4).
The μ-invariant of a power series over a discrete valuation ring: the least normalised
valuation of a coefficient. It is ⊤ exactly for the zero series.
Instances For
The λ-invariant of a power series over a discrete valuation ring: the least index of a
coefficient whose valuation is the μ-invariant. It is 0 for the zero series.
Instances For
The μ-invariant is attained, in degree λ(f).
Every coefficient before degree λ(f) has valuation strictly larger than μ(f).
λ(f) is the index of the first coefficient whose valuation is μ(f).
The μ-invariant vanishes exactly when the reduction modulo the maximal ideal is nonzero.
A unit has μ-invariant zero.
A unit has λ-invariant zero.
If μ(f) = 0, the reduction of f modulo the maximal ideal has order λ(f).
The constant a divides f exactly when v(a) ≤ μ(f).
For a uniformiser π, the constant π ^ k divides f exactly when k ≤ μ(f).
A nonzero power series is π ^ μ(f) times a series of μ-invariant zero.
A series admitting a Weierstrass factorisation has μ-invariant zero.
The distinguished polynomial of a Weierstrass factorisation has degree λ(g).
Weierstrass preparation with a uniformiser power. Over a discrete valuation ring complete
for its maximal ideal, a nonzero power series f factors as C (π ^ μ(f)) * u * P with u a
unit and P a distinguished polynomial of degree λ(f).
Uniqueness in Weierstrass preparation with a uniformiser power. For a fixed uniformiser
π, the exponent, the unit and the distinguished polynomial of a factorisation
C (π ^ m) * u * P are determined by the product.
The μ-invariant is additive on products.
The λ-invariant is additive on products of nonzero series.