[Merged by Bors] - feat: changeLevel for Dirichlet characters

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,9 +1162,15 @@ 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) :=
+lemma castHom_self : ZMod.castHom dvd_rfl (ZMod n) = RingHom.id (ZMod n) :=
   RingHom.ext_zmod (ZMod.castHom dvd_rfl (ZMod n)) (RingHom.id (ZMod n))
 
+@[simp]
+lemma castHom_comp {m d : ℕ} (hm : n ∣ m) (hd : m ∣ d) :
+    (ZMod.castHom hm (ZMod n)).comp (ZMod.castHom hd (ZMod m)) =
+    ZMod.castHom (dvd_trans hm hd) (ZMod n) :=
+  RingHom.ext_zmod _ _
+
 section lift
 
 variable (n) {A : Type*} [AddGroup A]

Mathlib/Data/ZMod/Units.lean

@@ -0,0 +1,23 @@
+/-
+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 (ZMod.castHom hm (ZMod n))
+
+lemma unitsMap_def (hm : n ∣ m) : ZMod.unitsMap hm = Units.map (ZMod.castHom hm (ZMod n)) := rfl
+
+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.
+- `change_level`: 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
@@ -49,4 +51,38 @@ lemma periodic {m : ℕ} (hm : n ∣ m) : Function.Periodic χ m := by
   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 change_level {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 change_level_def {m : ℕ} (hm : n ∣ m) :
+    change_level hm χ = MulChar.ofUnitHom (χ.toUnitHom.comp (ZMod.unitsMap hm)) := rfl
+
+lemma change_level_def' {m : ℕ} (hm : n ∣ m) :
+    (change_level hm χ).toUnitHom = χ.toUnitHom.comp (Units.map (ZMod.castHom hm (ZMod n))) := by
+  ext
+  rw [change_level_def, ZMod.unitsMap_def]
+  simp
+
+@[simp]
+lemma change_level_self : change_level (dvd_refl n) χ = χ := by
+  ext
+  rw [change_level_def]
+  simp [ZMod.unitsMap]
+
+lemma change_level_self_toUnitHom : (change_level (dvd_refl n) χ).toUnitHom = χ.toUnitHom := by
+  rw [change_level_self]
+
+lemma change_level_trans {m d : ℕ} (hm : n ∣ m) (hd : m ∣ d) :
+  change_level (dvd_trans hm hd) χ = change_level hd (change_level hm χ) := by
+  simp only [change_level_def, toUnitHom_eq, ZMod.unitsMap, ofUnitHom_eq, Equiv.apply_symm_apply]
+  rw [MonoidHom.comp_assoc, ←Units.map_comp]
+  congr
+  rw [← ZMod.castHom_comp hm hd]
+  rfl
+
 end DirichletCharacter