Fields generated by newform coefficients and nebentypus values

The coefficient field of a newform is the subfield of ℂ generated over ℚ by its positive Fourier coefficients. The character field is generated by the values of its nebentypus. The good-prime Hecke recurrence recovers character values at good primes from two Fourier coefficients, and prime factorization extends the field inclusion to every character value. This inclusion supplies the base field for studying Galois conjugates within a fixed nebentypus space. Conversely, the Hecke recurrences generate every coefficient from those at the primes and the character values, so a subfield of ℂ contains the coefficient field exactly when it contains these (CoefficientField_le_iff_forall_prime_and_char).

Use TauCeti.CharacterField χ for the character field, or CharacterField χ after open TauCeti. Its defining equation, generator membership, and containment criterion are CharacterField_def, char_mem_CharacterField, and CharacterField_le_iff in the same namespace.

The construction follows the coefficient-field convention of Shimura, Introduction to the Arithmetic Theory of Automorphic Functions, §3. The recurrence is Diamond–Shurman, A First Course in Modular Forms, Proposition 5.8.5.

noncomputable def TauCeti.CoefficientField {N : ℕ} {k : ℤ} [NeZero N] (f : HeckeRing.GL2.Newform N k) : IntermediateField ℚ ℂ

The subfield of ℂ generated over ℚ by the positive-index Fourier coefficients of a newform.

Equations

• TauCeti.CoefficientField f = IntermediateField.adjoin ℚ (Set.range fun (n : ℕ+) => (PowerSeries.coeff ↑n) (UpperHalfPlane.qExpansion 1 ⇑f.toCuspForm))

theorem TauCeti.CoefficientField_def {N : ℕ} {k : ℤ} [NeZero N] (f : HeckeRing.GL2.Newform N k) : CoefficientField f = IntermediateField.adjoin ℚ (Set.range fun (n : ℕ+) => (PowerSeries.coeff ↑n) (UpperHalfPlane.qExpansion 1 ⇑f.toCuspForm))

The coefficient field as an adjoin of positive-index Fourier coefficients.

@[simp]

theorem TauCeti.coeff_mem_CoefficientField {N : ℕ} {k : ℤ} [NeZero N] (f : HeckeRing.GL2.Newform N k) (n : ℕ+) : (PowerSeries.coeff ↑n) (UpperHalfPlane.qExpansion 1 ⇑f.toCuspForm) ∈ CoefficientField f

The Fourier coefficients generating CoefficientField belong to it.

@[simp]

theorem TauCeti.CoefficientField_le_iff {N : ℕ} {k : ℤ} [NeZero N] (f : HeckeRing.GL2.Newform N k) (K : IntermediateField ℚ ℂ) : CoefficientField f ≤ K ↔ ∀ (n : ℕ+), (PowerSeries.coeff ↑n) (UpperHalfPlane.qExpansion 1 ⇑f.toCuspForm) ∈ K

A field contains CoefficientField f exactly when it contains every positive-index Fourier coefficient of f.

noncomputable def TauCeti.CharacterField {N : ℕ} (χ : (ZMod N)ˣ →* ℂˣ) : IntermediateField ℚ ℂ

The subfield of ℂ generated over ℚ by the values of a nebentypus character.

Equations

• TauCeti.CharacterField χ = IntermediateField.adjoin ℚ (Set.range fun (u : (ZMod N)ˣ) => ↑(χ u))

theorem TauCeti.CharacterField_def {N : ℕ} (χ : (ZMod N)ˣ →* ℂˣ) : CharacterField χ = IntermediateField.adjoin ℚ (Set.range fun (u : (ZMod N)ˣ) => ↑(χ u))

The character field as an adjoin of character values.

@[simp]

theorem TauCeti.char_mem_CharacterField {N : ℕ} (χ : (ZMod N)ˣ →* ℂˣ) (u : (ZMod N)ˣ) : ↑(χ u) ∈ CharacterField χ

Every value of the nebentypus belongs to its character field.

@[simp]

theorem TauCeti.CharacterField_le_iff {N : ℕ} (χ : (ZMod N)ˣ →* ℂˣ) (K : IntermediateField ℚ ℂ) : CharacterField χ ≤ K ↔ ∀ (u : (ZMod N)ˣ), ↑(χ u) ∈ K

A field contains CharacterField χ exactly when it contains every value of χ.

theorem TauCeti.char_prime_eq_coeff {N : ℕ} {k : ℤ} [NeZero N] (f : HeckeRing.GL2.Newform N k) {p : ℕ} (hp : Nat.Prime p) (hpN : p.Coprime N) : ↑(f.χ (ZMod.unitOfCoprime p hpN)) = ((PowerSeries.coeff p) (UpperHalfPlane.qExpansion 1 ⇑f.toCuspForm) * (PowerSeries.coeff p) (UpperHalfPlane.qExpansion 1 ⇑f.toCuspForm) - (PowerSeries.coeff (p ^ 2)) (UpperHalfPlane.qExpansion 1 ⇑f.toCuspForm)) / ↑p ^ (k - 1)

At a prime p coprime to the level, the Hecke recurrence gives χ(p) = (a_p^2 - a_{p^2}) / p^(k-1).

theorem TauCeti.char_prime_mem_CoefficientField {N : ℕ} {k : ℤ} [NeZero N] (f : HeckeRing.GL2.Newform N k) {p : ℕ} (hp : Nat.Prime p) (hpN : p.Coprime N) : ↑(f.χ (ZMod.unitOfCoprime p hpN)) ∈ CoefficientField f

The nebentypus value at a good prime belongs to the coefficient field.

@[simp]

theorem TauCeti.char_mem_CoefficientField {N : ℕ} {k : ℤ} [NeZero N] (f : HeckeRing.GL2.Newform N k) (u : (ZMod N)ˣ) : ↑(f.χ u) ∈ CoefficientField f

Every value of the nebentypus of a newform lies in its coefficient field.

theorem TauCeti.CharacterField_le_CoefficientField {N : ℕ} {k : ℤ} [NeZero N] (f : HeckeRing.GL2.Newform N k) : CharacterField f.χ ≤ CoefficientField f

The field generated by the nebentypus values of a newform is a subfield of its coefficient field.

theorem TauCeti.CoefficientField_le_iff_forall_prime_and_char {N : ℕ} {k : ℤ} [NeZero N] (f : HeckeRing.GL2.Newform N k) (K : IntermediateField ℚ ℂ) : CoefficientField f ≤ K ↔ (∀ (p : ℕ), Nat.Prime p → (PowerSeries.coeff p) (UpperHalfPlane.qExpansion 1 ⇑f.toCuspForm) ∈ K) ∧ ∀ (u : (ZMod N)ˣ), ↑(f.χ u) ∈ K

A field contains CoefficientField f exactly when it contains the Fourier coefficients of f at the primes and the values of its nebentypus. The coefficients at the remaining indices follow from the Hecke recurrences.