IdealResidueUnitActionMean.lean

1 import PaperX.IdealResidueUnitAction
2 import Mathlib.Analysis.Complex.Basic
3 
4 /-! Zero mean on the actual ideal residue quotient, obtained from an actual unit
5 permutation. The unit witness remains explicit. -/
6 set_option autoImplicit false
7 noncomputable section
8 namespace PaperX.IdealResidueUnitAction
9 open Ideal NumberField
10 open PaperX.ResidueLattice PaperX.NormResidue PaperX.NormResidueLattice
11 open scoped nonZeroDivisors BigOperators
12 
13 variable (K : Type*) [Field K] [NumberField K]
14 
15 /-- A unit witness forces the norm-character mean on the actual ideal residues to vanish,
16 including after a fixed sign or other residue multiplier. -/
17 theorem sum_mul_residueNorm_eq_zero (M J : (Ideal (𝓞 K))⁰) (m : ℕ)
18     (hprod : modulusIdeal (𝓞 K) m * (J : Ideal (𝓞 K)) ≤ M)
19     (hM : (M : Ideal (𝓞 K)) ≤ modulusIdeal (𝓞 K) m)
20     [Fintype (IdealResidues K M J)] (χ : ZMod m →* ℂ)
21     (u : (𝓞 K ⧸ modulusIdeal (𝓞 K) m)ˣ)
22     (hu : χ (integerQuotientNorm K m (u : 𝓞 K ⧸ modulusIdeal (𝓞 K) m)) ≠ 1)
23     (s : ZMod m) :
24     ∑ c : IdealResidues K M J, χ (s * residueNorm K M J m hM c) = 0 := by
25   have hs : χ (integerQuotientNorm K m (u : 𝓞 K ⧸ modulusIdeal (𝓞 K) m)) *
26       (∑ c : IdealResidues K M J, χ (s * residueNorm K M J m hM c)) =
27       ∑ c : IdealResidues K M J, χ (s * residueNorm K M J m hM c) := by
28     calc
29       _ = ∑ c : IdealResidues K M J,
30           χ (s * residueNorm K M J m hM (unitPerm K M J m hprod u c)) := by
31         rw [Finset.mul_sum]
32         apply Finset.sum_congr rfl
33         intro c _
34         rw [residueNorm_unitPerm]
35         simp only [map_mul]
36         ring
37       _ = _ := Fintype.sum_equiv (unitPerm K M J m hprod u) _ _ (fun _ => rfl)
38   have hz : (χ (integerQuotientNorm K m (u : 𝓞 K ⧸ modulusIdeal (𝓞 K) m)) - 1) *
39       (∑ c : IdealResidues K M J, χ (s * residueNorm K M J m hM c)) = 0 := by
40     rw [sub_mul, one_mul, hs, sub_self]
41   exact (mul_eq_zero.mp hz).resolve_left (sub_ne_zero.mpr hu)
42 
43 /-- The actual nonzero product ideal mJ for a nonzero integer modulus. -/
44 def modulusTimesIdeal (J : (Ideal (𝓞 K))⁰) (m : ℕ) (hm : m ≠ 0) :
45     (Ideal (𝓞 K))⁰ :=
46   ⟨modulusIdeal (𝓞 K) m * (J : Ideal (𝓞 K)), by
47     rw [mem_nonZeroDivisors_iff_ne_zero]
48     apply mul_ne_zero
49     · change Ideal.span {(m : 𝓞 K)} ≠ ⊥
50       exact fun h => (Nat.cast_ne_zero.mpr hm) (Ideal.span_singleton_eq_bot.mp h)
51     · exact nonZeroDivisors.coe_ne_zero J⟩
52 
53 /-- The product ideal is contained in J. -/
54 theorem modulusTimesIdeal_le (J : (Ideal (𝓞 K))⁰) (m : ℕ) (hm : m ≠ 0) :
55     (modulusTimesIdeal K J m hm : Ideal (𝓞 K)) ≤ J :=
56   Ideal.mul_le_right
57 
58 /-- The product ideal is contained in mO. -/
59 theorem modulusTimesIdeal_le_modulus (J : (Ideal (𝓞 K))⁰) (m : ℕ) (hm : m ≠ 0) :
60     (modulusTimesIdeal K J m hm : Ideal (𝓞 K)) ≤ modulusIdeal (𝓞 K) m :=
61   Ideal.mul_le_left
62 
63 /-- The actual additive quotient J/mJ is finite, with no coprimality condition on J. -/
64 instance modulusTimesIdealResiduesFinite (J : (Ideal (𝓞 K))⁰) (m : ℕ) (hm : m ≠ 0) :
65     Finite (IdealResidues K (modulusTimesIdeal K J m hm) J) :=
66   finite_idealResidues K (modulusTimesIdeal_le K J m hm)
67 
68 /-- Explicit specialization to the actual finite quotient J/mJ. -/
69 theorem sum_modulusTimesIdeal_norm_eq_zero (J : (Ideal (𝓞 K))⁰) (m : ℕ) (hm : m ≠ 0)
70     [Fintype (IdealResidues K (modulusTimesIdeal K J m hm) J)]
71     (χ : ZMod m →* ℂ) (u : (𝓞 K ⧸ modulusIdeal (𝓞 K) m)ˣ)
72     (hu : χ (integerQuotientNorm K m (u : 𝓞 K ⧸ modulusIdeal (𝓞 K) m)) ≠ 1)
73     (s : ZMod m) :
74     ∑ c : IdealResidues K (modulusTimesIdeal K J m hm) J,
75       χ (s * residueNorm K (modulusTimesIdeal K J m hm) J m
76         (modulusTimesIdeal_le_modulus K J m hm) c) = 0 :=
77   sum_mul_residueNorm_eq_zero K (modulusTimesIdeal K J m hm) J m le_rfl
78     (modulusTimesIdeal_le_modulus K J m hm) χ u hu s
79 
80 end PaperX.IdealResidueUnitAction

Back to source controls