Power series supported on multiples of d

A power series is supported on multiples of d when every coefficient at an index not divisible by d vanishes. The condition is preserved by the module operations, so the series satisfying it form a submodule, and — over a commutative ring — they are exactly what the substitution q ↦ q ^ d (PowerSeries.expand) produces.

That last statement is an equality of submodules, proved in both directions. The inclusion the modular-form applications actually use is the easy one, that a level-raise is supported; the converse recovers the series substituted into, as PowerSeries.mk fun n ↦ P.coeff (d * n), and is what makes the description of the supported submodule complete rather than one-sided.

Nothing here mentions a modular form: the predicate is about power series over any type with a zero, and the modular-form consequences live in TauCeti/NumberTheory/ModularForms/Degeneracy.lean and TauCeti/NumberTheory/ModularForms/Newforms/QSupport.lean, the latter obtaining its submodule of cusp forms by pulling PowerSeries.supportedOnDvdSubmodule back along the q-expansion.

Main definitions

• PowerSeries.IsSupportedOnDvd: the support condition on a power series.
• PowerSeries.supportedOnDvdSubmodule: the same condition bundled as a submodule.

Main results

• PowerSeries.IsSupportedOnDvd.add, .smul, .neg, .sub: the condition is preserved by the module operations, and .one, .mul by the ring ones.
• PowerSeries.isSupportedOnDvd_expand: the substitution q ↦ q ^ d lands in the supported series. This is the direction the modular-form applications use, so every q ↦ q ^ d statement about a q-expansion reduces to it.
• PowerSeries.IsSupportedOnDvd.exists_expand and PowerSeries.isSupportedOnDvd_iff_exists_expand: the converse and the resulting characterisation — a series is supported on multiples of d exactly when it is a q ↦ q ^ d substitution.
• PowerSeries.range_expand_eq_supportedOnDvdSubmodule: the same characterisation in submodule form, an equality rather than a containment.

Typeclass assumptions

Each declaration assumes only what its own operation needs, which is worth recording because the coefficient condition invites a uniform [Semiring R]:

• the predicate and .zero need only [Zero R]. PowerSeries R is (Unit →₀ ℕ) → R, so the condition is stated by evaluating that function. Going through PowerSeries.coeff instead — a bundled R-linear map — would force a semiring here and on every lemma below;
• .add needs [AddMonoid R] and .neg, .sub need [AddGroup R]: those are exactly where Mathlib puts + and - on MvPowerSeries σ R;
• .smul needs [Semiring S] [AddCommMonoid R] [Module S R], Mathlib's only scalar action on power series;
• .one and .mul need [Semiring R], since they are about the ring operations, and the expand lemmas need [CommRing R], since PowerSeries.expand is an R-algebra homomorphism defined only there.

isSupportedOnDvd_iff restates the predicate through coeff for the semiring consumers, which is how every use site spells it.

Provenance

IsSupportedOnDvd and its closure lemmas zero, add, smul, neg, sub, one are adapted from the AINTLIB LeanModularForms project (Chris Birkbeck, github.com/CBirkbeck/AINTLIB, Apache-2.0) at commit 2baa76f74, file projects/LeanModularForms/LeanModularForms/Eigenforms/AtkinLehner.lean. The source states them over ℂ, inside its HeckeRing.GL2.AtkinLehner namespace; here each is stated over the weakest coefficient structure its own operation needs — the predicate and zero over [Zero R], add over [AddMonoid R], neg and sub over [AddGroup R], smul over a module, one and mul over [Semiring R] — and they are placed in the PowerSeries namespace under RingTheory/ accordingly, since nothing in them mentions a modular form. The modular-form consequences the source draws from them are in TauCeti/NumberTheory/ModularForms/Degeneracy.lean.

The expand characterisation has no counterpart in the source, which reaches the same conclusions by a coefficient computation at each use site.

Pointwise evaluation

PowerSeries R unfolds to (Unit →₀ ℕ) → R and carries exactly the pointwise algebraic structure, but it is a semireducible def, so Mathlib's Pi.add_apply and its siblings do not match against it. The four lemmas below record that pointwise behaviour once and for all, so the closure proofs further down are ordinary rewrites instead of restating the same definitional equality inline at each use. They are private: a consumer with a semiring available works through PowerSeries.coeff, whose simp lemmas cover this already.

def PowerSeries.IsSupportedOnDvd {R : Type u_1} [Zero R] (d : ℕ) (P : PowerSeries R) : Prop

A power series is supported on multiples of d when its coefficient at every index not divisible by d vanishes.

Stated by evaluating the underlying coefficient function — PowerSeries R is (Unit →₀ ℕ) → R — rather than through PowerSeries.coeff, which is a bundled R-linear map and would impose [Semiring R] on the predicate and on every closure lemma below. Only the operation each lemma is about is then assumed: [AddMonoid R] for add, [AddGroup R] for neg and sub, a semiring only where multiplication genuinely enters. isSupportedOnDvd_iff is the coeff form, for use once there is a semiring to state it in.

Equations

• PowerSeries.IsSupportedOnDvd d P = ∀ (n : ℕ), ¬d ∣ n → P (Finsupp.single () n) = 0

theorem PowerSeries.isSupportedOnDvd_iff {R : Type u_1} [Semiring R] {d : ℕ} {P : PowerSeries R} : IsSupportedOnDvd d P ↔ ∀ (n : ℕ), ¬d ∣ n → (coeff n) P = 0

