Even and odd Dirichlet characters

A Dirichlet character χ of level n is even when χ (-1) = 1 (DirichletCharacter.Even). The even characters form a subgroup of the group of Dirichlet characters of level n: the characters trivial on the subgroup {±1} of (ℤ/nℤ)ˣ. Under the character correspondence for the n-th cyclotomic field it is the subgroup attached to the maximal real subfield.

Main definitions

• TauCeti.DirichletCharacter.evenSubgroup: the subgroup of even Dirichlet characters of level n.

Main statements

• DirichletCharacter.mem_evenSubgroup_iff: membership in evenSubgroup is evenness.
• DirichletCharacter.exists_odd: above level two there is an odd character, when the values have enough roots of unity.
• DirichletCharacter.even_of_le_two: at the levels 1 and 2 every character is even.
• DirichletCharacter.two_mul_card_apply_neg_one_mul_apply_neg_one_eq: if one of two levels exceeds two, exactly half of the pairs of characters at these levels have a given product parity.
• DirichletCharacter.card_apply_neg_one_mul_apply_neg_one_eq_of_le_two: if neither level exceeds two, the only pair of characters has product parity 1.

def TauCeti.DirichletCharacter.evenSubgroup (R : Type u_1) [CommRing R] (n : ℕ) : Subgroup (DirichletCharacter R n)

The subgroup of even Dirichlet characters of level n, those with χ (-1) = 1.

@[simp]

theorem DirichletCharacter.mem_evenSubgroup_iff {R : Type u_1} [CommRing R] {n : ℕ} (χ : DirichletCharacter R n) : χ ∈ TauCeti.DirichletCharacter.evenSubgroup R n ↔ χ.Even

@[simp]

theorem DirichletCharacter.even_inv_iff {R : Type u_1} [CommRing R] {n : ℕ} (χ : DirichletCharacter R n) : χ⁻¹.Even ↔ χ.Even

The parity of an inverse character is unchanged.

theorem DirichletCharacter.exists_odd {R : Type u_1} [CommRing R] {n : ℕ} [IsDomain R] [HasEnoughRootsOfUnity R (Monoid.exponent (ZMod n)ˣ)] (hn : 2 < n) : ∃ (χ : DirichletCharacter R n), χ.Odd

Above level two there is an odd Dirichlet character: since -1 ≠ 1 modulo n, some character separates them, and its value at -1 is then -1.

theorem DirichletCharacter.even_of_le_two {R : Type u_1} [CommRing R] {n : ℕ} [NeZero n] (hn : n ≤ 2) (χ : DirichletCharacter R n) : χ.Even

At the levels 1 and 2 every Dirichlet character is even, since -1 = 1 there.

theorem DirichletCharacter.two_mul_card_apply_neg_one_mul_apply_neg_one_eq {R : Type u_1} [CommRing R] {a b : ℕ} [NeZero a] [NeZero b] [IsDomain R] [NeZero 2] [HasEnoughRootsOfUnity R (Monoid.exponent (ZMod a)ˣ)] [HasEnoughRootsOfUnity R (Monoid.exponent (ZMod b)ˣ)] (hab : 2 < a ∨ 2 < b) {ε : R} (hε : ε = 1 ∨ ε = -1) : 2 * Nat.card { q : DirichletCharacter R a × DirichletCharacter R b // q.1 (-1) * q.2 (-1) = ε } = a.totient * b.totient

If one of two levels exceeds 2, exactly half of the pairs of Dirichlet characters at these levels have a prescribed product parity ε = ±1: multiplying by a pair of parity -1 exchanges the two parities.

theorem DirichletCharacter.card_apply_neg_one_mul_apply_neg_one_eq_of_le_two {R : Type u_1} [CommRing R] {a b : ℕ} [NeZero a] [NeZero b] [HasEnoughRootsOfUnity R (Monoid.exponent (ZMod a)ˣ)] [HasEnoughRootsOfUnity R (Monoid.exponent (ZMod b)ˣ)] [DecidableEq R] (ha : a ≤ 2) (hb : b ≤ 2) (ε : R) : Nat.card { q : DirichletCharacter R a × DirichletCharacter R b // q.1 (-1) * q.2 (-1) = ε } = if ε = 1 then 1 else 0

If neither of two levels exceeds 2, there is a single pair of Dirichlet characters at these levels, and it is even: the pairs of product parity ε number one when ε = 1 and none otherwise.