feat: changeLevel for Dirichlet characters (#7263)

Co-authored-by: Moritz Firsching <firsching@google.com>

Mathlib.lean

@@ -1911,6 +1911,7 @@ import Mathlib.Data.ZMod.Coprime
 import Mathlib.Data.ZMod.Defs
 import Mathlib.Data.ZMod.Parity
 import Mathlib.Data.ZMod.Quotient
+import Mathlib.Data.ZMod.Units
 import Mathlib.Deprecated.Group
 import Mathlib.Deprecated.Ring
 import Mathlib.Deprecated.Subfield

Mathlib/Data/ZMod/Basic.lean

@@ -1162,8 +1162,13 @@ theorem ringHom_eq_of_ker_eq [CommRing R] (f g : R →+* ZMod n)
 #align zmod.ring_hom_eq_of_ker_eq ZMod.ringHom_eq_of_ker_eq
 
 @[simp]
-lemma castHom_self {n : ℕ} : ZMod.castHom dvd_rfl (ZMod n) = RingHom.id (ZMod n) :=
-  RingHom.ext_zmod (ZMod.castHom dvd_rfl (ZMod n)) (RingHom.id (ZMod n))
+lemma castHom_self : ZMod.castHom dvd_rfl (ZMod n) = RingHom.id (ZMod n) :=
+  Subsingleton.elim _ _
+
+@[simp]
+lemma castHom_comp {m d : ℕ} (hm : n ∣ m) (hd : m ∣ d) :
+    (castHom hm (ZMod n)).comp (castHom hd (ZMod m)) = castHom (dvd_trans hm hd) (ZMod n) :=
+  RingHom.ext_zmod _ _
 
 section lift
 

Mathlib/Data/ZMod/Units.lean

@@ -0,0 +1,33 @@
+/-
+Copyright (c) 2023 Moritz Firsching. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Moritz Firsching, Ashvni Narayanan, Michael Stoll
+-/
+import Mathlib.Data.ZMod.Basic
+
+
+/-!
+# Lemmas about units in `ZMod`.
+-/
+
+
+namespace ZMod
+
+variable {n m : ℕ}
+/-- `unitsMap` is a group homomorphism that maps units of `ZMod m` to units of `ZMod n` when `n`
+divides `m`. -/
+def unitsMap (hm : n ∣ m) : (ZMod m)ˣ →* (ZMod n)ˣ := Units.map (castHom hm (ZMod n))
+
+lemma unitsMap_def (hm : n ∣ m) : unitsMap hm = Units.map (castHom hm (ZMod n)) := rfl
+
+lemma unitsMap_comp {d : ℕ} (hm : n ∣ m) (hd : m ∣ d) :
+    (unitsMap hm).comp (unitsMap hd) = unitsMap (dvd_trans hm hd) := by
+  simp only [unitsMap_def]
+  rw [← Units.map_comp]
+  exact congr_arg Units.map <| congr_arg RingHom.toMonoidHom <| castHom_comp hm hd
+
+@[simp]
+lemma unitsMap_self (n : ℕ) : unitsMap (dvd_refl n) = MonoidHom.id _ := by
+  simp [unitsMap, castHom_self]
+
+end ZMod

Mathlib/NumberTheory/DirichletCharacter/Basic.lean

@@ -1,11 +1,13 @@
 /-
 Copyright (c) 2023 Ashvni Narayanan. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Ashvni Narayanan, Moritz Firsching
+Authors: Ashvni Narayanan, Moritz Firsching, Michael Stoll
 -/
 import Mathlib.Algebra.Periodic
+import Mathlib.Data.ZMod.Algebra
 import Mathlib.NumberTheory.LegendreSymbol.MulCharacter
 import Mathlib.Data.ZMod.Algebra
+import Mathlib.Data.ZMod.Units
 
 /-!
 # Dirichlet Characters
@@ -17,10 +19,10 @@ of `toUnitHom χ`, the restriction of `χ` to a group homomorphism `(ZMod n)ˣ 
 Main definitions:
 
 - `DirichletCharacter`: The type representing a Dirichlet character.
+- `changeLevel`: Extend the Dirichlet character χ of level `n` to level `m`, where `n` divides `m`.
 
 ## TODO
 
-- `change_level`: Extend the Dirichlet character χ of level `n` to level `m`, where `n` divides `m`.
 - definition of conductor
 
 ## Tags
@@ -35,18 +37,41 @@ open MulChar
 variable {R : Type} [CommMonoidWithZero R] {n : ℕ} (χ : DirichletCharacter R n)
 
 namespace DirichletCharacter
-lemma toUnitHom_eq_char' {a : ZMod n} (ha : IsUnit a) :
-  χ a = χ.toUnitHom ha.unit := by simp
+lemma toUnitHom_eq_char' {a : ZMod n} (ha : IsUnit a) : χ a = χ.toUnitHom ha.unit := by simp
 
-lemma toUnitHom_eq_iff (ψ : DirichletCharacter R n) :
-  toUnitHom χ = toUnitHom ψ ↔ χ = ψ := by simp
+lemma toUnitHom_eq_iff (ψ : DirichletCharacter R n) : toUnitHom χ = toUnitHom ψ ↔ χ = ψ := by simp
 
-lemma eval_modulus_sub (x : ZMod n) :
-  χ (n - x) = χ (-x) := by simp
+lemma eval_modulus_sub (x : ZMod n) : χ (n - x) = χ (-x) := by simp
 
 lemma periodic {m : ℕ} (hm : n ∣ m) : Function.Periodic χ m := by
   intro a
   rw [← ZMod.nat_cast_zmod_eq_zero_iff_dvd] at hm
   simp only [hm, add_zero]
 
+/-- A function that modifies the level of a Dirichlet character to some multiple
+  of its original level. -/
+noncomputable def changeLevel {R : Type} [CommMonoidWithZero R] {n m : ℕ} (hm : n ∣ m) :
+    DirichletCharacter R n →* DirichletCharacter R m :=
+  { toFun := fun ψ ↦ MulChar.ofUnitHom (ψ.toUnitHom.comp (ZMod.unitsMap hm)),
+    map_one' := by ext; simp,
+    map_mul' := fun ψ₁ ψ₂ ↦ by ext; simp }
+
+lemma changeLevel_def {m : ℕ} (hm : n ∣ m) :
+    changeLevel hm χ = MulChar.ofUnitHom (χ.toUnitHom.comp (ZMod.unitsMap hm)) := rfl
+
+lemma changeLevel_def' {m : ℕ} (hm : n ∣ m) :
+    (changeLevel hm χ).toUnitHom = χ.toUnitHom.comp (ZMod.unitsMap hm) := by
+  simp [changeLevel]
+
+@[simp]
+lemma changeLevel_self : changeLevel (dvd_refl n) χ = χ := by
+  simp [changeLevel, ZMod.unitsMap]
+
+lemma changeLevel_self_toUnitHom : (changeLevel (dvd_refl n) χ).toUnitHom = χ.toUnitHom := by
+  rw [changeLevel_self]
+
+lemma changeLevel_trans {m d : ℕ} (hm : n ∣ m) (hd : m ∣ d) :
+    changeLevel (dvd_trans hm hd) χ = changeLevel hd (changeLevel hm χ) := by
+  simp [changeLevel_def, MonoidHom.comp_assoc, ZMod.unitsMap_comp]
+
 end DirichletCharacter