Dirichlet characters agreeing at almost all primes

A Dirichlet character of nonzero level is determined by its values at all but finitely many primes. At a fixed level this is Dirichlet's theorem on primes in arithmetic progressions: every unit residue class contains primes larger than any given bound. Across two levels, both characters are lifted to a common multiple level, where they agree at all primes not dividing that level and outside the exceptional set; the lifts are then equal, so the two characters have the same conductor and the same primitive character. In particular, two primitive Dirichlet characters agreeing at almost all primes have the same level and are equal.

Agreement at almost all primes is written ∀ᶠ p in Filter.cofinite, p.Prime → χ p = ψ p. A hypothesis of the form "χ p = ψ p for every prime p ∉ S" with S finite is turned into this one by Set.Finite.eventually_cofinite_notMem.

Main results

• DirichletCharacter.eq_of_eventually_apply_prime_eq: two characters of the same nonzero level agreeing at almost all primes are equal.
• DirichletCharacter.changeLevel_eq_changeLevel_of_eventually_apply_prime_eq: two characters agreeing at almost all primes have the same lift to every common multiple of their levels.
• DirichletCharacter.conductor_eq_of_eventually_apply_prime_eq and DirichletCharacter.primitiveCharacter_apply_eq_of_eventually_apply_prime_eq: such characters have the same conductor and the same primitive character.
• DirichletCharacter.IsPrimitive.level_eq_of_eventually_apply_prime_eq and DirichletCharacter.IsPrimitive.apply_eq_of_eventually_apply_prime_eq: two primitive characters agreeing at almost all primes have equal levels and agree at every integer.

References

• M. A. Bennett and S. Siksek, A conjecture of Erdős, supersingular primes and short character sums, Ann. of Math. 191 (2020), §6, Lemma 6.2 (ii), whose uniqueness assertion is the statement for primitive characters.

theorem DirichletCharacter.eq_of_eventually_apply_prime_eq {R : Type u_1} [CommMonoidWithZero R] {N : ℕ} [NeZero N] {χ ψ : DirichletCharacter R N} (h : ∀ᶠ (p : ℕ) in Filter.cofinite, Nat.Prime p → χ ↑p = ψ ↑p) : χ = ψ

Two Dirichlet characters of the same nonzero level that agree at all but finitely many primes are equal.

theorem DirichletCharacter.changeLevel_eq_changeLevel_of_eventually_apply_prime_eq {R : Type u_1} [CommMonoidWithZero R] {N M L : ℕ} [NeZero L] {χ : DirichletCharacter R N} {ψ : DirichletCharacter R M} (hN : N ∣ L) (hM : M ∣ L) (h : ∀ᶠ (p : ℕ) in Filter.cofinite, Nat.Prime p → χ ↑p = ψ ↑p) : (changeLevel hN) χ = (changeLevel hM) ψ

Two Dirichlet characters of nonzero levels that agree at all but finitely many primes have the same lift to every common multiple of their levels.

theorem DirichletCharacter.conductor_eq_of_eventually_apply_prime_eq {R : Type u_1} [CommMonoidWithZero R] {N M : ℕ} [NeZero N] [NeZero M] {χ : DirichletCharacter R N} {ψ : DirichletCharacter R M} (h : ∀ᶠ (p : ℕ) in Filter.cofinite, Nat.Prime p → χ ↑p = ψ ↑p) : χ.conductor = ψ.conductor

Two Dirichlet characters of nonzero levels that agree at all but finitely many primes have the same conductor.

theorem DirichletCharacter.primitiveCharacter_apply_eq_of_eventually_apply_prime_eq {R : Type u_1} [CommMonoidWithZero R] {N M : ℕ} [Nontrivial R] [NeZero N] [NeZero M] {χ : DirichletCharacter R N} {ψ : DirichletCharacter R M} (h : ∀ᶠ (p : ℕ) in Filter.cofinite, Nat.Prime p → χ ↑p = ψ ↑p) (a : ℤ) : χ.primitiveCharacter ↑a = ψ.primitiveCharacter ↑a

Two Dirichlet characters of nonzero levels that agree at all but finitely many primes have the same primitive character: its values agree at every integer.

theorem DirichletCharacter.IsPrimitive.level_eq_of_eventually_apply_prime_eq {R : Type u_1} [CommMonoidWithZero R] {N M : ℕ} [NeZero N] [NeZero M] {χ : DirichletCharacter R N} {ψ : DirichletCharacter R M} (hχ : χ.IsPrimitive) (hψ : ψ.IsPrimitive) (h : ∀ᶠ (p : ℕ) in Filter.cofinite, Nat.Prime p → χ ↑p = ψ ↑p) : N = M

Two primitive Dirichlet characters of nonzero levels that agree at all but finitely many primes have the same level.

theorem DirichletCharacter.IsPrimitive.apply_eq_of_eventually_apply_prime_eq {R : Type u_1} [CommMonoidWithZero R] {N M : ℕ} [NeZero N] [NeZero M] {χ : DirichletCharacter R N} {ψ : DirichletCharacter R M} (hχ : χ.IsPrimitive) (hψ : ψ.IsPrimitive) (h : ∀ᶠ (p : ℕ) in Filter.cofinite, Nat.Prime p → χ ↑p = ψ ↑p) (a : ℤ) : χ ↑a = ψ ↑a

Two primitive Dirichlet characters of nonzero levels that agree at all but finitely many primes agree at every integer. Their levels are equal by DirichletCharacter.IsPrimitive.level_eq_of_eventually_apply_prime_eq.