Conductors and primitive Dirichlet characters

DefinitionDirichlet character of a given modulus#✓fully proved

Let \(R\) be a monoid with zero, let \(\chi \colon \mathbb{Z} \to R\) be a multiplicative map with \(\chi(1) = 1\), and let \(q\) be a natural number. Then \(\chi\) is a Dirichlet character of modulus \(q\) if \(\chi(n + q) = \chi(n)\) for every integer \(n\), and, for every integer \(n\), \(\chi(n) \neq 0\) if and only if \(q\) and \(n\) are coprime.

def IsDirichletCharacterModulus (χ : ℤ →* R) (q : ℕ) : Prop :=
  Function.Periodic χ (q : ℤ) ∧ ∀ n : ℤ, χ n ≠ 0 ↔ IsCoprime (q : ℤ) n
Used by 2
Used byModuli of a character with a given least period · A character is a Dirichlet character modulo its least period

TheoremModuli of a character with a given least period#✓fully proved

Let \(R\) be a nontrivial monoid with zero in which nonzero elements can be cancelled on both sides, and let \(\chi \colon \mathbb{Z} \to R\) be a multiplicative map with \(\chi(1) = 1\). Suppose \(m \ge 1\) is the least positive period of \(\chi\): \(\chi(n + m) = \chi(n)\) for every integer \(n\), and every positive integer \(d\) with \(\chi(n + d) = \chi(n)\) for all \(n\) satisfies \(m \le d\). Then for every integer \(m' \ge 1\), \(\chi\) is a Dirichlet character of modulus \(m'\) if and only if \(m \mid m'\) and \(m' \mid m^k\) for some natural number \(k\).

The hypothesis that \(R\) is nontrivial cannot be dropped: in the zero monoid every value of \(\chi\) is \(0\), so \(\chi\) is a Dirichlet character of no modulus.

