Dirichlet character conductors

An injective change of coefficient ring preserves the conductor and primitivity of a Dirichlet character. The conductor of a product of Dirichlet characters with pairwise coprime conductors is the product of their conductors. In particular, primitive characters at pairwise coprime levels remain primitive after lifting to the product level and multiplying. This applies to the quadratic characters attached to the prime factors of a fundamental discriminant.

Injective changes of the coefficient ring

theorem DirichletCharacter.factorsThrough_ringHomComp_iff {R : Type u_1} {R' : Type u_2} [CommRing R] [CommRing R'] {n d : ℕ} [NeZero n] (χ : DirichletCharacter R n) (f : R →+* R') (hf : Function.Injective ⇑f) : FactorsThrough (MulChar.ringHomComp χ f) d ↔ χ.FactorsThrough d

Factoring a Dirichlet character through a lower level is unchanged by an injective change of coefficient ring.

theorem DirichletCharacter.conductor_ringHomComp {R : Type u_1} {R' : Type u_2} [CommRing R] [CommRing R'] {n : ℕ} [NeZero n] (χ : DirichletCharacter R n) (f : R →+* R') (hf : Function.Injective ⇑f) : conductor (MulChar.ringHomComp χ f) = χ.conductor

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

theorem DirichletCharacter.isPrimitive_ringHomComp_iff {R : Type u_1} {R' : Type u_2} [CommRing R] [CommRing R'] {n : ℕ} [NeZero n] (χ : DirichletCharacter R n) (f : R →+* R') (hf : Function.Injective ⇑f) : IsPrimitive (MulChar.ringHomComp χ f) ↔ χ.IsPrimitive

An injective change of coefficient ring preserves primitivity of a Dirichlet character.

theorem TauCeti.conductor_mul_eq_mul_of_coprime {R : Type u_1} [CommMonoidWithZero R] {N : ℕ} {χ ψ : DirichletCharacter R N} (hcop : χ.conductor.Coprime ψ.conductor) : (χ * ψ).conductor = χ.conductor * ψ.conductor

Multiplication cannot cancel any conductor factor when the two conductors are coprime.

theorem TauCeti.conductor_prod_eq_prod_of_pairwise_coprime {R : Type u_1} {ι : Type u_2} [CommMonoidWithZero R] {N : ℕ} {s : Finset ι} {χ : ι → DirichletCharacter R N} (hcop : (↑s).Pairwise fun (i j : ι) => (χ i).conductor.Coprime (χ j).conductor) (hlevel : s.Nonempty ∨ N ≠ 0) : (∏ i ∈ s, χ i).conductor = ∏ i ∈ s, (χ i).conductor

The conductor of a finite product is the product of the pairwise coprime conductors, provided the product is nonempty or the level is nonzero.