NormResidueCharacter.lean

1 import PaperX.NormResidueArithmetic
2 import Mathlib.Analysis.Complex.Basic
3 
4 /-! A unit witness gives zero mean for a pulled-back norm character on the
5 whole finite residue ring. Nontriviality on the codomain alone is not enough:
6 the character must remain nontrivial on the image of a unit. -/
7 
8 set_option autoImplicit false
9 noncomputable section
10 
11 open scoped BigOperators NumberField
12 
13 namespace PaperX.NormResidue
14 
15 /-- Multiplication by a unit permutes every element of a finite monoid,
16 including nonunits. A nontrivial multiplier therefore forces zero total sum. -/
17 theorem sum_norm_character_eq_zero {R S : Type*} [Monoid R] [Fintype R] [Monoid S]
18     (N : R →* S) (χ : S →* ℂ) (u : Rˣ) (hu : χ (N (u : R)) ≠ 1) :
19     ∑ a : R, χ (N a) = 0 := by
20   have hs : χ (N (u : R)) * ∑ a : R, χ (N a) = ∑ a : R, χ (N a) := by
21     rw [Finset.mul_sum]
22     simp_rw [← map_mul χ, ← map_mul N]
23     exact Equiv.sum_comp u.mulLeft (fun a => χ (N a))
24   have hz : (χ (N (u : R)) - 1) * ∑ a : R, χ (N a) = 0 := by
25     rw [sub_mul, one_mul, hs, sub_self]
26   exact (mul_eq_zero.mp hz).resolve_left (sub_ne_zero.mpr hu)
27 
28 /-- A fixed residue multiplier, in particular a fixed norm sign, preserves
29 the zero-mean conclusion. -/
30 theorem sum_mul_norm_character_eq_zero {R S : Type*}
31     [Monoid R] [Fintype R] [Monoid S]
32     (N : R →* S) (χ : S →* ℂ) (u : Rˣ) (hu : χ (N (u : R)) ≠ 1) (c : S) :
33     ∑ a : R, χ (c * N a) = 0 := by
34   simp_rw [map_mul χ]
35   rw [← Finset.mul_sum, sum_norm_character_eq_zero N χ u hu, mul_zero]
36 
37 /-- Nontriviality of the character pulled back to units is exactly the
38 existence of the unit witness used by the cancellation theorem. -/
39 theorem norm_unit_character_ne_one_iff {R S : Type*} [Monoid R] [Monoid S]
40     (N : R →* S) (χ : S →* ℂ) :
41     (χ.comp N).comp (Units.coeHom R) ≠ 1 ↔ ∃ u : Rˣ, χ (N (u : R)) ≠ 1 := by
42   constructor
43   · intro h
44     by_contra hn
45     push Not at hn
46     apply h
47     exact MonoidHom.ext (fun u => by simpa using hn u)
48   · rintro ⟨u, hu⟩ h
49     apply hu
50     exact DFunLike.congr_fun h u
51 
52 variable (K : Type*) [Field K] [NumberField K]
53 
54 /-- Zero mean for the actual determinant norm on the residue ring of integers.
55 The finite enumeration can be obtained from `integer_quotient_finite` for every
56 nonzero modulus. The unit witness remains explicit. -/
57 theorem integerQuotient_sum_character_eq_zero (m : ℕ)
58     [Fintype (𝓞 K ⧸ modulusIdeal (𝓞 K) m)]
59     (χ : ZMod m →*₀ ℂ) (u : (𝓞 K ⧸ modulusIdeal (𝓞 K) m)ˣ)
60     (hu : χ (integerQuotientNorm K m (u : 𝓞 K ⧸ modulusIdeal (𝓞 K) m)) ≠ 1) :
61     ∑ a : 𝓞 K ⧸ modulusIdeal (𝓞 K) m, χ (integerQuotientNorm K m a) = 0 :=
62   sum_norm_character_eq_zero (integerQuotientNorm K m) χ.toMonoidHom u hu
63 
64 /-- The same exact mean cancellation holds after any fixed residue multiplier,
65 so positive and negative norm-sign sectors have the same cancellation input. -/
66 theorem integerQuotient_sum_mul_character_eq_zero (m : ℕ)
67     [Fintype (𝓞 K ⧸ modulusIdeal (𝓞 K) m)]
68     (χ : ZMod m →*₀ ℂ) (u : (𝓞 K ⧸ modulusIdeal (𝓞 K) m)ˣ)
69     (hu : χ (integerQuotientNorm K m (u : 𝓞 K ⧸ modulusIdeal (𝓞 K) m)) ≠ 1)
70     (c : ZMod m) :
71     ∑ a : 𝓞 K ⧸ modulusIdeal (𝓞 K) m, χ (c * integerQuotientNorm K m a) = 0 :=
72   sum_mul_norm_character_eq_zero (integerQuotientNorm K m) χ.toMonoidHom u hu c
73 
74 end PaperX.NormResidue

Back to source controls