NormResidueTotientWitness.lean

1 import PaperX.NormResidueScalarPower
2 import PaperX.NormResidueCharacterCounting
3 import Mathlib.Data.Nat.Totient
4 
5 /-!
6 # Totient criterion for automatic norm-residue cancellation
7 
8 The scalar unit group of `ZMod m` has cardinality `φ(m)`.  Thus coprimality of
9 `[K : ℚ]` with `φ(m)` makes the degree power map on scalar units bijective.  A
10 nontrivial scalar-unit character then supplies the residue-unit witness needed
11 by the actual ideal norm-character cancellation theorem.
12 -/
13 
14 set_option autoImplicit false
15 noncomputable section
16 
17 open scoped NumberField nonZeroDivisors
18 open Ideal NumberField
19 
20 namespace PaperX.NormResidue
21 
22 variable (K : Type*) [Field K] [NumberField K]
23 
24 /-- Concrete Euler-totient version of the scalar power witness criterion. -/
25 theorem exists_scalarResidueUnit_witness_of_totient_coprime
26     (m : ℕ) (hm : m ≠ 0) (χ : ZMod m →*₀ ℂ)
27     (hχ : χ.toMonoidHom.comp (Units.coeHom (ZMod m)) ≠ 1)
28     (hdeg : (Module.finrank ℚ K).Coprime m.totient) :
29     ∃ u : (𝓞 K ⧸ modulusIdeal (𝓞 K) m)ˣ,
30       χ (integerQuotientNorm K m (u : 𝓞 K ⧸ modulusIdeal (𝓞 K) m)) ≠ 1 := by
31   let _ : NeZero m := ⟨hm⟩
32   apply exists_scalarResidueUnit_witness_of_card_coprime K m hm χ hχ
33   rw [Nat.card_eq_fintype_card, ZMod.card_units_eq_totient]
34   exact hdeg.symm
35 
36 end PaperX.NormResidue
37 
38 namespace PaperX.NormResidueLattice
39 
40 open PaperX.IdealClassQuantitative PaperX.IdealNormWeighted PaperX.NormResidue
41 
42 variable (K : Type*) [Field K] [NumberField K]
43 
44 /-- The residue-unit witness is eliminated from the class norm-character bound
45 whenever the scalar restriction is nontrivial and the field degree is coprime
46 to `φ(m)`.  The inverse-class representative nonvanishing condition remains
47 explicit. -/
48 theorem exists_classNormSum_bound_of_totient_coprime
49     {C : ClassGroup (𝓞 K)} {J : (Ideal (𝓞 K))⁰}
50     (hJ : ClassGroup.mk0 J = C⁻¹)
51     (m : ℕ) (hm : m ≠ 0) (χ : ZMod m →*₀ ℂ)
52     (hχ : χ.toMonoidHom.comp (Units.coeHom (ZMod m)) ≠ 1)
53     (hdeg : (Module.finrank ℚ K).Coprime m.totient)
54     (hχJ : χ (absNorm (J : Ideal (𝓞 K)) : ZMod m) ≠ 0) :
55     ∃ B : ℝ, 0 ≤ B ∧ ∀ X : ℝ, 1 ≤ X →
56       ‖classNormSum K C (fun n => χ (n : ZMod m)) X‖ ≤
57         B * X ^ countExponent K := by
58   obtain ⟨u, hu⟩ :=
59     exists_scalarResidueUnit_witness_of_totient_coprime K m hm χ hχ hdeg
60   exact exists_classNormSum_bound_of_unit K hJ m hm χ u hu hχJ
61 
62 end PaperX.NormResidueLattice

Back to source controls