Kummer's Criterion and Regular Primes in Lean

2.2. Dirichlet characters🔗

Definition2.2.1
uses 0
Used by 7
Reverse dependency previews
Preview
Definition 2.2.2
Loading preview
Reverse dependency preview content is loaded from the Blueprint HTML cache.
✓L∃∀N

Let N\ge 1 and let R be a commutative ring. A Dirichlet character modulo N with values in R is a multiplicative map \chi : \mathbb{Z}/N\mathbb{Z} \to R which vanishes on non-units.

Lean code for Definition2.2.1●1 definition
  • abbrevdefined in Mathlib/NumberTheory/DirichletCharacter/Basic.lean
    complete
    abbrev DirichletCharacter.{u_1} (R : Type u_1) [CommMonoidWithZero R] (n : ℕ) :
  Type u_1
    abbrev DirichletCharacter.{u_1} (R : Type u_1)
  [CommMonoidWithZero R] (n : ℕ) :
  Type u_1
    The type of Dirichlet characters of level `n`.

When p is prime, the non-trivial characters modulo p are exactly the characters of the cyclic group (\mathbb{Z}/p\mathbb{Z})^\times. In particular they form a cyclic group of order p-1, and every non-trivial character satisfies the orthogonality relation \sum_{a\in \mathbb{Z}/p\mathbb{Z}} \chi(a) = 0.

Definition2.2.2
uses 1used by 1✓L∃∀N

Teichmüller character. The Teichmüller character is the unique character \omega : (\mathbb{Z}/p\mathbb{Z})^\times \longrightarrow \mathbb{Z}_p^\times such that \omega(a)\equiv a\pmod p for every nonzero residue class a. It generates the character group.

Definition 2.2.1

Lean code for Definition2.2.2●1 definition
  • defdefined in BernoulliRegular/BernoulliGeneralized.lean
    complete
    def BernoulliRegular.teichmullerCharQp (p : ℕ) [Fact (Nat.Prime p)] :
  DirichletCharacter ℚ_[p] p
    def BernoulliRegular.teichmullerCharQp (p : ℕ)
  [Fact (Nat.Prime p)] :
  DirichletCharacter ℚ_[p] p
    The `ℚ_[p]`-valued Teichmüller character, obtained by post-composing
the `ℤ_[p]`-valued Teichmüller character with the natural embedding
`ℤ_[p] → ℚ_[p]`.

Thus every Dirichlet character modulo p can be written uniquely as a power \omega^j with 0\le j\le p-2.