IdealClassQuantitativeAttachment.lean

1 import Mathlib.NumberTheory.NumberField.Ideal.Asymptotics
2 
3 /-!
4 # Exact attachment of ordinary ideal-class counts to a cone lattice count
5 
6 This file exposes actual ideal and lattice counting identities used by the
7 qualitative theorem in Mathlib. It does not assume or prove a quantitative
8 lattice estimate. The fixed representative is in the inverse ideal class.
9 -/
10 
11 set_option backward.isDefEq.respectTransparency.types false
12 noncomputable section
13 
14 open Ideal
15 open scoped nonZeroDivisors Real Pointwise Classical
16 open NumberField NumberField.InfinitePlace NumberField.mixedEmbedding
17 open NumberField.mixedEmbedding.euclidean NumberField.mixedEmbedding.fundamentalCone
18 open NumberField.Units Submodule
19 
20 namespace PaperX.IdealClassQuantitative
21 
22 variable (K : Type*) [Field K] [NumberField K]
23 
24 /-- The actual number of nonzero integral ideals in a fixed ideal class. -/
25 def classCount (C : ClassGroup (𝓞 K)) (s : ℝ) : ℕ :=
26   Nat.card {I : (Ideal (𝓞 K))⁰ //
27     absNorm (I : Ideal (𝓞 K)) ≤ s ∧ ClassGroup.mk0 I = C}
28 
29 /-- The ordinary fundamental cone truncated by the actual field norm. -/
30 def coneRegion (s : ℝ) : Set (euclidean.mixedSpace K) :=
31   {x | toMixed K x ∈ fundamentalCone K ∧ mixedEmbedding.norm (toMixed K x) ≤ s}
32 
33 /-- The Euclidean image of the lattice of an actual nonzero integral ideal. -/
34 abbrev idealEuclideanLattice (J : (Ideal (𝓞 K))⁰) : Submodule ℤ (euclidean.mixedSpace K) :=
35   ZLattice.comap ℝ (E := mixedSpace K) (F := euclidean.mixedSpace K)
36     (idealLattice K (FractionalIdeal.mk0 K J)) (toMixed K).toLinearMap
37 
38 /-- The actual finite count in the truncated cone and the ideal lattice. -/
39 def latticeCount (J : (Ideal (𝓞 K))⁰) (s : ℝ) : ℕ :=
40   Nat.card (coneRegion K s ∩ idealEuclideanLattice K J : Set (euclidean.mixedSpace K))
41 
42 /-- Multiplication by an inverse-class ideal turns ideals in `C` into principal ideals. -/
43 theorem classCount_eq_principal_count {C : ClassGroup (𝓞 K)}
44     {J : (Ideal (𝓞 K))⁰} (hJ : ClassGroup.mk0 J = C⁻¹) (s : ℝ) :
45     classCount K C s =
46       Nat.card {I : (Ideal (𝓞 K))⁰ // (J : Ideal (𝓞 K)) ∣ I ∧
47         IsPrincipal (I : Ideal (𝓞 K)) ∧
48         absNorm (I : Ideal (𝓞 K)) ≤ s * absNorm (J : Ideal (𝓞 K))} := by
49   unfold classCount
50   simp_rw [← nonZeroDivisors_dvd_iff_dvd_coe]
51   refine Nat.card_congr ?_
52   refine ((Equiv.dvd J).subtypeEquiv fun I ↦ ?_).trans
53     (Equiv.subtypeSubtypeEquivSubtypeInter (fun I : (Ideal (𝓞 K))⁰ ↦ J ∣ I) _)
54   rw [← ClassGroup.mk0_eq_one_iff (SetLike.coe_mem _)]
55   simp_rw [Equiv.dvd_apply, Submonoid.coe_mul, ← Submonoid.mul_def, _root_.map_mul, hJ,
56     inv_mul_eq_one, Nat.cast_mul, mul_comm s, eq_comm, and_comm, and_congr_left_iff]
57   exact fun _ ↦
58     (mul_le_mul_iff_of_pos_left (Nat.cast_pos.mpr (absNorm_pos_of_nonZeroDivisors J))).symm
59 
60 /-- The cone lattice points are precisely the bounded generators in the fundamental cone. -/
61 def coneLatticeEquiv (J : (Ideal (𝓞 K))⁰) (s : ℝ) :
62     (coneRegion K s ∩ idealEuclideanLattice K J : Set (euclidean.mixedSpace K)) ≃
63       {a : idealSet K J // mixedEmbedding.norm (a : mixedSpace K) ≤ s} := by
64   classical
65   unfold coneRegion idealEuclideanLattice
66   rw [ZLattice.coe_comap]
67   refine (((toMixed K).toEquiv.image _).trans (Equiv.subtypeEquivProp ?_)).trans
68     (Equiv.subtypeSubtypeEquivSubtypeInter _ (mixedEmbedding.norm · ≤ s)).symm
69   ext
70   simp_rw [mem_idealSet, Set.mem_image, Set.mem_inter_iff, Set.mem_preimage, SetLike.mem_coe,
71     mem_idealLattice, FractionalIdeal.coe_mk0]
72   constructor
73   · rintro ⟨_, ⟨⟨hx₁, hx₂⟩, _, ⟨x, hx₃, rfl⟩, h⟩, rfl⟩
74     exact ⟨⟨hx₁, x, hx₃, h⟩, hx₂⟩
75   · rintro ⟨⟨hx₁, ⟨x, hx₂, rfl⟩⟩, hx₃⟩
76     exact ⟨(toMixed K).symm (mixedEmbedding K x),
77       ⟨⟨hx₁, hx₃⟩, ⟨(x : K), by simp [hx₂], rfl⟩⟩, rfl⟩
78 
79 /-- The torsion factor is exact, including at negative and zero thresholds. -/
80 theorem latticeCount_eq_classCount_mul_torsion {C : ClassGroup (𝓞 K)}
81     {J : (Ideal (𝓞 K))⁰} (hJ : ClassGroup.mk0 J = C⁻¹) (s : ℝ) :
82     latticeCount K J (s * absNorm (J : Ideal (𝓞 K))) =
83       classCount K C s * torsionOrder K := by
84   unfold latticeCount
85   rw [Nat.card_congr (coneLatticeEquiv K J _), ← card_isPrincipal_dvd_norm_le,
86     classCount_eq_principal_count K hJ]
87 
88 /-- The unit truncation is the actual norm-le-one cone used by Mathlib. -/
89 theorem coneRegion_one : coneRegion K 1 = toMixed K ⁻¹' normLeOne K := by
90   ext x
91   simp [coneRegion]
92 
93 /-- Positive dilation of the unit cone raises the norm threshold by the degree. -/
94 theorem smul_coneRegion_one {t : ℝ} (ht : 0 < t) :
95     t • coneRegion K 1 = coneRegion K (t ^ Module.finrank ℚ K) := by
96   ext x
97   simp_rw [Set.mem_smul_set_iff_inv_smul_mem₀ ht.ne', coneRegion, Set.mem_ofPred_eq,
98     map_smul, mixedEmbedding.norm_smul, abs_of_nonneg (inv_pos.mpr ht).le,
99     inv_pow, inv_mul_le_iff₀ (pow_pos ht _), mul_one, and_congr_left_iff]
100   intro _
101   exact smul_mem_iff_mem (inv_ne_zero ht.ne')
102 
103 end PaperX.IdealClassQuantitative

Back to source controls