Factoring a Dirichlet character through a divisor

Facts about when a Dirichlet character χ mod N factors through a divisor of N, stated for characters valued in any CommMonoidWithZero, which is the generality of DirichletCharacter.factorsThrough_iff_ker_unitsMap and of the conductor.

If χ does not factor through d ∣ N, then knowing a unit's reduction modulo d does not determine its character value: every unit has a partner in the same fibre of ZMod.unitsMap on which χ takes a different value. This is the form the level-lowering argument for the conductor theorem consumes.

If the lift of χ to a multiple level factors through d, then χ itself factors through gcd (N, d): changeLevel preserves the conductor, which then divides both. This is how a factorisation found at an auxiliary level is brought back to the level of χ; the arithmetic case the descent uses is d = L N / p with p ∣ N coprime to L, where the gcd is N / p.

Main results

• DirichletCharacter.exists_alt_unit_in_coset_with_char_separation: character separation within a fibre of the reduction map.
• DirichletCharacter.factorsThrough_gcd_of_changeLevel_factorsThrough: a factorisation of the lift to a multiple level through d descends to a factorisation of χ through gcd (N, d), and DirichletCharacter.factorsThrough_div_of_changeLevel_factorsThrough: its arithmetic specialisation, from L N / p to N / p.
• DirichletCharacter.exists_eq_comp_unitsMap_of_factorsThrough: a factorisation of MulChar.ofUnitHom χ through d, read back on unit homomorphisms as χ = χ₀ ∘ unitsMap.
• DirichletCharacter.even_changeLevel_iff: changing the level preserves parity.
• DirichletCharacter.conductor_eq_prime_pow_of_emod_eq_of_apply_ne_apply: a primitivity criterion at a prime-power level, obtained by comparing values on congruent units, and its specialisations DirichletCharacter.conductor_eq_four_of_apply_one_ne_apply_three and DirichletCharacter.conductor_eq_eight_of_apply_one_ne_apply_five.

Provenance

Adapted from the AINTLIB LeanModularForms project (Chris Birkbeck, github.com/CBirkbeck/AINTLIB, Apache-2.0) at commit 2baa76f74, file projects/LeanModularForms/LeanModularForms/Eigenforms/ConductorTheorem.lean, declaration exists_alt_unit_in_coset_with_char_separation (:656). The source reaches it through an intermediate shift form (exists_kernel_unit_with_char_shift, :646) and a separate non-factorisation witness (exists_unit_of_not_factorsThrough, :542); each is a one-line consequence of the other, so only this form is ported and the extraction is done inline.

factorsThrough_div_of_changeLevel_factorsThrough is extracted from the same project at commit eb9621e7bcb0ce220ad53983ec45d987cb5b9002, file projects/LeanModularForms/LeanModularForms/StrongMultiplicityOne/InductiveStep.lean: the conductor step inside the proof of miyake_4_6_8_factor_dichotomy, which the source carries as the private lemmas conductor_dvd_of_factorsThrough, factorsThrough_of_conductor_dvd and conductor_changeLevel specialised to L N / p. Here those three are Mathlib's conductor_dvd_of_mem_conductorSet, mem_conductorSet_iff_conductor_dvd and conductor_changeLevel, so what is ported is the arithmetic of the descent — the conductor divides gcd (N, L N / p) = N / p — stated once for characters valued in any CommMonoidWithZero.

theorem DirichletCharacter.apply_eq_apply_of_factorsThrough {R : Type u_1} [CommMonoidWithZero R] {N d : ℕ} (chi : DirichletCharacter R N) (hfac : chi.FactorsThrough d) {a b : ℤ} (ha : IsCoprime a ↑N) (hb : IsCoprime b ↑N) (hab : a % ↑d = b % ↑d) : chi ↑a = chi ↑b

A character which factors through d takes the same value on level-units congruent modulo d.

theorem DirichletCharacter.conductor_eq_prime_pow_of_emod_eq_of_apply_ne_apply {R : Type u_1} [CommMonoidWithZero R] {p k : ℕ} (hp : Nat.Prime p) (chi : DirichletCharacter R (p ^ k)) {a b : ℤ} (ha : IsCoprime a ↑(p ^ k)) (hb : IsCoprime b ↑(p ^ k)) (hab : a % ↑(p ^ (k - 1)) = b % ↑(p ^ (k - 1))) (hdist : chi ↑a ≠ chi ↑b) : chi.conductor = p ^ k

