ResidueLatticeIdeal.lean

1 import PaperX.ResidueLatticeFibers
2 import PaperX.IdealClassQuantitativeGeometry
3 
4 /-! Uniform actual additive-residue counts inside integral ideal lattices. -/
5 set_option autoImplicit false
6 noncomputable section
7 open Ideal MeasureTheory Module
8 open scoped nonZeroDivisors Real Classical Pointwise
9 open NumberField NumberField.mixedEmbedding NumberField.mixedEmbedding.euclidean
10 namespace PaperX.ResidueLattice
11 open PaperX.IdealClassQuantitative
12 
13 variable (K : Type*) [Field K] [NumberField K]
14 
15 /-- Inclusion of integral ideals gives the same inclusion of their actual Euclidean lattices. -/
16 theorem idealLattice_mono {M J : (Ideal (𝓞 K))⁰} (h : (M : Ideal (𝓞 K)) ≤ J) :
17     idealEuclideanLattice K M ≤ idealEuclideanLattice K J := by
18   intro x hx
19   change toMixed K x ∈ idealLattice K (FractionalIdeal.mk0 K J)
20   change toMixed K x ∈ idealLattice K (FractionalIdeal.mk0 K M) at hx
21   rw [mem_idealLattice] at hx ⊢
22   obtain ⟨a, ha, he⟩ := hx
23   refine ⟨a, ?_, he⟩
24   rw [FractionalIdeal.coe_mk0] at ha ⊢
25   obtain ⟨y, hy, rfl⟩ := (FractionalIdeal.mem_coeIdeal _).mp ha
26   exact FractionalIdeal.mem_coeIdeal_of_mem _ (h hy)
27 
28 /-- The actual finite additive quotient for two integral ideal lattices. -/
29 abbrev IdealResidues (M J : (Ideal (𝓞 K))⁰) :=
30   Residues (idealEuclideanLattice K M) (idealEuclideanLattice K J)
31 
32 /-- The exact count of lattice points in one additive residue of the unit fundamental cone. -/
33 def idealFiberCount (M J : (Ideal (𝓞 K))⁰) (c : IdealResidues K M J) (t : ℝ) : ℕ :=
34   fiberCount (idealEuclideanLattice K M) (idealEuclideanLattice K J) (coneRegion K 1) c t
35 
36 /-- The residue space for an inclusion of nonzero integral ideals is finite. -/
37 theorem finite_idealResidues {M J : (Ideal (𝓞 K))⁰} (h : (M : Ideal (𝓞 K)) ≤ J) :
38     Finite (IdealResidues K M J) :=
39   finite_residues _ _ (idealLattice_mono K h)
40 
41 /-- Every actual residue of one nonzero ideal modulo another has a common surface-order estimate.
42 All geometric and lattice hypotheses are supplied internally for the actual number field. -/
43 theorem exists_idealFiber_bound {M J : (Ideal (𝓞 K))⁰} (h : (M : Ideal (𝓞 K)) ≤ J) :
44     ∃ B : ℝ, 0 ≤ B ∧ ∀ (c : IdealResidues K M J) (t : ℝ), 1 ≤ t →
45       |(idealFiberCount K M J c t : ℝ) -
46         t ^ Module.finrank ℚ K * (latticeDensity K J / Nat.card (IdealResidues K M J))| ≤
47         B * (t ^ (Module.finrank ℚ K - 1) + 1) := by
48   let b := Module.Free.chooseBasis ℤ (idealEuclideanLattice K M)
49   obtain ⟨A⟩ := ideal_cone_boundaryAtlas K M b
50   obtain ⟨B, hB0, hB⟩ := exists_fiber_discrepancy_bound
51     (idealEuclideanLattice K M) (idealEuclideanLattice K J) (idealLattice_mono K h) b
52     (coneRegion_one_measurable K) (coneRegion_one_bounded K) A
53   refine ⟨B, hB0, fun c t ht => ?_⟩
54   simpa only [ideal_basis_card K b, idealFiberCount, latticeDensity] using hB c t ht
55 
56 end PaperX.ResidueLattice

Back to source controls