Quadratic Dirichlet characters under level changes and products #
Being quadratic is preserved by lifting a Dirichlet character to a multiple of its level, and
reflected by it when the target level is nonzero. Together with the fact that a product of
quadratic multiplicative characters is quadratic (MulChar.IsQuadratic.mul, in
TauCeti.NumberTheory.MulChar.Basic), this shows that the product χ.mul ψ of characters of
different levels, taken at their common level, is quadratic.
Main results #
MulChar.IsQuadratic.changeLevel: lifting a quadratic Dirichlet character to a multiple of its level leaves it quadratic.DirichletCharacter.isQuadratic_changeLevel_iff: at a nonzero target level, a lifted character is quadratic exactly when the original character is quadratic.DirichletCharacter.isQuadratic_mul: the common-level product of two quadratic characters is quadratic.
theorem
MulChar.IsQuadratic.changeLevel
{R : Type u_1}
[CommRing R]
{n m : ℕ}
{χ : DirichletCharacter R n}
(hχ : IsQuadratic χ)
(h : n ∣ m)
:
Lifting a quadratic Dirichlet character to a multiple of its level leaves it quadratic.
@[simp]
theorem
DirichletCharacter.isQuadratic_changeLevel_iff
{R : Type u_1}
[CommRing R]
{n m : ℕ}
[NeZero m]
{χ : DirichletCharacter R n}
(h : n ∣ m)
:
Lifting to a nonzero multiple of the level preserves and reflects being quadratic.
theorem
DirichletCharacter.isQuadratic_mul
{R : Type u_1}
[CommRing R]
{n m : ℕ}
{χ : DirichletCharacter R n}
{ψ : DirichletCharacter R m}
(hχ : MulChar.IsQuadratic χ)
(hψ : MulChar.IsQuadratic ψ)
:
MulChar.IsQuadratic (χ.mul ψ)
The product of two quadratic characters, taken at the least common multiple of their levels, is quadratic.