feat: add API for additive characters (#13389)

This adds some API lemmas for additive characters.
* Name change: `AddChar.primitiveCharFiniteField` to `AddChar.FiniteField.primitiveChar`

We also remove a porting note (`AddChar.PrimitiveAddChar` can be a structure again) and fix a typo in a lemma name from another recent PR.

Author: MichaelStollBayreuth

Mathlib/Algebra/Group/AddChar.lean

@@ -237,6 +237,14 @@ instance instCommGroup : CommGroup (AddChar A M) :=
 
 end fromAddCommGroup
 
+section fromAddGrouptoCommMonoid
+
+/-- The values of an additive character on an additive group are units. -/
+lemma val_isUnit {A M} [AddGroup A] [Monoid M] (φ : AddChar A M) (a : A) : IsUnit (φ a) :=
+  IsUnit.map φ.toMonoidHom <| Group.isUnit (Multiplicative.ofAdd a)
+
+end fromAddGrouptoCommMonoid
+
 section fromAddGrouptoDivisionMonoid
 
 variable {A M : Type*} [AddGroup A] [DivisionMonoid M]

Mathlib/NumberTheory/LegendreSymbol/AddCharacter.lean

@@ -7,6 +7,7 @@ import Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots
 import Mathlib.FieldTheory.Finite.Trace
 import Mathlib.Algebra.Group.AddChar
 import Mathlib.Data.ZMod.Units
+import Mathlib.Analysis.Complex.Polynomial
 
 #align_import number_theory.legendre_symbol.add_character from "leanprover-community/mathlib"@"0723536a0522d24fc2f159a096fb3304bef77472"
 
@@ -47,12 +48,29 @@ section Additive
 -- The domain and target of our additive characters. Now we restrict to a ring in the domain.
 variable {R : Type u} [CommRing R] {R' : Type v} [CommMonoid R']
 
+/-- The values of an additive character on a ring of positive characteristic are roots of unity. -/
+lemma val_mem_rootsOfUnity (φ : AddChar R R') (a : R) (h : 0 < ringChar R) :
+    (φ.val_isUnit a).unit ∈ rootsOfUnity (ringChar R).toPNat' R' := by
+  simp only [mem_rootsOfUnity', IsUnit.unit_spec, Nat.toPNat'_coe, h, ↓reduceIte, ← map_nsmul_pow,
+    nsmul_eq_mul, CharP.cast_eq_zero, zero_mul, map_zero_one]
+
 /-- An additive character is *primitive* iff all its multiplicative shifts by nonzero
 elements are nontrivial. -/
 def IsPrimitive (ψ : AddChar R R') : Prop :=
   ∀ a : R, a ≠ 0 → IsNontrivial (mulShift ψ a)
 #align add_char.is_primitive AddChar.IsPrimitive
 
+/-- The composition of a primitive additive character with an injective mooid homomorphism
+is also primitive. -/
+lemma IsPrimitive.compMulHom_of_isPrimitive {R'' : Type*} [CommMonoid R''] {φ : AddChar R R'}
+    {f : R' →* R''} (hφ : φ.IsPrimitive) (hf : Function.Injective f) :
+    (f.compAddChar φ).IsPrimitive := by
+  intro a a_ne_zero
+  obtain ⟨r, ne_one⟩ := hφ a a_ne_zero
+  rw [mulShift_apply] at ne_one
+  simp only [IsNontrivial, mulShift_apply, f.coe_compAddChar, Function.comp_apply]
+  exact ⟨r, fun H ↦ ne_one <| hf <| f.map_one ▸ H⟩
+
 /-- The map associating to `a : R` the multiplicative shift of `ψ` by `a`
 is injective when `ψ` is primitive. -/
 theorem to_mulShift_inj_of_isPrimitive {ψ : AddChar R R'} (hψ : IsPrimitive ψ) :
@@ -87,33 +105,22 @@ lemma not_isPrimitive_mulShift [Finite R] (e : AddChar R R') {r : R}
   exact ⟨x, h', by simp only [mulShift_mulShift, mul_comm r, h, mulShift_zero, not_ne_iff,
     isNontrivial_iff_ne_trivial]⟩
 
--- Porting note: Using `structure` gives a timeout, see
--- https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/mysterious.20finsupp.20related.20timeout/near/365719262 and
--- https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/mysterious.20finsupp.20related.20timeout
--- In Lean4, `set_option genInjectivity false in` may solve this issue.
--- can't prove that they always exist (referring to providing an `Inhabited` instance)
 /-- Definition for a primitive additive character on a finite ring `R` into a cyclotomic extension
 of a field `R'`. It records which cyclotomic extension it is, the character, and the
 fact that the character is primitive. -/
 -- Porting note(#5171): this linter isn't ported yet.
+-- can't prove that they always exist (referring to providing an `Inhabited` instance)
 -- @[nolint has_nonempty_instance]
-def PrimitiveAddChar (R : Type u) [CommRing R] (R' : Type v) [Field R'] :=
-  Σ n : ℕ+, Σ' char : AddChar R (CyclotomicField n R'), IsPrimitive char
+structure PrimitiveAddChar (R : Type u) [CommRing R] (R' : Type v) [Field R'] where
+  /-- The first projection from `PrimitiveAddChar`, giving the cyclotomic field. -/
+  n : ℕ+
+  /-- The second projection from `PrimitiveAddChar`, giving the character. -/
+  char : AddChar R (CyclotomicField n R')
+  /-- The third projection from `PrimitiveAddChar`, showing that `χ.char` is primitive. -/
+  prim : IsPrimitive char
 #align add_char.primitive_add_char AddChar.PrimitiveAddChar
-
-/-- The first projection from `PrimitiveAddChar`, giving the cyclotomic field. -/
-noncomputable def PrimitiveAddChar.n {R : Type u} [CommRing R] {R' : Type v} [Field R'] :
-    PrimitiveAddChar R R' → ℕ+ := fun χ => χ.1
 #align add_char.primitive_add_char.n AddChar.PrimitiveAddChar.n
-
-/-- The second projection from `PrimitiveAddChar`, giving the character. -/
-noncomputable def PrimitiveAddChar.char {R : Type u} [CommRing R] {R' : Type v} [Field R'] :
-    ∀ χ : PrimitiveAddChar R R', AddChar R (CyclotomicField χ.n R') := fun χ => χ.2.1
 #align add_char.primitive_add_char.char AddChar.PrimitiveAddChar.char
-
-/-- The third projection from `PrimitiveAddChar`, showing that `χ.char` is primitive. -/
-theorem PrimitiveAddChar.prim {R : Type u} [CommRing R] {R' : Type v} [Field R'] :
-    ∀ χ : PrimitiveAddChar R R', IsPrimitive χ.char := fun χ => χ.2.2
 #align add_char.primitive_add_char.prim AddChar.PrimitiveAddChar.prim
 
 /-!
@@ -225,9 +232,10 @@ end Additive
 
 /-- There is a primitive additive character on the finite field `F` if the characteristic
 of the target is different from that of `F`.
+
 We obtain it as the composition of the trace from `F` to `ZMod p` with a primitive
 additive character on `ZMod p`, where `p` is the characteristic of `F`. -/
-noncomputable def primitiveCharFiniteField (F F' : Type*) [Field F] [Finite F] [Field F']
+noncomputable def FiniteField.primitiveChar (F F' : Type*) [Field F] [Finite F] [Field F']
     (h : ringChar F' ≠ ringChar F) : PrimitiveAddChar F F' := by
   let p := ringChar F
   haveI hp : Fact p.Prime := ⟨CharP.char_is_prime F _⟩
@@ -245,13 +253,13 @@ noncomputable def primitiveCharFiniteField (F F' : Type*) [Field F] [Finite F] [
     rw [one_mul] at ha
     exact ⟨a, fun hf => ha <| (ψ.prim.zmod_char_eq_one_iff pp <| Algebra.trace (ZMod p) F a).mp hf⟩
   exact ⟨ψ.n, ψ', hψ'.isPrimitive⟩
-#align add_char.primitive_char_finite_field AddChar.primitiveCharFiniteField
+#align add_char.primitive_char_finite_field AddChar.FiniteField.primitiveChar
+@[deprecated (since := "2024-05-30")] alias primitiveCharFiniteField := FiniteField.primitiveChar
 
 /-!
 ### The sum of all character values
 -/
 
-
 section sum
 
 variable {R : Type*} [AddGroup R] [Fintype R] {R' : Type*} [CommRing R']
@@ -294,4 +302,49 @@ theorem sum_mulShift {R : Type*} [CommRing R] [Fintype R] [DecidableEq R]
     exact mod_cast sum_eq_zero_of_isNontrivial (hψ b h)
 #align add_char.sum_mul_shift AddChar.sum_mulShift
 
+/-!
+### Complex-valued additive characters
+-/
+
+section Ring
+
+variable {R : Type*} [CommRing R]
+
+/-- Post-composing an additive character to `ℂ` with complex conjugation gives the inverse
+character. -/
+lemma starComp_eq_inv (hR : 0 < ringChar R) {φ : AddChar R ℂ} :
+    (starRingEnd ℂ).compAddChar φ = φ⁻¹ := by
+  ext1 a
+  simp only [RingHom.toMonoidHom_eq_coe, MonoidHom.coe_compAddChar, MonoidHom.coe_coe,
+    Function.comp_apply, inv_apply']
+  have H := Complex.norm_eq_one_of_mem_rootsOfUnity <| φ.val_mem_rootsOfUnity a hR
+  exact (Complex.inv_eq_conj H).symm
+
+lemma starComp_apply (hR : 0 < ringChar R) {φ : AddChar R ℂ} (a : R) :
+    (starRingEnd ℂ) (φ a) = φ⁻¹ a := by
+  rw [← starComp_eq_inv hR]
+  rfl
+
+end Ring
+
+section Field
+
+variable (F : Type*) [Field F] [Finite F] [DecidableEq F]
+
+private lemma ringChar_ne : ringChar ℂ ≠ ringChar F := by
+  simpa only [ringChar.eq_zero] using (CharP.ringChar_ne_zero_of_finite F).symm
+
+/--  A primitive additive character on the finite field `F` with values in `ℂ`. -/
+noncomputable def FiniteField.primitiveChar_to_Complex : AddChar F ℂ := by
+  refine MonoidHom.compAddChar ?_ (primitiveChar F ℂ <| ringChar_ne F).char
+  exact (IsCyclotomicExtension.algEquiv ?n ℂ (CyclotomicField ?n ℂ) ℂ : CyclotomicField ?n ℂ →* ℂ)
+
+lemma FiniteField.primitiveChar_to_Complex_isPrimitive :
+    (primitiveChar_to_Complex F).IsPrimitive := by
+  refine IsPrimitive.compMulHom_of_isPrimitive (PrimitiveAddChar.prim _) ?_
+  let nn := (primitiveChar F ℂ <| ringChar_ne F).n
+  exact (IsCyclotomicExtension.algEquiv nn ℂ (CyclotomicField nn ℂ) ℂ).injective
+
+end Field
+
 end AddChar

Mathlib/NumberTheory/LegendreSymbol/GaussSum.lean

@@ -215,7 +215,7 @@ theorem Char.card_pow_card {F : Type*} [Field F] [Fintype F] {F' : Type*} [Field
     (χ (-1) * Fintype.card F) ^ (Fintype.card F' / 2) = χ (Fintype.card F') := by
   obtain ⟨n, hp, hc⟩ := FiniteField.card F (ringChar F)
   obtain ⟨n', hp', hc'⟩ := FiniteField.card F' (ringChar F')
-  let ψ := primitiveCharFiniteField F F' hch₁
+  let ψ := FiniteField.primitiveChar F F' hch₁
   -- Porting note: this was a `let` but then Lean would time out at
   -- unification so it is changed to a `set` and `FF'` is replaced by its
   -- definition before unification

Mathlib/RingTheory/RootsOfUnity/Complex.lean

@@ -188,7 +188,7 @@ theorem IsPrimitiveRoot.arg {n : ℕ} {ζ : ℂ} (h : IsPrimitiveRoot ζ n) (hn
   · exact Nat.cast_pos.mpr hn.bot_lt
 #align is_primitive_root.arg IsPrimitiveRoot.arg
 
-lemma Complex.norm_eq_one_of_mem_rootOfUnity {ζ : ℂˣ} {n : ℕ+} (hζ : ζ ∈ rootsOfUnity n ℂ) :
+lemma Complex.norm_eq_one_of_mem_rootsOfUnity {ζ : ℂˣ} {n : ℕ+} (hζ : ζ ∈ rootsOfUnity n ℂ) :
     ‖(ζ : ℂ)‖ = 1 := by
   refine norm_eq_one_of_pow_eq_one ?_ <| n.ne_zero
   norm_cast