feat(AddChar): Additive group structure and double dual embedding (#1…

…5441)

This PR constructs the additive group structure on `AddChar A G` (a copy of its multiplicative group structure) and leverages it to define the double dual embedding as a morphism `A →+ AddChar (AddChar A M) M`.

From LeanAPAP

Mathlib/Algebra/Group/AddChar.lean

@@ -23,6 +23,15 @@ We also include some constructions specific to the case when `A = R` is a ring;
 For more refined results of a number-theoretic nature (primitive characters, Gauss sums, etc)
 see `Mathlib.NumberTheory.LegendreSymbol.AddCharacter`.
 
+# Implementation notes
+
+Due to their role as the dual of an additive group, additive characters must themselves be an
+additive group. This contrasts to their pointwise operations which make them a multiplicative group.
+We simply define both the additive and multiplicative group structures and prove them equal.
+
+For more information on this design decision, see the following zulip thread:
+https://leanprover.zulipchat.com/#narrow/stream/116395-maths/topic/Additive.20characters
+
 ## Tags
 
 additive character
@@ -33,6 +42,8 @@ additive character
 -/
 
 open Function Multiplicative
+open Finset hiding card
+open Fintype (card)
 
 section AddCharDef
 
@@ -171,11 +182,18 @@ lemma coe_toAddMonoidHomEquiv (ψ : AddChar A M) :
 @[simp] lemma toAddMonoidHomEquiv_symm_apply (ψ : A →+ Additive M) (a : A) :
     toAddMonoidHomEquiv.symm ψ a = Additive.toMul (ψ a) := rfl
 
-/-- The trivial additive character (sending everything to `1`) is `(1 : AddChar A M).` -/
+/-- The trivial additive character (sending everything to `1`). -/
 instance instOne : One (AddChar A M) := toMonoidHomEquiv.one
 
+/-- The trivial additive character (sending everything to `1`). -/
+instance instZero : Zero (AddChar A M) := ⟨1⟩
+
 @[simp, norm_cast] lemma coe_one : ⇑(1 : AddChar A M) = 1 := rfl
+@[simp, norm_cast] lemma coe_zero : ⇑(0 : AddChar A M) = 1 := rfl
 @[simp] lemma one_apply (a : A) : (1 : AddChar A M) a = 1 := rfl
+@[simp] lemma zero_apply (a : A) : (0 : AddChar A M) a = 1 := rfl
+
+lemma one_eq_zero : (1 : AddChar A M) = (0 : AddChar A M) := rfl
 
 instance instInhabited : Inhabited (AddChar A M) := ⟨1⟩
 
