ResidueLatticeIdealPoints.lean

1 import PaperX.ResidueLatticeIdeal
2 
3 /-! The residue fibers count actual algebraic integers, not just coordinates. -/
4 set_option autoImplicit false
5 noncomputable section
6 open Ideal Module
7 open scoped nonZeroDivisors Real Classical Pointwise
8 open NumberField NumberField.mixedEmbedding NumberField.mixedEmbedding.euclidean
9 namespace PaperX.ResidueLattice
10 open PaperX.IdealClassQuantitative
11 variable (K : Type*) [Field K] [NumberField K]
12 
13 /-- The actual Euclidean embedding of an algebraic integer. -/
14 def integerPoint (x : 𝓞 K) : euclidean.mixedSpace K :=
15   (toMixed K).symm (mixedEmbedding K (x : K))
16 
17 /-- Integral membership is faithfully represented by membership in the ideal lattice. -/
18 theorem integerPoint_mem_iff (J : (Ideal (𝓞 K))⁰) (x : 𝓞 K) :
19     integerPoint K x ∈ idealEuclideanLattice K J ↔ x ∈ (J : Ideal (𝓞 K)) := by
20   change toMixed K (integerPoint K x) ∈ idealLattice K (FractionalIdeal.mk0 K J) ↔ _
21   simp only [integerPoint, ContinuousLinearEquiv.apply_symm_apply, mem_idealLattice,
22     FractionalIdeal.coe_mk0]
23   constructor
24   · rintro ⟨y, hy, he⟩
25     obtain ⟨z, hz, rfl⟩ := (FractionalIdeal.mem_coeIdeal _).mp hy
26     have hez : z = x := by
27       apply Subtype.ext
28       exact mixedEmbedding_injective K he
29     exact hez ▸ hz
30   · exact fun hx => ⟨x, FractionalIdeal.mem_coeIdeal_of_mem _ hx, rfl⟩
31 
32 /-- The embedding preserves the additive congruence difference. -/
33 theorem integerPoint_sub (x y : 𝓞 K) :
34     integerPoint K (x - y) = integerPoint K x - integerPoint K y := by
35   simp [integerPoint, map_sub]
36 
37 /-- Faithfulness of the Euclidean embedding. -/
38 theorem integerPoint_injective : Function.Injective (integerPoint K) := by
39   intro x y h
40   apply Subtype.ext
41   apply mixedEmbedding_injective K
42   exact (toMixed K).symm.injective h
43 
44 /-- Every point in the actual integral ideal lattice comes from a unique integer of that ideal. -/
45 def idealPointEquiv (J : (Ideal (𝓞 K))⁰) :
46     (J : Ideal (𝓞 K)) ≃ idealEuclideanLattice K J :=
47   Equiv.ofBijective (fun x => ⟨integerPoint K x.1, (integerPoint_mem_iff K J x.1).mpr x.2⟩)
48     ⟨fun x y h => Subtype.ext (integerPoint_injective K (congrArg Subtype.val h)), by
49       intro x
50       have hx := x.2
51       change toMixed K x.1 ∈ idealLattice K (FractionalIdeal.mk0 K J) at hx
52       rw [mem_idealLattice, FractionalIdeal.coe_mk0] at hx
53       obtain ⟨y, hy, he⟩ := hx
54       obtain ⟨z, hz, rfl⟩ := (FractionalIdeal.mem_coeIdeal _).mp hy
55       refine ⟨⟨z, hz⟩, ?_⟩
56       apply Subtype.ext
57       change (toMixed K).symm (mixedEmbedding K (z : K)) = x.1
58       rw [he, ContinuousLinearEquiv.symm_apply_apply]⟩
59 
60 /-- A residue equality in the lattice is exactly congruence of algebraic integers modulo the ideal. -/
61 theorem idealPoint_residue_eq_iff (M J : (Ideal (𝓞 K))⁰) (x a : (J : Ideal (𝓞 K))) :
62     (Submodule.Quotient.mk (idealPointEquiv K J x) : IdealResidues K M J) =
63       Submodule.Quotient.mk (idealPointEquiv K J a) ↔
64         (x.1 - a.1) ∈ (M : Ideal (𝓞 K)) := by
65   rw [residue_eq_iff]
66   change integerPoint K x.1 - integerPoint K a.1 ∈ idealEuclideanLattice K M ↔ _
67   rw [← integerPoint_sub, integerPoint_mem_iff]
68 
69 /-- The fiber count is exactly the count of algebraic integers in a prescribed ideal congruence. -/
70 theorem idealFiberCount_eq_integer_count (M J : (Ideal (𝓞 K))⁰)
71     (a : (J : Ideal (𝓞 K))) (t : ℝ) :
72     idealFiberCount K M J (Submodule.Quotient.mk (idealPointEquiv K J a)) t =
73       Nat.card {x : (J : Ideal (𝓞 K)) // x.1 - a.1 ∈ (M : Ideal (𝓞 K)) ∧
74         integerPoint K x.1 ∈ t • coneRegion K 1} := by
75   unfold idealFiberCount fiberCount
76   exact Nat.card_congr ((idealPointEquiv K J).subtypeEquiv (fun x => by
77     simp only [idealPoint_residue_eq_iff]
78     rfl)).symm
79 
80 end PaperX.ResidueLattice

Back to source controls