Power series with coefficients in a subring: division and expansion

Let R be a subring of a ring S, and let D be a power series over S with coefficients in R whose first nonzero coefficient, in degree m, is 1; that is, D = Xᵐ u with u(0) = 1. If F * D has coefficients in R, then so does F (PowerSeries.coeff_mem_of_coeff_mul_mem): the coefficients of F are solved for recursively from those of F * D.

This is how integrality of q-expansions passes through division by a modular form such as the discriminant Δ = q + ⋯, whose q-expansion has integer coefficients.

A power series lies in the image of PowerSeries.map f exactly when each of its coefficients lies in the range of f (PowerSeries.mem_map_range), so the same division statement applies to images of power series over another ring.

Substituting Xᵖ for X (PowerSeries.expand) only spreads the coefficients out and inserts zeros, so it neither creates nor destroys coefficients in R (PowerSeries.forall_coeff_expand_mem_iff). This is how integrality of a q-expansion is unchanged when it is read in a power of q, for instance at a multiple of the cusp width.

Main results

• PowerSeries.mem_map_range: the range of PowerSeries.map f consists of the power series whose coefficients all lie in the range of f.
• PowerSeries.coeff_mem_of_coeff_mul_mem: if F * D and D = Xᵐ u, u(0) = 1, have coefficients in R, then so does F.
• PowerSeries.forall_coeff_expand_mem_iff: expand p φ has coefficients in R if and only if φ does.

theorem PowerSeries.mem_map_range {S : Type u_1} [Ring S] {T : Type u_2} [Ring T] (f : T →+* S) {p : PowerSeries S} : p ∈ (map f).range ↔ ∀ (n : ℕ), (coeff n) p ∈ f.range

The range of PowerSeries.map f consists of the power series whose coefficients all lie in the range of f.

theorem PowerSeries.coeff_mem_of_coeff_mul_mem {S : Type u_1} [Ring S] {R : Subring S} {m : ℕ} {F D : PowerSeries S} (hD : ∀ i < m, (coeff i) D = 0) (hDm : (coeff m) D = 1) (hDR : ∀ (i : ℕ), (coeff i) D ∈ R) (hFD : ∀ (n : ℕ), (coeff n) (F * D) ∈ R) (n : ℕ) : (coeff n) F ∈ R

Division by Xᵐ u with u(0) = 1 preserves coefficients in a subring. If D has coefficients in R, vanishes below degree m and has coefficient 1 in degree m, and F * D has coefficients in R, then F has coefficients in R.

@[simp]

theorem PowerSeries.forall_coeff_expand_mem_iff {S : Type u_2} [CommRing S] {R : Subring S} {p : ℕ} (hp : p ≠ 0) {φ : PowerSeries S} : (∀ (n : ℕ), (coeff n) ((expand p hp) φ) ∈ R) ↔ ∀ (n : ℕ), (coeff n) φ ∈ R

Expansion preserves and reflects coefficients in a subring. The coefficients of expand p φ, the power series φ with Xᵖ substituted for X, all lie in a subring R if and only if those of φ do.