@@ -220,7 +238,9 @@ lemma compAddMonoidHom_injective_right (ψ : AddChar B M) (hψ : Injective ψ) :
   rw [DFunLike.ext'_iff] at h ⊢; exact hψ.comp_left h
 
 lemma eq_one_iff : ψ = 1 ↔ ∀ x, ψ x = 1 := DFunLike.ext_iff
+lemma eq_zero_iff : ψ = 0 ↔ ∀ x, ψ x = 1 := DFunLike.ext_iff
 lemma ne_one_iff : ψ ≠ 1 ↔ ∃ x, ψ x ≠ 1 := DFunLike.ne_iff
+lemma ne_zero_iff : ψ ≠ 0 ↔ ∃ x, ψ x ≠ 1 := DFunLike.ne_iff
 
 /-- An additive character is *nontrivial* if it takes a value `≠ 1`. -/
 @[deprecated (since := "2024-06-06")]
@@ -236,15 +256,40 @@ end Basic
 
 section toCommMonoid
 
-variable {A M : Type*} [AddMonoid A] [CommMonoid M]
+variable {ι A M : Type*} [AddMonoid A] [CommMonoid M]
 
 /-- When `M` is commutative, `AddChar A M` is a commutative monoid. -/
 instance instCommMonoid : CommMonoid (AddChar A M) := toMonoidHomEquiv.commMonoid
+/-- When `M` is commutative, `AddChar A M` is an additive commutative monoid. -/
+instance instAddCommMonoid : AddCommMonoid (AddChar A M) := Additive.addCommMonoid
 
 @[simp, norm_cast] lemma coe_mul (ψ χ : AddChar A M) : ⇑(ψ * χ) = ψ * χ := rfl
+@[simp, norm_cast] lemma coe_add (ψ χ : AddChar A M) : ⇑(ψ + χ) = ψ * χ := rfl
 @[simp, norm_cast] lemma coe_pow (ψ : AddChar A M) (n : ℕ) : ⇑(ψ ^ n) = ψ ^ n := rfl
-@[simp, norm_cast] lemma mul_apply (ψ φ : AddChar A M) (a : A) : (ψ * φ) a = ψ a * φ a := rfl
-@[simp, norm_cast] lemma pow_apply (ψ : AddChar A M) (n : ℕ) (a : A) : (ψ ^ n) a = (ψ a) ^ n := rfl
+@[simp, norm_cast] lemma coe_nsmul (n : ℕ) (ψ : AddChar A M) : ⇑(n • ψ) = ψ ^ n := rfl
+
+@[simp, norm_cast]
+lemma coe_prod (s : Finset ι) (ψ : ι → AddChar A M) : ∏ i in s, ψ i = ∏ i in s, ⇑(ψ i) := by
+  induction s using Finset.cons_induction <;> simp [*]
+
+@[simp, norm_cast]
+lemma coe_sum (s : Finset ι) (ψ : ι → AddChar A M) : ∑ i in s, ψ i = ∏ i in s, ⇑(ψ i) := by
+  induction s using Finset.cons_induction <;> simp [*]
+
+@[simp] lemma mul_apply (ψ φ : AddChar A M) (a : A) : (ψ * φ) a = ψ a * φ a := rfl
+@[simp] lemma add_apply (ψ φ : AddChar A M) (a : A) : (ψ + φ) a = ψ a * φ a := rfl
+@[simp] lemma pow_apply (ψ : AddChar A M) (n : ℕ) (a : A) : (ψ ^ n) a = (ψ a) ^ n := rfl
+@[simp] lemma nsmul_apply (ψ : AddChar A M) (n : ℕ) (a : A) : (n • ψ) a = (ψ a) ^ n := rfl
+
+lemma prod_apply (s : Finset ι) (ψ : ι → AddChar A M) (a : A) :
+    (∏ i in s, ψ i) a = ∏ i in s, ψ i a := by rw [coe_prod, Finset.prod_apply]
+
+lemma sum_apply (s : Finset ι) (ψ : ι → AddChar A M) (a : A) :
+    (∑ i in s, ψ i) a = ∏ i in s, ψ i a := by rw [coe_sum, Finset.prod_apply]
+
+lemma mul_eq_add (ψ χ : AddChar A M) : ψ * χ = ψ + χ := rfl
+lemma pow_eq_nsmul (ψ : AddChar A M) (n : ℕ) : ψ ^ n = n • ψ := rfl
+lemma prod_eq_sum (s : Finset ι) (ψ : ι → AddChar A M) : ∏ i in s, ψ i = ∑ i in s, ψ i := rfl
 
 /-- The natural equivalence to `(Multiplicative A →* M)` is a monoid isomorphism. -/
 def toMonoidHomMulEquiv : AddChar A M ≃* (Multiplicative A →* M) :=
@@ -255,8 +300,39 @@ def toMonoidHomMulEquiv : AddChar A M ≃* (Multiplicative A →* M) :=
 def toAddMonoidAddEquiv : Additive (AddChar A M) ≃+ (A →+ Additive M) :=
   { toAddMonoidHomEquiv with map_add' := fun φ ψ ↦ by rfl }
 
+/-- The double dual embedding. -/
+def doubleDualEmb : A →+ AddChar (AddChar A M) M where
+  toFun a := { toFun := fun ψ ↦ ψ a
+               map_zero_eq_one' := by simp
+               map_add_eq_mul' := by simp }
+  map_zero' := by ext; simp
+  map_add' _ _ := by ext; simp [map_add_eq_mul]
+
+@[simp] lemma doubleDualEmb_apply (a : A) (ψ : AddChar A M) : doubleDualEmb a ψ = ψ a := rfl
+
 end toCommMonoid
 
+section CommSemiring
+variable {A R : Type*} [AddGroup A] [Fintype A] [CommSemiring R] [IsDomain R]
+  [DecidableEq (AddChar A R)] {ψ : AddChar A R}
+
+lemma sum_eq_ite (ψ : AddChar A R) : ∑ a, ψ a = if ψ = 0 then ↑(card A) else 0 := by
+  split_ifs with h
+  · simp [h, card_univ]
+  obtain ⟨x, hx⟩ := ne_one_iff.1 h
+  refine eq_zero_of_mul_eq_self_left hx ?_
+  rw [Finset.mul_sum]
+  exact Fintype.sum_equiv (Equiv.addLeft x) _ _ fun y ↦ (map_add_eq_mul ..).symm
+
+variable [CharZero R]
+
+lemma sum_eq_zero_iff_ne_zero : ∑ x, ψ x = 0 ↔ ψ ≠ 0 := by
+  rw [sum_eq_ite, Ne.ite_eq_right_iff]; exact Nat.cast_ne_zero.2 Fintype.card_ne_zero
+
+lemma sum_ne_zero_iff_eq_zero : ∑ x, ψ x ≠ 0 ↔ ψ = 0 := sum_eq_zero_iff_ne_zero.not_left
+
+end CommSemiring
+
 /-!
 ## Additive characters of additive abelian groups
 -/
@@ -273,7 +349,13 @@ instance instCommGroup : CommGroup (AddChar A M) :=
     inv := fun ψ ↦ ψ.compAddMonoidHom negAddMonoidHom
     inv_mul_cancel := fun ψ ↦ by ext1 x; simp [negAddMonoidHom, ← map_add_eq_mul]}
 
-@[simp] lemma inv_apply (ψ : AddChar A M) (x : A) : ψ⁻¹ x = ψ (-x) := rfl
+/-- The additive characters on a commutative additive group form a commutative group. -/
+instance : AddCommGroup (AddChar A M) := Additive.addCommGroup
+
+@[simp] lemma inv_apply (ψ : AddChar A M) (a : A) : ψ⁻¹ a = ψ (-a) := rfl
+@[simp] lemma neg_apply (ψ : AddChar A M) (a : A) : (-ψ) a = ψ (-a) := rfl
+@[simp] lemma div_apply (ψ χ : AddChar A M) (a : A) : (ψ / χ) a = ψ a * χ (-a) := rfl
+@[simp] lemma sub_apply (ψ χ : AddChar A M) (a : A) : (ψ - χ) a = ψ a * χ (-a) := rfl
 
 end fromAddCommGroup
 
@@ -307,7 +389,14 @@ section fromAddGrouptoDivisionCommMonoid
 
 variable {A M : Type*} [AddCommGroup A] [DivisionCommMonoid M]
 
-lemma inv_apply' (ψ : AddChar A M) (x : A) : ψ⁻¹ x = (ψ x)⁻¹ := by rw [inv_apply, map_neg_eq_inv]
+lemma inv_apply' (ψ : AddChar A M) (a : A) : ψ⁻¹ a = (ψ a)⁻¹ := by rw [inv_apply, map_neg_eq_inv]
+lemma neg_apply' (ψ : AddChar A M) (a : A) : (-ψ) a = (ψ a)⁻¹ := map_neg_eq_inv _ _
+
+lemma div_apply' (ψ χ : AddChar A M) (a : A) : (ψ / χ) a = ψ a / χ a := by
+  rw [div_apply, map_neg_eq_inv, div_eq_mul_inv]
+
+lemma sub_apply' (ψ χ : AddChar A M) (a : A) : (ψ - χ) a = ψ a / χ a := by
+  rw [sub_apply, map_neg_eq_inv, div_eq_mul_inv]
 
 lemma map_sub_eq_div (ψ : AddChar A M) (a b : A) : ψ (a - b) = ψ a / ψ b :=
   ψ.toMonoidHom.map_div _ _