English
A Dirichlet character χ at level n can be lifted to level m when n | m by composing χ.toUnitHom with ZMod.unitsMap hm and passing through MulChar.
Русский
Символ Дирихле χ уровня n может быть поднят до уровня m, если n делит m, путём композиции χ.toUnitHom с ZMod.unitsMap hm и прохождения через MulChar.
LaTeX
$$$$ \\text{changeLevel}_{n\\to m}(χ) = \\operatorname{MulChar.ofUnitHom}(χ.toUnitHom \\circ ZMod.unitsMap hm).$$$$
Lean4
/-- A function that modifies the level of a Dirichlet character to some multiple
of its original level. -/
noncomputable def changeLevel {n m : ℕ} (hm : n ∣ m) : DirichletCharacter R n →* DirichletCharacter R m
where
toFun ψ := MulChar.ofUnitHom (ψ.toUnitHom.comp (ZMod.unitsMap hm))
map_one' := by ext; simp
map_mul' ψ₁ ψ₂ := by ext; simp