IsSupportedOnDvd in the PowerSeries.coeff spelling, which is how every consumer states it. Definitionally the same condition: coeff n is evaluation at Finsupp.single () n.

@[simp]

theorem PowerSeries.IsSupportedOnDvd.zero {R : Type u_1} [Zero R] (d : ℕ) : IsSupportedOnDvd d 0

theorem PowerSeries.IsSupportedOnDvd.add {R : Type u_1} {d : ℕ} {P Q : PowerSeries R} [AddMonoid R] (hP : IsSupportedOnDvd d P) (hQ : IsSupportedOnDvd d Q) : IsSupportedOnDvd d (P + Q)

theorem PowerSeries.IsSupportedOnDvd.smul {R : Type u_1} {S : Type u_2} {d : ℕ} {P : PowerSeries R} [Semiring S] [AddCommMonoid R] [Module S R] (c : S) (hP : IsSupportedOnDvd d P) : IsSupportedOnDvd d (c • P)

theorem PowerSeries.IsSupportedOnDvd.neg {R : Type u_1} {d : ℕ} {P : PowerSeries R} [AddGroup R] (hP : IsSupportedOnDvd d P) : IsSupportedOnDvd d (-P)

theorem PowerSeries.IsSupportedOnDvd.sub {R : Type u_1} {d : ℕ} {P Q : PowerSeries R} [AddGroup R] (hP : IsSupportedOnDvd d P) (hQ : IsSupportedOnDvd d Q) : IsSupportedOnDvd d (P - Q)

@[simp]

theorem PowerSeries.IsSupportedOnDvd.one {R : Type u_1} [Semiring R] (d : ℕ) : IsSupportedOnDvd d 1

The constant power series 1 is supported on multiples of any d: its only nonzero coefficient sits at 0, which every d divides.

theorem PowerSeries.IsSupportedOnDvd.mul {R : Type u_1} {d : ℕ} {P Q : PowerSeries R} [Semiring R] (hP : IsSupportedOnDvd d P) (hQ : IsSupportedOnDvd d Q) : IsSupportedOnDvd d (P * Q)

The condition is closed under multiplication. In a coefficient of P * Q at an index n not divisible by d, each term aᵢ · b_j with i + j = n has one of its two factors at an index away from the multiples of d: if d ∣ i then d ∤ j, since otherwise d ∣ n.

Both hypotheses are needed, and one-sidedness fails already over ℕ: 1 is supported on multiples of 2 while 1 * X = X is not. The coefficient semiring has to be named — over the trivial one X = 0, which is supported.

def PowerSeries.supportedOnDvdSubmodule (R : Type u_1) [Semiring R] (d : ℕ) : Submodule R (PowerSeries R)

The submodule of power series supported on multiples of d. This is the bundled form of IsSupportedOnDvd; its closure proofs are exactly the lemmas above.

Equations

• PowerSeries.supportedOnDvdSubmodule R d = { carrier := {P : PowerSeries R | PowerSeries.IsSupportedOnDvd d P}, add_mem' := ⋯, zero_mem' := ⋯, smul_mem' := ⋯ }

@[simp]

theorem PowerSeries.mem_supportedOnDvdSubmodule {R : Type u_1} [Semiring R] {d : ℕ} {P : PowerSeries R} : P ∈ supportedOnDvdSubmodule R d ↔ IsSupportedOnDvd d P

theorem PowerSeries.isSupportedOnDvd_expand {R : Type u_1} [CommRing R] {d : ℕ} (hd : d ≠ 0) (P : PowerSeries R) : IsSupportedOnDvd d ((expand d hd) P)

Substituting q ↦ q ^ d lands in the supported series. Every coefficient of PowerSeries.expand d sits at a multiple of d, which is the defining condition. This is the bridge that turns a q ↦ q ^ d description of a series into the support condition, so the support statements downstream never repeat the coefficient computation.

theorem PowerSeries.IsSupportedOnDvd.exists_expand {R : Type u_1} [CommRing R] {d : ℕ} (hd : d ≠ 0) {P : PowerSeries R} (hP : IsSupportedOnDvd d P) : ∃ (Q : PowerSeries R), (expand d hd) Q = P

Every supported series is a substitution q ↦ q ^ d, the converse of PowerSeries.isSupportedOnDvd_expand. The series substituted into is recovered by reading off the coefficients that survive, PowerSeries.mk fun n ↦ P.coeff (d * n): at an index d * m the two sides agree by PowerSeries.coeff_expand_mul, and elsewhere both vanish — the left by PowerSeries.coeff_expand_of_not_dvd, the right by hypothesis.

theorem PowerSeries.isSupportedOnDvd_iff_exists_expand {R : Type u_1} [CommRing R] {d : ℕ} (hd : d ≠ 0) (P : PowerSeries R) : IsSupportedOnDvd d P ↔ ∃ (Q : PowerSeries R), (expand d hd) Q = P

Being supported on multiples of d is exactly being a substitution q ↦ q ^ d. The two directions are PowerSeries.IsSupportedOnDvd.exists_expand and PowerSeries.isSupportedOnDvd_expand.

theorem PowerSeries.range_expand_eq_supportedOnDvdSubmodule {R : Type u_1} [CommRing R] {d : ℕ} (hd : d ≠ 0) : (expand d hd).toLinearMap.range = supportedOnDvdSubmodule R d

The range of PowerSeries.expand d is the supported submodule, the bundled form of PowerSeries.isSupportedOnDvd_iff_exists_expand. expand is an AlgHom, so the range is taken of its underlying linear map.