IdealClassCharacterSum.lean

1 import PaperX.IdealClassQuantitativeTheorem
2 
3 /-!
4 # Actual ideal sums weighted by ordinary ideal classes
5 
6 The sums range over nonzero integral ideals subject to their actual absolute norm.
7 Grouping by the ordinary ideal class is an exact finite identity at every real threshold.
8 -/
9 set_option autoImplicit false
10 noncomputable section
11 
12 open Ideal NumberField
13 open scoped nonZeroDivisors Classical BigOperators
14 
15 namespace PaperX.IdealClassCharacter
16 
17 open PaperX.IdealClassQuantitative
18 
19 variable (K : Type*) [Field K] [NumberField K]
20 
21 /-- The actual set of bounded nonzero integral ideals is finite at every real threshold. -/
22 instance boundedIdeals_finite (X : ℝ) :
23     Finite {I : (Ideal (𝓞 K))⁰ // (absNorm (I : Ideal (𝓞 K)) : ℝ) ≤ X} := by
24   have : Finite {I : (Ideal (𝓞 K))⁰ // absNorm (I : Ideal (𝓞 K)) ≤ ⌊X⌋₊} :=
25     finite_setOfPred_absNorm_le₀ ⌊X⌋₊
26   exact Finite.of_injective
27     (fun I => (⟨I.val, Nat.le_floor I.property⟩ :
28       {I : (Ideal (𝓞 K))⁰ // absNorm (I : Ideal (𝓞 K)) ≤ ⌊X⌋₊}))
29     (fun _ _ h => Subtype.ext (congrArg
30       (fun I : {I : (Ideal (𝓞 K))⁰ // absNorm (I : Ideal (𝓞 K)) ≤ ⌊X⌋₊} => I.val) h))
31 
32 /-- A finite sum over actual ideals, with the coefficient given by the ideal class. -/
33 def weightedSum (w : ClassGroup (𝓞 K) → ℂ) (X : ℝ) : ℂ :=
34   letI := Fintype.ofFinite {I : (Ideal (𝓞 K))⁰ //
35     (absNorm (I : Ideal (𝓞 K)) : ℝ) ≤ X}
36   ∑ I : {I : (Ideal (𝓞 K))⁰ // (absNorm (I : Ideal (𝓞 K)) : ℝ) ≤ X},
37     w (ClassGroup.mk0 I.val)
38 
39 /-- Exact grouping of the ideal sum by ordinary ideal class. -/
40 theorem weightedSum_eq_sum_classCount (w : ClassGroup (𝓞 K) → ℂ) (X : ℝ) :
41     weightedSum K w X = ∑ C, w C * (classCount K C X : ℂ) := by
42   let := Fintype.ofFinite {I : (Ideal (𝓞 K))⁰ //
43     (absNorm (I : Ideal (𝓞 K)) : ℝ) ≤ X}
44   unfold weightedSum
45   rw [← Fintype.sum_fiberwise (fun I : {I : (Ideal (𝓞 K))⁰ //
46     (absNorm (I : Ideal (𝓞 K)) : ℝ) ≤ X} => ClassGroup.mk0 I.val)]
47   apply Finset.sum_congr rfl
48   intro C _
49   have he := Equiv.subtypeSubtypeEquivSubtypeInter
50     (fun I : (Ideal (𝓞 K))⁰ => (absNorm (I : Ideal (𝓞 K)) : ℝ) ≤ X)
51     (fun I => ClassGroup.mk0 I = C)
52   have hc : classCount K C X =
53       Fintype.card {I : {I : (Ideal (𝓞 K))⁰ //
54         (absNorm (I : Ideal (𝓞 K)) : ℝ) ≤ X} // ClassGroup.mk0 I.val = C} := by
55     rw [classCount, ← Nat.card_congr he, Nat.card_eq_fintype_card]
56   simp only [hc]
57   simp_rw [show ∀ I : {I : {I : (Ideal (𝓞 K))⁰ //
58     (absNorm (I : Ideal (𝓞 K)) : ℝ) ≤ X} // ClassGroup.mk0 I.val = C},
59     w (ClassGroup.mk0 I.val.val) = w C from fun I => congrArg w I.property]
60   simp [mul_comm]
61 
62 /-- Every nontrivial complex character of a finite group has zero total sum. -/
63 theorem sum_character_eq_zero {G : Type*} [Group G] [Fintype G]
64     (χ : G →* ℂ) (hχ : χ ≠ 1) : ∑ g, χ g = 0 := by
65   obtain ⟨a, ha⟩ : ∃ a, χ a ≠ 1 := by
66     by_contra h
67     push Not at h
68     exact hχ (MonoidHom.ext fun a => by simpa using h a)
69   have hs : χ a * ∑ g, χ g = ∑ g, χ g := by
70     rw [Finset.mul_sum]
71     simp_rw [← map_mul]
72     exact Fintype.sum_equiv (Equiv.mulLeft a) _ _ (fun _ => rfl)
73   have hz : (χ a - 1) * ∑ g, χ g = 0 := by
74     rw [sub_mul, one_mul, hs, sub_self]
75   exact (mul_eq_zero.mp hz).resolve_left (sub_ne_zero.mpr ha)
76 
77 end PaperX.IdealClassCharacter

Back to source controls