feat(LegendreSymbol/AddCharacter): std add char of ZMod N is primitive (#14495)

The standard additive character of `ZMod N` is a primitive character.

Author: loefflerd

Mathlib.lean

@@ -1252,6 +1252,7 @@ import Mathlib.Analysis.SpecialFunctions.Complex.Analytic
 import Mathlib.Analysis.SpecialFunctions.Complex.Arctan
 import Mathlib.Analysis.SpecialFunctions.Complex.Arg
 import Mathlib.Analysis.SpecialFunctions.Complex.Circle
+import Mathlib.Analysis.SpecialFunctions.Complex.CircleAddChar
 import Mathlib.Analysis.SpecialFunctions.Complex.Log
 import Mathlib.Analysis.SpecialFunctions.Complex.LogBounds
 import Mathlib.Analysis.SpecialFunctions.Complex.LogDeriv

Mathlib/Analysis/Fourier/ZMod.lean

@@ -3,7 +3,7 @@ Copyright (c) 2024 David Loeffler. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: David Loeffler
 -/
-import Mathlib.Analysis.SpecialFunctions.Complex.Circle
+import Mathlib.Analysis.SpecialFunctions.Complex.CircleAddChar
 import Mathlib.Analysis.Fourier.FourierTransform
 import Mathlib.NumberTheory.DirichletCharacter.GaussSum
 

Mathlib/Analysis/SpecialFunctions/Complex/Circle.lean

@@ -3,7 +3,6 @@ Copyright (c) 2021 Yury G. Kudryashov. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Yury G. Kudryashov
 -/
-import Mathlib.Algebra.Group.AddChar
 import Mathlib.Analysis.Complex.Circle
 import Mathlib.Analysis.SpecialFunctions.Complex.Log
 
@@ -155,6 +154,9 @@ theorem toCircle_add (x : AddCircle T) (y : AddCircle T) :
   induction y using QuotientAddGroup.induction_on'
   simp_rw [← coe_add, toCircle_apply_mk, mul_add, expMapCircle_add]
 
+lemma toCircle_zero : toCircle (0 : AddCircle T) = 1 := by
+  rw [← QuotientAddGroup.mk_zero, toCircle_apply_mk, mul_zero, expMapCircle_zero]
+
 theorem continuous_toCircle : Continuous (@toCircle T) :=
   continuous_coinduced_dom.mpr (expMapCircle.continuous.comp <| continuous_const.mul continuous_id')
 
@@ -205,52 +207,3 @@ open AddCircle
 lemma isLocalHomeomorph_expMapCircle : IsLocalHomeomorph expMapCircle := by
   have : Fact (0 < 2 * π) := ⟨by positivity⟩
   exact homeomorphCircle'.isLocalHomeomorph.comp (isLocalHomeomorph_coe (2 * π))
-
-namespace ZMod
-
-/-!
-### Additive characters valued in the complex circle
--/
-
-open scoped Real
-
-variable {N : ℕ} [NeZero N]
-
-/-- The additive character from `ZMod N` to the unit circle in `ℂ`, sending `j mod N` to
-`exp (2 * π * I * j / N)`. -/
-noncomputable def toCircle : AddChar (ZMod N) circle where
-  toFun := fun j ↦ (toAddCircle j).toCircle
-  map_add_eq_mul' a b := by simp_rw [map_add, AddCircle.toCircle_add]
-  map_zero_eq_one' := by simp_rw [map_zero, AddCircle.toCircle, ← QuotientAddGroup.mk_zero,
-    Function.Periodic.lift_coe, mul_zero, expMapCircle_zero]
-
-lemma toCircle_intCast (j : ℤ) :
-    toCircle (j : ZMod N) = exp (2 * π * I * j / N) := by
-  rw [toCircle, AddChar.coe_mk, AddCircle.toCircle, toAddCircle_intCast,
-    Function.Periodic.lift_coe, expMapCircle_apply]
-  push_cast
-  ring_nf
-
-lemma toCircle_natCast (j : ℕ) :
-    toCircle (j : ZMod N) = exp (2 * π * I * j / N) := by
-  simpa using toCircle_intCast (N := N) j
-
-/--
-Explicit formula for `toCircle j`. Note that this is "evil" because it uses `ZMod.val`. Where
-possible, it is recommended to lift `j` to `ℤ` and use `toCircle_intCast` instead.
--/
-lemma toCircle_apply (j : ZMod N) :
-    toCircle j = exp (2 * π * I * j.val / N) := by
-  rw [← toCircle_natCast, natCast_zmod_val]
-
-/-- The additive character from `ZMod N` to `ℂ`, sending `j mod N` to `exp (2 * π * I * j / N)`. -/
-noncomputable def stdAddChar : AddChar (ZMod N) ℂ := circle.subtype.compAddChar toCircle
-
-lemma stdAddChar_coe (j : ℤ) :
-    stdAddChar (j : ZMod N) = exp (2 * π * I * j / N) := by
-  simp only [stdAddChar, MonoidHom.coe_compAddChar, Function.comp_apply,
-    Submonoid.coe_subtype, toCircle_intCast]
-
-lemma stdAddChar_apply (j : ZMod N) : stdAddChar j = ↑(toCircle j) := rfl
-
-end ZMod

Mathlib/Analysis/SpecialFunctions/Complex/CircleAddChar.lean

@@ -0,0 +1,82 @@
+/-
+Copyright (c) 2024 David Loeffler. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: David Loeffler
+-/
+import Mathlib.Analysis.SpecialFunctions.Complex.Circle
+import Mathlib.NumberTheory.LegendreSymbol.AddCharacter
+
+/-!
+# Additive characters valued in the unit circle
+
+This file defines additive characters, valued in the unit circle, from either
+* the ring `ZMod N` for any non-zero natural `N`,
+* the additive circle `ℝ / T ⬝ ℤ`, for any real `T`.
+
+These results are separate from `Analysis.SpecialFunctions.Complex.Circle` in order to reduce
+the imports of that file.
+-/
+
+open Complex Function
+
+open scoped Real
+
+/-- The canonical map from the additive to the multiplicative circle, as an `AddChar`. -/
+noncomputable def AddCircle.toCircle_addChar {T : ℝ} : AddChar (AddCircle T) circle where
+  toFun := toCircle
+  map_zero_eq_one' := toCircle_zero
+  map_add_eq_mul' := toCircle_add
+
+open AddCircle
+
+namespace ZMod
+
+variable {N : ℕ} [NeZero N]
+
+/-- The additive character from `ZMod N` to the unit circle in `ℂ`, sending `j mod N` to
+`exp (2 * π * I * j / N)`. -/
+noncomputable def toCircle : AddChar (ZMod N) circle :=
+  toCircle_addChar.compAddMonoidHom toAddCircle
+
+lemma toCircle_intCast (j : ℤ) :
+    toCircle (j : ZMod N) = exp (2 * π * I * j / N) := by
+  rw [toCircle, AddChar.compAddMonoidHom_apply, toCircle_addChar, AddChar.coe_mk,
+    AddCircle.toCircle, toAddCircle_intCast, Function.Periodic.lift_coe, expMapCircle_apply]
+  push_cast
+  ring_nf
+
+lemma toCircle_natCast (j : ℕ) :
+    toCircle (j : ZMod N) = exp (2 * π * I * j / N) := by
+  simpa using toCircle_intCast (N := N) j
+
+/--
+Explicit formula for `toCircle j`. Note that this is "evil" because it uses `ZMod.val`. Where
+possible, it is recommended to lift `j` to `ℤ` and use `toCircle_intCast` instead.
+-/
+lemma toCircle_apply (j : ZMod N) :
+    toCircle j = exp (2 * π * I * j.val / N) := by
+  rw [← toCircle_natCast, natCast_zmod_val]
+
+lemma injective_toCircle : Injective (toCircle : ZMod N → circle) :=
+  (AddCircle.injective_toCircle one_ne_zero).comp (toAddCircle_injective N)
+
+/-- The additive character from `ZMod N` to `ℂ`, sending `j mod N` to `exp (2 * π * I * j / N)`. -/
+noncomputable def stdAddChar : AddChar (ZMod N) ℂ := circle.subtype.compAddChar toCircle
+
+lemma stdAddChar_coe (j : ℤ) :
+    stdAddChar (j : ZMod N) = exp (2 * π * I * j / N) := by
+  simp only [stdAddChar, MonoidHom.coe_compAddChar, Function.comp_apply,
+    Submonoid.coe_subtype, toCircle_intCast]
+
+lemma stdAddChar_apply (j : ZMod N) : stdAddChar j = ↑(toCircle j) := rfl
+
+lemma injective_stdAddChar : Injective (stdAddChar : AddChar (ZMod N) ℂ) :=
+  Subtype.coe_injective.comp injective_toCircle
+
+/-- The standard additive character `ZMod N → ℂ` is primitive. -/
+lemma isPrimitive_stdAddChar (N : ℕ) [NeZero N] :
+    (stdAddChar (N := N)).IsPrimitive := by
+  refine AddChar.zmod_char_primitive_of_eq_one_only_at_zero _ _ (fun t ht ↦ ?_)
+  rwa [← (stdAddChar (N := N)).map_zero_eq_one, injective_stdAddChar.eq_iff] at ht
+
+end ZMod