NormResidueRepresentative.lean

1 import PaperX.NormResidueTotientWitness
2 
3 /-!
4 # Coprime inverse-class representatives
5 
6 A multiplicative character on `ZMod m` is nonzero exactly on units.  Hence an
7 inverse-class ideal whose absolute norm is coprime to `m` automatically
8 satisfies the representative nonvanishing hypothesis in the norm-character
9 transfer theorem.
10 -/
11 
12 set_option autoImplicit false
13 noncomputable section
14 
15 open Ideal NumberField
16 open scoped NumberField nonZeroDivisors
17 
18 namespace PaperX.NormResidue
19 
20 /-- Coprimality of an integer with the modulus forces every multiplicative
21 character to be nonzero on its residue class. -/
22 theorem mulChar_natCast_ne_zero_of_coprime (m n : ℕ) (χ : ZMod m →*₀ ℂ)
23     (h : n.Coprime m) : χ (n : ZMod m) ≠ 0 := by
24   exact (((ZMod.isUnit_iff_coprime n m).2 h).map χ).ne_zero
25 
26 end PaperX.NormResidue
27 
28 namespace PaperX.NormResidueLattice
29 
30 open PaperX.IdealClassQuantitative PaperX.IdealNormWeighted PaperX.NormResidue
31 
32 variable (K : Type*) [Field K] [NumberField K]
33 
34 /-- Under the scalar-unit/totient criterion, a coprime inverse-class
35 representative is enough for the actual ideal norm-character power saving.
36 The separate nonvanishing character-value hypothesis has disappeared. -/
37 theorem exists_classNormSum_bound_of_totient_coprime_representative
38     {C : ClassGroup (𝓞 K)} {J : (Ideal (𝓞 K))⁰}
39     (hJ : ClassGroup.mk0 J = C⁻¹)
40     (m : ℕ) (hm : m ≠ 0) (χ : ZMod m →*₀ ℂ)
41     (hχ : χ.toMonoidHom.comp (Units.coeHom (ZMod m)) ≠ 1)
42     (hdeg : (Module.finrank ℚ K).Coprime m.totient)
43     (hJcop : (absNorm (J : Ideal (𝓞 K))).Coprime m) :
44     ∃ B : ℝ, 0 ≤ B ∧ ∀ X : ℝ, 1 ≤ X →
45       ‖classNormSum K C (fun n => χ (n : ZMod m)) X‖ ≤
46         B * X ^ countExponent K := by
47   apply exists_classNormSum_bound_of_totient_coprime K hJ m hm χ hχ hdeg
48   exact mulChar_natCast_ne_zero_of_coprime m _ χ hJcop
49 
50 end PaperX.NormResidueLattice

Back to source controls