The p-adic kit: evaluation of power series #
Evaluation of a power series h ∈ O⟦X⟧ at a point z₀ of the maximal ideal of O
(ChabautyColeman.PSeries.eval), as the convergent sum ∑ aₖ z₀ᵏ
(ChabautyColeman.PSeries.hasSum_eval). This is a thin layer over Mathlib's
PowerSeries.eval₂; the point of this file is the standing hypothesis pack of the
whole p-adic kit:
O is a complete Hausdorff uniform ring that is local with 𝔪-adic topology
([Fact (IsAdic (maximalIdeal O))]). The model case is O = ℤ_p
(PadicInt.instFactIsAdic); rings of integers of finite extensions of ℚ_p also
qualify. From the Fact we derive IsLinearTopology O O and topological nilpotency of
the points of 𝔪 (ChabautyColeman.PSeries.hasEval_of_mem), which is what Mathlib's
evaluation machinery consumes.
The evaluation calculus: evaluation is a ring homomorphism
(ChabautyColeman.PSeries.evalRingHom); it is compatible with the composition
ChabautyColeman.PSeries.comp of power series, defined for inner series with constant
coefficient in 𝔪 by evaluating in O⟦X⟧ with the product topology
(ChabautyColeman.PSeries.eval_comp) — this is more general than Mathlib's algebraic
PowerSeries.subst, which requires a nilpotent constant coefficient. The formal
derivative computes the first-order behaviour of evaluation, with an explicit
second-order remainder (ChabautyColeman.PSeries.eval_deriv).
The setting is complete: ChabautyColeman.PSeries.instIsAdicComplete derives
IsAdicComplete (maximalIdeal O) O from completeness and separatedness of the adic
topology, so Mathlib's Weierstrass preparation
(PowerSeries.exists_isWeierstrassFactorization, uniqueness
PowerSeries.IsWeierstrassFactorization.elim) applies to O⟦X⟧ as-is.
Blueprint nodes: def:eval, lem:eval-hom, thm:wprep.
Evaluation of a power series h ∈ O⟦X⟧ at a point z₀ of the maximal ideal:
the convergent sum ∑ aₖ z₀ᵏ (Mathlib's PowerSeries.eval₂; the value is junk
for z₀ outside the maximal ideal).
Equations
- ChabautyColeman.PSeries.eval z₀ h = PowerSeries.eval₂ (RingHom.id O) z₀ h
Instances For
Composition h ↦ h(k(X)) of power series, for k with constant coefficient in the
maximal ideal (junk otherwise); defined by evaluating h at the point k of O⟦X⟧
with the product topology. In contrast to Mathlib's algebraic PowerSeries.subst,
the constant coefficient of k need not be nilpotent.
Equations
Instances For
In a linearly topologized ring, multiplying a null sequence by an arbitrary sequence gives a null sequence.
Points of the maximal ideal are legitimate evaluation points for power series.
Power series with constant coefficient in the maximal ideal are legitimate
evaluation points in O⟦X⟧.
The adic summability test: a series whose terms lie in growing powers of the maximal ideal is summable.
The standing hypotheses make O a complete local ring in the algebraic sense, so
Mathlib's Weierstrass preparation applies to O⟦X⟧ (blueprint node thm:wprep).
The defining series of PSeries.eval converges.
Evaluation as a ring homomorphism (blueprint node lem:eval-hom) #
Evaluation at a point of the maximal ideal, as a ring homomorphism.
Equations
Instances For
Compatibility with composition #
Evaluation of a composition is the composition of the evaluations.
The constant coefficient of a composition is the value of h at the constant
coefficient of k.
The derivative and difference quotients #
Taylor expansion to second order: the formal derivative gives the first-order behaviour of evaluation, with an explicit second-order remainder.
The value of a power series at a point of the maximal ideal is congruent to its constant coefficient modulo the maximal ideal.