Conductors of groups of Dirichlet characters

The conductor of a finite group of Dirichlet characters is the least common multiple of the conductors of its members. At a nonzero original level, its divisibility characterization says that among divisors of the original level it is the least level, in the divisibility order, through which every character in the group factors.

This file provides the divisibility characterization of the group conductor, its monotonicity, its value on a cyclic character group, and its invariance under an injective change of coefficient ring. The last result lets integer-valued quadratic character groups be used inside the complex-valued character correspondence for cyclotomic fields.

Main results

• Subgroup.dirichletConductor_dvd_iff: the group conductor divides m exactly when every member's conductor divides m.
• Subgroup.dirichletConductor_dvd_iff_forall_factorsThrough: at a divisor of the original level, this means that every member factors through that level.
• Subgroup.dirichletConductor_sup: the conductor of the supremum of two finite character groups is the least common multiple of their conductors.
• Subgroup.dirichletConductor_closure_singleton: a cyclic character group has the conductor of its generator.
• Subgroup.dirichletConductor_map_ringHomComp: injectively changing the coefficient ring preserves the group conductor.

noncomputable def Subgroup.dirichletConductor {R : Type u_1} [CommMonoidWithZero R] {n : ℕ} (Y : Subgroup (DirichletCharacter R n)) [Finite ↥Y] : ℕ

The conductor of a subgroup of Dirichlet characters: the least common multiple of the conductors of all its members.

theorem Subgroup.conductor_dvd_dirichletConductor {R : Type u_1} [CommMonoidWithZero R] {n : ℕ} (Y : Subgroup (DirichletCharacter R n)) [Finite ↥Y] {χ : DirichletCharacter R n} (hχ : χ ∈ Y) : χ.conductor ∣ Y.dirichletConductor

The conductor of every character in a subgroup divides the subgroup conductor.

@[simp]

theorem Subgroup.dirichletConductor_dvd_iff {R : Type u_1} [CommMonoidWithZero R] {n : ℕ} (Y : Subgroup (DirichletCharacter R n)) [Finite ↥Y] {m : ℕ} : Y.dirichletConductor ∣ m ↔ ∀ χ ∈ Y, χ.conductor ∣ m

A subgroup conductor divides m exactly when every character in the subgroup has conductor dividing m.

theorem Subgroup.dirichletConductor_dvd_level {R : Type u_1} [CommMonoidWithZero R] {n : ℕ} (Y : Subgroup (DirichletCharacter R n)) [Finite ↥Y] : Y.dirichletConductor ∣ n

The conductor of a subgroup of level-n characters divides n.

theorem Subgroup.dirichletConductor_ne_zero {R : Type u_1} [CommMonoidWithZero R] {n : ℕ} [NeZero n] (Y : Subgroup (DirichletCharacter R n)) [Finite ↥Y] : Y.dirichletConductor ≠ 0

The conductor of a subgroup at a nonzero level is nonzero.

theorem Subgroup.dirichletConductor_dvd_iff_forall_factorsThrough {R : Type u_1} [CommMonoidWithZero R] {n : ℕ} [NeZero n] (Y : Subgroup (DirichletCharacter R n)) [Finite ↥Y] {m : ℕ} (hmn : m ∣ n) : Y.dirichletConductor ∣ m ↔ ∀ χ ∈ Y, χ.FactorsThrough m

If m divides the original level, the subgroup conductor divides m exactly when every character in the subgroup factors through level m.

theorem Subgroup.dirichletConductor_dvd_of_le {R : Type u_1} [CommMonoidWithZero R] {n : ℕ} {Y Z : Subgroup (DirichletCharacter R n)} [Finite ↥Y] [Finite ↥Z] (hYZ : Y ≤ Z) : Y.dirichletConductor ∣ Z.dirichletConductor

Group conductors are monotone for subgroup inclusion, in the divisibility order.

theorem Subgroup.finite_sup {R : Type u_1} [CommMonoidWithZero R] {n : ℕ} {Y Z : Subgroup (DirichletCharacter R n)} [Finite ↥Y] [Finite ↥Z] : Finite ↥(Y ⊔ Z)

@[simp]

theorem Subgroup.dirichletConductor_sup {R : Type u_1} [CommMonoidWithZero R] {n : ℕ} (Y Z : Subgroup (DirichletCharacter R n)) [Finite ↥Y] [Finite ↥Z] : (Y ⊔ Z).dirichletConductor = Y.dirichletConductor.lcm Z.dirichletConductor

The conductor of the supremum of two finite character groups is the least common multiple of their conductors.

@[simp]

theorem Subgroup.dirichletConductor_bot {R : Type u_1} [CommMonoidWithZero R] {n : ℕ} [NeZero n] : ⊥.dirichletConductor = 1

The trivial character group has conductor one.

theorem Subgroup.finite_closure_singleton {R : Type u_1} [CommMonoidWithZero R] {n : ℕ} {χ : DirichletCharacter R n} : Finite ↥(closure {χ})

@[simp]

theorem Subgroup.dirichletConductor_closure_singleton {R : Type u_1} [CommMonoidWithZero R] {n : ℕ} (χ : DirichletCharacter R n) : (closure {χ}).dirichletConductor = χ.conductor

The subgroup generated by one Dirichlet character has the conductor of that character.

theorem Subgroup.finite_map {R : Type u_1} {R' : Type u_2} [CommRing R] [CommRing R'] {n : ℕ} {Y : Subgroup (DirichletCharacter R n)} [Finite ↥Y] {f : R →+* R'} : Finite ↥(map (MulChar.ringHomCompHom f) Y)

theorem Subgroup.dirichletConductor_map_ringHomComp {R : Type u_1} {R' : Type u_2} [CommRing R] [CommRing R'] {n : ℕ} (Y : Subgroup (DirichletCharacter R n)) [Finite ↥Y] (f : R →+* R') (hf : Function.Injective ⇑f) : (map (MulChar.ringHomCompHom f) Y).dirichletConductor = Y.dirichletConductor

An injective change of coefficient ring preserves the conductor of a character subgroup.