theorem isDirichletCharacterModulus_iff {χ : ℤ →* R} [Nontrivial R]
    [IsCancelMulZero R] {m m' : ℕ}
    (hm : 0 < m)
    (hper : Function.Periodic χ (m : ℤ))
    (hmin : ∀ d : ℕ, 0 < d → Function.Periodic χ (d : ℤ) → m ≤ d)
    (hm' : 0 < m') :
    χ.IsDirichletCharacterModulus m' ↔ m ∣ m' ∧ ∃ k : ℕ, m' ∣ m ^ k
Sources
  • ATLAS NumberTheoryI Lemma 18.8. Forward: minimality gives the divisibility, and a prime divisor of m' divides m (else χ p is simultaneously zero and nonzero). Backward: periodicity lifts along m ∣ m', and the nonvanishing locus transfers via the two lemmas above.
Uses 1 · Used by 1
Statement usesDirichlet character of a given modulus
Used byA character is a Dirichlet character modulo its least period

TheoremA character is a Dirichlet character modulo its least period#✓fully proved

Let \(R\) be a nontrivial monoid with zero in which nonzero elements can be cancelled on both sides, and let \(\chi \colon \mathbb{Z} \to R\) be a multiplicative map with \(\chi(1) = 1\). If \(m \ge 1\) is the least positive period of \(\chi\) (that is, \(\chi(n + m) = \chi(n)\) for every integer \(n\), and every positive integer \(d\) with \(\chi(n + d) = \chi(n)\) for all \(n\) satisfies \(m \le d\)), then \(\chi\) is a Dirichlet character of modulus \(m\).

theorem isDirichletCharacterModulus_self {χ : ℤ →* R} [Nontrivial R]
    [IsCancelMulZero R] {m : ℕ} (hm : 0 < m)
    (hper : Function.Periodic χ (m : ℤ))
    (hmin : ∀ d : ℕ, 0 < d → Function.Periodic χ (d : ℤ) → m ≤ d) :
    χ.IsDirichletCharacterModulus m
Uses 2
Statement usesDirichlet character of a given modulus
Proof usesModuli of a character with a given least period

StructurePrimitive characters at divisor levels#✓fully proved

Let \(R\) be a commutative monoid with zero and \(m\) a natural number. A primitive inducer of modulus \(m\) with values in \(R\) consists of a natural number \(d\), its level, with \(d \mid m\), together with a Dirichlet character \(\psi\) of level \(d\) with values in \(R\) that is primitive, that is, whose conductor is \(d\). These are the elements of the set \(X(m)\) of Corollary 18.16; changing the level of \(\psi\) from \(d\) to \(m\) gives the induced Dirichlet character of level \(m\).

structure PrimitiveInducer (R : Type*) [CommMonoidWithZero R] (m : ℕ) where
  level : ℕ
  level_dvd : level ∣ m
  char : DirichletCharacter R level
  isPrimitive : char.IsPrimitive
Used by 6
Used byDirichlet characters correspond to primitive characters at divisor levels · Character of the primitive inducer attached to a character · Level of the primitive inducer attached to a character · Primitive characters at divisor levels correspond to unit-group characters · Values of the unit-group character of a primitive inducer · Equality of primitive characters at divisor levels

TheoremEquality of primitive characters at divisor levels#✓fully proved

Let \(R\) be a commutative monoid with zero and \(m\) a natural number, and let \(p\) and \(q\) be primitive inducers of modulus \(m\) with values in \(R\). If \(p\) and \(q\) have the same level, and the character of \(p\), transported along this equality of levels, equals the character of \(q\), then \(p = q\).

theorem ext {p q : PrimitiveInducer R m} (hlevel : p.level = q.level)
    (hchar : hlevel ▸ p.char = q.char) : p = q
Uses 1 · Used by 1
Statement usesPrimitive characters at divisor levels
Used byDirichlet characters correspond to primitive characters at divisor levels

DefinitionDirichlet characters correspond to primitive characters at divisor levels#✓fully proved

Let \(R\) be a commutative monoid with zero and \(m \ge 1\) a natural number. This is the bijection from Dirichlet characters of level \(m\) with values in \(R\) to primitive inducers of modulus \(m\) (primitive Dirichlet characters with values in \(R\) whose level divides \(m\)) that sends \(\chi\) to the primitive character associated to \(\chi\), whose level is the conductor of \(\chi\). Its inverse sends a primitive character \(\psi\) of level \(d \mid m\) to the Dirichlet character of level \(m\) obtained from \(\psi\) by changing the level from \(d\) to \(m\).

DirichletCharacter.equivPrimitiveInducer · 18 lines 
noncomputable def equivPrimitiveInducer (m : ℕ) (hm : m ≠ 0) :
    DirichletCharacter R m ≃ PrimitiveInducer R m where
  toFun χ :=
    { level := χ.conductor
      level_dvd := χ.conductor_dvd_level
      char := χ.primitiveCharacter
      isPrimitive := χ.primitiveCharacter_isPrimitive }
  invFun p := changeLevel p.level_dvd p.char
  left_inv χ := changeLevel_primitiveCharacter χ
  right_inv p := by
    obtain ⟨d, hd, ψ, hprim⟩ := p
    have : NeZero m := ⟨hm⟩
    have hlevel : (changeLevel hd ψ).conductor = d :=
      (conductor_changeLevel ψ hd).trans hprim
    apply PrimitiveInducer.ext hlevel
    apply changeLevel_injective hd
    rw [PrimitiveInducer.changeLevel_cast_eq hlevel hd]
    exact changeLevel_primitiveCharacter (changeLevel hd ψ)
Sources
  • ATLAS NumberTheoryI, Section 18.2.1, Corollary 18.16 (first bijection).
Uses 2 · Used by 4
Statement usesPrimitive characters at divisor levels · Equality of primitive characters at divisor levels
Used byCharacter of the primitive inducer attached to a character · Level of the primitive inducer attached to a character · Primitive characters at divisor levels correspond to unit-group characters · Values of the unit-group character of a primitive inducer

TheoremLevel of the primitive inducer attached to a character#✓fully proved

Let \(R\) be a commutative monoid with zero, let \(m \ge 1\), and let \(\chi\) be a Dirichlet character of level \(m\) with values in \(R\). The level of the primitive inducer that the bijection between Dirichlet characters of level \(m\) and primitive inducers of modulus \(m\) assigns to \(\chi\) is the conductor of \(\chi\).

theorem equivPrimitiveInducer_level (χ : DirichletCharacter R m) (hm : m ≠ 0) :
    (equivPrimitiveInducer m hm χ).level = χ.conductor
Uses 2
Statement usesPrimitive characters at divisor levels · Dirichlet characters correspond to primitive characters at divisor levels

TheoremCharacter of the primitive inducer attached to a character#✓fully proved

Let \(R\) be a commutative monoid with zero, let \(m \ge 1\), and let \(\chi\) be a Dirichlet character of level \(m\) with values in \(R\). The character of the primitive inducer that the bijection between Dirichlet characters of level \(m\) and primitive inducers of modulus \(m\) assigns to \(\chi\), a Dirichlet character whose level is the conductor of \(\chi\), is the primitive character associated to \(\chi\).

theorem equivPrimitiveInducer_char (χ : DirichletCharacter R m) (hm : m ≠ 0) :
    ((equivPrimitiveInducer m hm χ).char : DirichletCharacter R χ.conductor) =
      χ.primitiveCharacter
Uses 2
Statement usesPrimitive characters at divisor levels · Dirichlet characters correspond to primitive characters at divisor levels

DefinitionPrimitive characters at divisor levels correspond to unit-group characters#✓fully proved

Let \(R\) be a commutative monoid with zero and \(m \ge 1\) a natural number. This is the bijection from primitive inducers of modulus \(m\) with values in \(R\) to monoid homomorphisms \((\mathbb{Z}/m\mathbb{Z})^\times \to R^\times\) that sends a primitive character \(\psi\) of level \(d \mid m\) to the homomorphism \(u \mapsto \chi(u)\), where \(\chi\) is the Dirichlet character of level \(m\) obtained from \(\psi\) by changing the level from \(d\) to \(m\).

noncomputable def PrimitiveInducer.equivUnitHom (m : ℕ) (hm : m ≠ 0) :
    PrimitiveInducer R m ≃ ((ZMod m)ˣ →* Rˣ) :=
  (equivPrimitiveInducer m hm).symm.trans MulChar.equivToUnitHom
Sources
  • ATLAS NumberTheoryI, Section 18.2.1, Corollary 18.16 (second bijection).
Uses 2 · Used by 1
Statement usesPrimitive characters at divisor levels · Dirichlet characters correspond to primitive characters at divisor levels
Used byValues of the unit-group character of a primitive inducer

TheoremValues of the unit-group character of a primitive inducer#✓fully proved

Let \(R\) be a commutative monoid with zero, let \(m \ge 1\), and let \(p\) be a primitive inducer of modulus \(m\) with values in \(R\), with level \(d\) and character \(\psi\). For every unit \(u\) of \(\mathbb{Z}/m\mathbb{Z}\), the value at \(u\) of the homomorphism \((\mathbb{Z}/m\mathbb{Z})^\times \to R^\times\) corresponding to \(p\), viewed as an element of \(R\), equals the value at \(u\) of the Dirichlet character of level \(m\) obtained from \(\psi\) by changing the level from \(d\) to \(m\).

@[simp] theorem PrimitiveInducer.equivUnitHom_apply
    (p : PrimitiveInducer R m) (hm : m ≠ 0) (u : (ZMod m)ˣ) :
    (PrimitiveInducer.equivUnitHom m hm p u : R) =
      changeLevel p.level_dvd p.char (u : ZMod m)
Uses 3
Statement usesPrimitive characters at divisor levels · Primitive characters at divisor levels correspond to unit-group characters
Proof usesDirichlet characters correspond to primitive characters at divisor levels

TheoremThe level of a primitive inducer is the conductor#✓fully proved

Let \(R\) be a commutative monoid with zero, let \(n \ge 1\) and \(d\) be natural numbers with \(d \mid n\), and let \(\chi\) be a Dirichlet character of level \(n\) with values in \(R\). If \(\chi'\) is a primitive Dirichlet character of level \(d\) whose change of level to \(n\) is \(\chi\), then \(d\) equals the conductor of \(\chi\).

public theorem conductor_eq_of_isPrimitive_changeLevel {d : ℕ}
    {χ' : DirichletCharacter R d} (χ : DirichletCharacter R n)
    (hprim : χ'.IsPrimitive) (hd : d ∣ n)
    (h : changeLevel hd χ' = χ) : d = χ.conductor
Used by 1
Used byExistence and uniqueness of the primitive character inducing a Dirichlet character

TheoremAn inducer at the conductor level is the primitive character#✓fully proved

Let \(R\) be a commutative monoid with zero, let \(n \ge 1\) and \(d\) be natural numbers with \(d \mid n\), and let \(\chi\) be a Dirichlet character of level \(n\) with values in \(R\) whose conductor is \(d\). If \(\chi'\) is a Dirichlet character of level \(d\) whose change of level to \(n\) is \(\chi\), then \(\chi'\) is the primitive character associated to \(\chi\).

public theorem eq_primitiveCharacter_of_changeLevel_eq {d : ℕ}
    {χ' : DirichletCharacter R d} (χ : DirichletCharacter R n)
    (hlev : d = χ.conductor) (hd : d ∣ n)
    (h : changeLevel hd χ' = χ) :
    hlev ▸ χ' = χ.primitiveCharacter
Used by 1
Used byExistence and uniqueness of the primitive character inducing a Dirichlet character

TheoremExistence and uniqueness of the primitive character inducing a Dirichlet character#✓fully proved

Let \(R\) be a commutative monoid with zero, let \(n \ge 1\), and let \(\chi\) be a Dirichlet character of level \(n\) with values in \(R\). The primitive character associated to \(\chi\), whose level is the conductor of \(\chi\), is primitive, and its change of level to \(n\) is \(\chi\). Moreover, if \(\chi'\) is a primitive Dirichlet character of some level \(d\) with \(d \mid n\) whose change of level to \(n\) is \(\chi\), then \(d\) is the conductor of \(\chi\) and \(\chi'\) is the primitive character associated to \(\chi\).

public theorem primitiveCharacter_isPrimitive_and_unique (χ : DirichletCharacter R n) :
    χ.primitiveCharacter.IsPrimitive ∧
      changeLevel (conductor_dvd_level χ) χ.primitiveCharacter = χ ∧
      ∀ (d : ℕ) (χ' : DirichletCharacter R d), χ'.IsPrimitive →
        ∀ (hd : d ∣ n), changeLevel hd χ' = χ →
          ∃ (hlev : d = χ.conductor), hlev ▸ χ' = χ.primitiveCharacter
Uses 2
Proof usesThe level of a primitive inducer is the conductor · An inducer at the conductor level is the primitive character
13 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.