IdealNormWeightedAttachment.lean

1 import PaperX.IdealNormFilterAttachment
2 import PaperX.IdealClassCharacterSum
3 import Mathlib.Algebra.BigOperators.Finprod
4 import Mathlib.Data.ZMod.Basic
5 
6 /-! Exact weighted generator-to-ideal attachment. The roots-of-unity factor
7 and the norm of the inverse-class representative are retained explicitly. -/
8 set_option autoImplicit false
9 set_option backward.isDefEq.respectTransparency.types false
10 noncomputable section
11 
12 open Ideal NumberField Submodule
13 open scoped nonZeroDivisors Classical BigOperators
14 open NumberField.mixedEmbedding NumberField.mixedEmbedding.fundamentalCone
15 open NumberField.Units
16 
17 namespace PaperX.IdealNormWeighted
18 
19 open PaperX.IdealNormFilter
20 
21 variable (K : Type*) [Field K] [NumberField K]
22 
23 /-- The actual absolute norm of the principal ideal generated by a cone point. -/
24 def generatorAbsNorm (J : (Ideal (𝓞 K))⁰) (a : idealSet K J) : ℕ :=
25   absNorm (span {(preimageOfMemIntegerSet (idealSetMap K J a) : 𝓞 K)})
26 
27 /-- This integral norm equals the real norm of the represented cone point. -/
28 theorem generatorAbsNorm_cast (J : (Ideal (𝓞 K))⁰) (a : idealSet K J) :
29     (generatorAbsNorm K J a : ℝ) = mixedEmbedding.norm (a : mixedSpace K) := by
30   rw [generatorAbsNorm, ← idealSetPrincipalEquiv_apply_fst]
31   exact idealSetPrincipalEquiv_absNorm K J a
32 
33 /-- Actual nonzero integral ideals in a class, bounded by absolute norm. -/
34 abbrev BoundedClassIdeals (C : ClassGroup (𝓞 K)) (X : ℝ) :=
35   {I : (Ideal (𝓞 K))⁰ // (absNorm (I : Ideal (𝓞 K)) : ℝ) ≤ X ∧ ClassGroup.mk0 I = C}
36 
37 /-- Actual divisible principal ideals, bounded by absolute norm. -/
38 abbrev BoundedPrincipalIdeals (J : (Ideal (𝓞 K))⁰) (Y : ℝ) :=
39   {I : (Ideal (𝓞 K))⁰ // (J : Ideal (𝓞 K)) ∣ I ∧
40     IsPrincipal (I : Ideal (𝓞 K)) ∧ (absNorm (I : Ideal (𝓞 K)) : ℝ) ≤ Y}
41 
42 instance boundedClassIdeals_finite (C : ClassGroup (𝓞 K)) (X : ℝ) :
43     Finite (BoundedClassIdeals K C X) :=
44   Finite.of_injective
45     (fun I => (⟨I.val, I.property.1⟩ :
46       {I : (Ideal (𝓞 K))⁰ // (absNorm (I : Ideal (𝓞 K)) : ℝ) ≤ X}))
47     (fun _ _ h => Subtype.ext (congrArg
48       (fun z : {I : (Ideal (𝓞 K))⁰ // (absNorm (I : Ideal (𝓞 K)) : ℝ) ≤ X} => z.val) h))
49 
50 instance boundedPrincipalIdeals_finite (J : (Ideal (𝓞 K))⁰) (Y : ℝ) :
51     Finite (BoundedPrincipalIdeals K J Y) :=
52   Finite.of_injective
53     (fun I => (⟨I.val, I.property.2.2⟩ :
54       {I : (Ideal (𝓞 K))⁰ // (absNorm (I : Ideal (𝓞 K)) : ℝ) ≤ Y}))
55     (fun _ _ h => Subtype.ext (congrArg
56       (fun z : {I : (Ideal (𝓞 K))⁰ // (absNorm (I : Ideal (𝓞 K)) : ℝ) ≤ Y} => z.val) h))
57 
58 /-- Bounded generator sums have finite domains; no infinite-support convention is used. -/
59 instance boundedGenerators_finite (J : (Ideal (𝓞 K))⁰) (Y : ℝ) :
60     Finite {a : idealSet K J // mixedEmbedding.norm (a : mixedSpace K) ≤ Y} :=
61   Finite.of_injective (idealSetPrincipalFilterEquiv K J (fun y => y ≤ Y))
62     (idealSetPrincipalFilterEquiv K J (fun y => y ≤ Y)).injective
63 
64 /-- Multiplication by the supplied inverse-class ideal is an exact bounded equivalence. -/
65 def classPrincipalEquiv {C : ClassGroup (𝓞 K)} {J : (Ideal (𝓞 K))⁰}
66     (hJ : ClassGroup.mk0 J = C⁻¹) (X : ℝ) :
67     BoundedClassIdeals K C X ≃
68       BoundedPrincipalIdeals K J (X * absNorm (J : Ideal (𝓞 K))) := by
69   let e : BoundedClassIdeals K C X ≃
70       {I : (Ideal (𝓞 K))⁰ // J ∣ I ∧ IsPrincipal (I : Ideal (𝓞 K)) ∧
71         (absNorm (I : Ideal (𝓞 K)) : ℝ) ≤ X * absNorm (J : Ideal (𝓞 K))} := by
72     refine ((Equiv.dvd J).subtypeEquiv fun I => ?_).trans
73       (Equiv.subtypeSubtypeEquivSubtypeInter (fun I : (Ideal (𝓞 K))⁰ => J ∣ I) _)
74     rw [← ClassGroup.mk0_eq_one_iff (SetLike.coe_mem _)]
75     simp_rw [Equiv.dvd_apply, Submonoid.coe_mul, ← Submonoid.mul_def, _root_.map_mul, hJ,
76       inv_mul_eq_one, Nat.cast_mul, mul_comm X, eq_comm, and_comm, and_congr_left_iff]
77     exact fun _ =>
78       (mul_le_mul_iff_of_pos_left (Nat.cast_pos.mpr (absNorm_pos_of_nonZeroDivisors J))).symm
79   exact e.trans (Equiv.subtypeEquivRight fun I => by rw [nonZeroDivisors_dvd_iff_dvd_coe])
80 
81 /-- The bounded equivalence preserves the product norm, not just the cardinality. -/
82 theorem classPrincipalEquiv_absNorm {C : ClassGroup (𝓞 K)} {J : (Ideal (𝓞 K))⁰}
83     (hJ : ClassGroup.mk0 J = C⁻¹) (X : ℝ) (I : BoundedClassIdeals K C X) :
84     absNorm ((classPrincipalEquiv K hJ X I).val : Ideal (𝓞 K)) =
85       absNorm (I.val : Ideal (𝓞 K)) * absNorm (J : Ideal (𝓞 K)) := by
86   change absNorm ((J : Ideal (𝓞 K)) * (I.val : Ideal (𝓞 K))) = _
87   rw [_root_.map_mul, mul_comm]
88 
89 /-- Sum of any absolute-norm weight over the actual bounded generators. -/
90 def boundedGeneratorSum (J : (Ideal (𝓞 K))⁰) (f : ℕ → ℂ) (Y : ℝ) : ℂ :=
91   ∑ᶠ a : {a : idealSet K J // mixedEmbedding.norm (a : mixedSpace K) ≤ Y},
92     f (generatorAbsNorm K J a.val)
93 
94 /-- Sum of any absolute-norm weight over actual bounded ideals in one class. -/
95 def classNormSum (C : ClassGroup (𝓞 K)) (f : ℕ → ℂ) (X : ℝ) : ℂ :=
96   ∑ᶠ I : BoundedClassIdeals K C X, f (absNorm (I.val : Ideal (𝓞 K)))
97 
98 /-- The generator sum has the exact roots-of-unity multiplicity over principal ideals. -/
99 theorem boundedGeneratorSum_eq_principal (J : (Ideal (𝓞 K))⁰) (f : ℕ → ℂ) (Y : ℝ) :
100     boundedGeneratorSum K J f Y = (torsionOrder K : ℂ) *
101       ∑ᶠ I : BoundedPrincipalIdeals K J Y, f (absNorm (I.val : Ideal (𝓞 K))) := by
102   let e := idealSetPrincipalFilterEquiv K J (fun y => y ≤ Y)
103   let := Fintype.ofFinite (BoundedPrincipalIdeals K J Y)
104   let := Fintype.ofFinite (torsion K)
105   have hsum : boundedGeneratorSum K J f Y =
106       ∑ᶠ p : BoundedPrincipalIdeals K J Y × torsion K,
107         f (absNorm (p.1.val : Ideal (𝓞 K))) := by
108     apply finsum_eq_of_bijective e e.bijective
109     intro a
110     rfl
111   rw [hsum, finsum_eq_sum_of_fintype, finsum_eq_sum_of_fintype, Fintype.sum_prod_type]
112   simp only [Finset.sum_const, Finset.card_univ, nsmul_eq_mul]
113   rw [← Finset.mul_sum]
114   congr 1
115   rw [torsionOrder, Nat.card_eq_fintype_card]
116 
117 /-- Exact weighted attachment at every real threshold, with the ideal-norm scaling retained. -/
118 theorem boundedGeneratorSum_eq_classNormSum {C : ClassGroup (𝓞 K)}
119     {J : (Ideal (𝓞 K))⁰} (hJ : ClassGroup.mk0 J = C⁻¹) (f : ℕ → ℂ) (X : ℝ) :
120     boundedGeneratorSum K J f (X * absNorm (J : Ideal (𝓞 K))) =
121       (torsionOrder K : ℂ) *
122         classNormSum K C (fun n => f (n * absNorm (J : Ideal (𝓞 K)))) X := by
123   rw [boundedGeneratorSum_eq_principal]
124   congr 1
125   symm
126   exact finsum_eq_of_bijective (classPrincipalEquiv K hJ X)
127     (classPrincipalEquiv K hJ X).bijective
128     (fun I => congrArg f (classPrincipalEquiv_absNorm K hJ X I).symm)
129 
130 /-- A multiplicative norm-residue character factors out the norm of the
131 inverse-class representative exactly. -/
132 theorem boundedGeneratorSum_character {C : ClassGroup (𝓞 K)}
133     {J : (Ideal (𝓞 K))⁰} (hJ : ClassGroup.mk0 J = C⁻¹)
134     (m : ℕ) (χ : ZMod m →*₀ ℂ) (X : ℝ) :
135     boundedGeneratorSum K J (fun n => χ (n : ZMod m))
136         (X * absNorm (J : Ideal (𝓞 K))) =
137       ((torsionOrder K : ℂ) * χ (absNorm (J : Ideal (𝓞 K)) : ZMod m)) *
138         classNormSum K C (fun n => χ (n : ZMod m)) X := by
139   rw [boundedGeneratorSum_eq_classNormSum K hJ]
140   unfold classNormSum
141   simp_rw [Nat.cast_mul, map_mul]
142   rw [← finsum_mul]
143   ring
144 
145 /-- Recovering the actual ideal character sum requires the representative's
146 character value to be nonzero; this condition is not inferred from nontriviality. -/
147 theorem classNormSum_character_eq_div {C : ClassGroup (𝓞 K)}
148     {J : (Ideal (𝓞 K))⁰} (hJ : ClassGroup.mk0 J = C⁻¹)
149     (m : ℕ) (χ : ZMod m →*₀ ℂ)
150     (hχJ : χ (absNorm (J : Ideal (𝓞 K)) : ZMod m) ≠ 0) (X : ℝ) :
151     classNormSum K C (fun n => χ (n : ZMod m)) X =
152       boundedGeneratorSum K J (fun n => χ (n : ZMod m))
153           (X * absNorm (J : Ideal (𝓞 K))) /
154         ((torsionOrder K : ℂ) * χ (absNorm (J : Ideal (𝓞 K)) : ZMod m)) := by
155   have htor : (torsionOrder K : ℂ) ≠ 0 := Nat.cast_ne_zero.mpr (torsionOrder_ne_zero K)
156   apply (eq_div_iff (mul_ne_zero htor hχJ)).mpr
157   rw [boundedGeneratorSum_character K hJ]
158   ring
159 
160 end PaperX.IdealNormWeighted

Back to source controls