Evaluating integral coefficient series in non-archimedean normed rings

Every integer has norm at most one in a non-archimedean normed ring with ‖1‖ = 1. Thus a series with arbitrary integer coefficients converges at any parameter of norm below one, provided the ring is complete. This includes complete valued fields with nondiscrete valuations or positive characteristic.

In a commutative target ring, evalIntSeries evaluates these series as a ring homomorphism. Evaluation has norm at most one, and multiplication by an evaluated formal unit preserves norms, even when the ring norm is only submultiplicative.

theorem TauCeti.summable_norm_intCast_mul_pow {K : Type u_1} [NormedRing K] [NormOneClass K] [IsUltrametricDist K] (a : ℕ → ℤ) {q : K} (hq : ‖q‖ < 1) : Summable fun (n : ℕ) => ‖↑(a n) * q ^ n‖

The terms of an integer-coefficient power series are absolutely summable at a parameter of norm below one in a non-archimedean normed ring.

theorem TauCeti.summable_intCast_mul_pow {K : Type u_1} [NormedRing K] [NormOneClass K] [CompleteSpace K] [IsUltrametricDist K] (a : ℕ → ℤ) {q : K} (hq : ‖q‖ < 1) : Summable fun (n : ℕ) => ↑(a n) * q ^ n

An arbitrary integer-coefficient power series converges at a parameter of norm below one in a complete non-archimedean normed ring.

noncomputable def TauCeti.evalIntSeries {K : Type u_1} [NormedCommRing K] [NormOneClass K] [CompleteSpace K] [IsUltrametricDist K] (q : K) (hq : ‖q‖ < 1) : PowerSeries ℤ →+* K

Evaluation of an integral formal power series at a parameter of norm below one in a complete non-archimedean normed commutative ring. Integer coefficients are bounded in norm, so the defining sum converges without requiring a linear topology on the target.

Equations

• TauCeti.evalIntSeries q hq = { toFun := fun (f : PowerSeries ℤ) => ∑' (n : ℕ), ↑((PowerSeries.coeff n) f) * q ^ n, map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ }

theorem TauCeti.evalIntSeries_apply {K : Type u_1} [NormedCommRing K] [NormOneClass K] [CompleteSpace K] [IsUltrametricDist K] (q : K) (hq : ‖q‖ < 1) (f : PowerSeries ℤ) : (evalIntSeries q hq) f = ∑' (n : ℕ), ↑((PowerSeries.coeff n) f) * q ^ n

The evaluation map is the convergent sum of the coefficients times powers of the parameter.

@[simp]

theorem TauCeti.evalIntSeries_X {K : Type u_1} [NormedCommRing K] [NormOneClass K] [CompleteSpace K] [IsUltrametricDist K] (q : K) (hq : ‖q‖ < 1) : (evalIntSeries q hq) PowerSeries.X = q

Evaluating the formal parameter gives the chosen element.

theorem TauCeti.norm_evalIntSeries_le_one {K : Type u_1} [NormedCommRing K] [NormOneClass K] [CompleteSpace K] [IsUltrametricDist K] (q : K) (hq : ‖q‖ < 1) (f : PowerSeries ℤ) : ‖(evalIntSeries q hq) f‖ ≤ 1

Evaluation of an integral series inside the open unit ball has norm at most one.

@[simp]

theorem TauCeti.norm_mul_evalIntSeries_of_isUnit {K : Type u_1} [NormedCommRing K] [NormOneClass K] [CompleteSpace K] [IsUltrametricDist K] (x q : K) (hq : ‖q‖ < 1) {f : PowerSeries ℤ} (hf : IsUnit f) : ‖x * (evalIntSeries q hq) f‖ = ‖x‖

Multiplication by an integral formal unit evaluated inside the open unit ball preserves norms in a complete non-archimedean normed commutative ring with ‖1‖ = 1.

@[simp]

theorem TauCeti.norm_evalIntSeries_eq_one_of_isUnit {K : Type u_1} [NormedCommRing K] [NormOneClass K] [CompleteSpace K] [IsUltrametricDist K] (q : K) (hq : ‖q‖ < 1) {f : PowerSeries ℤ} (hf : IsUnit f) : ‖(evalIntSeries q hq) f‖ = 1

An integral formal unit evaluates to an element of norm one inside the open unit ball.