A primitivity criterion at a prime-power level. A character of level p ^ k taking different values on two level-units congruent modulo p ^ (k - 1) cannot factor through a proper divisor of its level, so its conductor is the full level p ^ k.

theorem DirichletCharacter.conductor_eq_four_of_apply_one_ne_apply_three {R : Type u_1} [CommMonoidWithZero R] (chi : DirichletCharacter R 4) (hdist : chi ↑1 ≠ chi ↑3) : chi.conductor = 4

A character of level four which distinguishes 1 and 3 is primitive.

theorem DirichletCharacter.conductor_eq_eight_of_apply_one_ne_apply_five {R : Type u_1} [CommMonoidWithZero R] (chi : DirichletCharacter R 8) (hdist : chi ↑1 ≠ chi ↑5) : chi.conductor = 8

A character of level eight which distinguishes 1 and 5 is primitive.

theorem DirichletCharacter.exists_alt_unit_in_coset_with_char_separation {R : Type u_1} [CommMonoidWithZero R] {N : ℕ} [NeZero N] {d : ℕ} (hd : d ∣ N) {χ : DirichletCharacter R N} (h_not_fac : ¬χ.FactorsThrough d) (u : (ZMod N)ˣ) : ∃ (u' : (ZMod N)ˣ), (ZMod.unitsMap hd) u' = (ZMod.unitsMap hd) u ∧ (MulChar.toUnitHom χ) u' ≠ (MulChar.toUnitHom χ) u

Character separation within a coset. If χ does not factor through d ∣ N, then every unit u has a partner u' with the same reduction modulo d but a different character value — so the character cannot be read off the reduction alone.

theorem DirichletCharacter.factorsThrough_gcd_of_changeLevel_factorsThrough {R : Type u_1} [CommMonoidWithZero R] {N M d : ℕ} [NeZero M] (hNM : N ∣ M) {ψ : DirichletCharacter R N} (hfac : ((changeLevel hNM) ψ).FactorsThrough d) : ψ.FactorsThrough (N.gcd d)

A factorisation found at a multiple level descends to the gcd. If the lift of ψ mod N to a multiple level M factors through d, then ψ factors through gcd (N, d): changeLevel preserves the conductor, which then divides both the level N and d.

theorem DirichletCharacter.factorsThrough_div_of_changeLevel_factorsThrough {R : Type u_1} [CommMonoidWithZero R] {N p L : ℕ} [NeZero N] [NeZero L] (hpN : p ∣ N) (hpL : p.Coprime L) {ψ : DirichletCharacter R N} (hfac : ((changeLevel ⋯) ψ).FactorsThrough (L * N / p)) : ψ.FactorsThrough (N / p)

A factorisation found at an auxiliary level descends. If the lift of ψ mod N to level L N factors through L N / p, for p ∣ N coprime to L, then ψ factors through N / p. This is factorsThrough_gcd_of_changeLevel_factorsThrough at the gcd gcd (N, L N / p) = gcd (p, L) · (N / p) = N / p.

theorem DirichletCharacter.exists_eq_comp_unitsMap_of_factorsThrough {R : Type u_1} [CommMonoidWithZero R] {N d : ℕ} (hd : d ∣ N) {χ : (ZMod N)ˣ →* Rˣ} (hfac : FactorsThrough (MulChar.ofUnitHom χ) d) : ∃ (χ₀ : (ZMod d)ˣ →* Rˣ), χ = χ₀.comp (ZMod.unitsMap hd)

A factorisation, read on unit homomorphisms. If the Dirichlet character MulChar.ofUnitHom χ factors through d ∣ N, the unit homomorphism χ is itself a composition χ₀ ∘ ZMod.unitsMap with a unit homomorphism modulo d — the form in which a lowered nebentypus is consumed, by the descent lemmas of Newforms/Descent and by the Main Lemma's induction.

@[simp]

theorem DirichletCharacter.even_changeLevel_iff {S : Type u_1} [CommRing S] {d n : ℕ} (h : d ∣ n) (χ : DirichletCharacter S d) : ((changeLevel h) χ).Even ↔ χ.Even

Changing the level preserves parity: the value at -1 of a Dirichlet character is the value at -1 of its lift to any multiple level.