IdealNormFilterAttachment.lean

1 import PaperX.IdealClassQuantitativeAttachment
2 
3 /-!
4 # Exact norm-filtered generator and ideal counts
5 
6 Arbitrary conditions on the actual absolute norm survive the generator-to-ideal
7 correspondence. The roots-of-unity multiplicity is retained exactly.
8 -/
9 set_option autoImplicit false
10 set_option backward.isDefEq.respectTransparency.types false
11 noncomputable section
12 
13 open Ideal NumberField Submodule
14 open scoped nonZeroDivisors Classical
15 open NumberField.mixedEmbedding NumberField.mixedEmbedding.fundamentalCone
16 open NumberField.Units
17 
18 namespace PaperX.IdealNormFilter
19 
20 open PaperX.IdealClassQuantitative
21 
22 variable (K : Type*) [Field K] [NumberField K]
23 
24 /-- Generators in the actual ideal cone correspond to divisible principal ideals
25 and a roots-of-unity coordinate. -/
26 def idealSetPrincipalEquiv (J : (Ideal (𝓞 K))⁰) :
27     idealSet K J ≃
28       {I : (Ideal (𝓞 K))⁰ // (J : Ideal (𝓞 K)) ∣ I ∧
29         IsPrincipal (I : Ideal (𝓞 K))} × torsion K :=
30   calc
31     _ ≃ {a : integerSet K // (preimageOfMemIntegerSet a : 𝓞 K) ∈ (J : Ideal (𝓞 K))} :=
32       idealSetEquiv K J
33     _ ≃ {I : {I : (Ideal (𝓞 K))⁰ // IsPrincipal I.val} × torsion K //
34         (J : Ideal (𝓞 K)) ∣ I.1.val} :=
35       Equiv.subtypeEquiv (integerSetEquiv K) fun a => by
36         rw [integerSetEquiv_apply_fst, dvd_span_singleton]
37     _ ≃ {I : {I : (Ideal (𝓞 K))⁰ // IsPrincipal I.val} //
38         (J : Ideal (𝓞 K)) ∣ I.val} × torsion K :=
39       Equiv.prodSubtypeFstEquivSubtypeProd
40         (p := fun I : {I : (Ideal (𝓞 K))⁰ // IsPrincipal I.val} =>
41           (J : Ideal (𝓞 K)) ∣ I.val)
42     _ ≃ {I : (Ideal (𝓞 K))⁰ //
43         (J : Ideal (𝓞 K)) ∣ I ∧ IsPrincipal (I : Ideal (𝓞 K))} × torsion K :=
44       Equiv.prodCongrLeft fun _ =>
45         (Equiv.subtypeSubtypeEquivSubtypeInter
46           (fun I : (Ideal (𝓞 K))⁰ => IsPrincipal (I : Ideal (𝓞 K)))
47           (fun I => (J : Ideal (𝓞 K)) ∣ I)).trans
48           (Equiv.subtypeEquivRight fun _ => and_comm)
49 
50 /-- The principal ideal is generated by the represented integral element. -/
51 theorem idealSetPrincipalEquiv_apply_fst (J : (Ideal (𝓞 K))⁰) (a : idealSet K J) :
52     ((idealSetPrincipalEquiv K J a).1 : Ideal (𝓞 K)) =
53       span {(preimageOfMemIntegerSet (idealSetMap K J a) : 𝓞 K)} := rfl
54 
55 /-- The correspondence preserves the actual absolute norm. -/
56 theorem idealSetPrincipalEquiv_absNorm (J : (Ideal (𝓞 K))⁰) (a : idealSet K J) :
57     (absNorm ((idealSetPrincipalEquiv K J a).1 : Ideal (𝓞 K)) : ℝ) =
58       mixedEmbedding.norm (a : mixedSpace K) := by
59   rw [idealSetPrincipalEquiv_apply_fst, absNorm_span_singleton, ← intNorm,
60     intNorm_coe, idealSetMap_apply]
61 
62 /-- Restricting by any norm predicate retains the full torsion coordinate. -/
63 def idealSetPrincipalFilterEquiv (J : (Ideal (𝓞 K))⁰) (P : ℝ → Prop) :
64     {a : idealSet K J // P (mixedEmbedding.norm (a : mixedSpace K))} ≃
65       {I : (Ideal (𝓞 K))⁰ // (J : Ideal (𝓞 K)) ∣ I ∧
66         IsPrincipal (I : Ideal (𝓞 K)) ∧ P (absNorm (I : Ideal (𝓞 K)))} × torsion K :=
67   calc
68     _ ≃ {I : {I : (Ideal (𝓞 K))⁰ // (J : Ideal (𝓞 K)) ∣ I ∧
69         IsPrincipal (I : Ideal (𝓞 K))} × torsion K //
70         P (absNorm (I.1 : Ideal (𝓞 K)))} :=
71       Equiv.subtypeEquiv (idealSetPrincipalEquiv K J) fun a => by
72         rw [idealSetPrincipalEquiv_absNorm]
73     _ ≃ {I : {I : (Ideal (𝓞 K))⁰ // (J : Ideal (𝓞 K)) ∣ I ∧
74         IsPrincipal (I : Ideal (𝓞 K))} //
75         P (absNorm (I : Ideal (𝓞 K)))} × torsion K :=
76       Equiv.prodSubtypeFstEquivSubtypeProd
77         (p := fun I : {I : (Ideal (𝓞 K))⁰ // (J : Ideal (𝓞 K)) ∣ I ∧
78           IsPrincipal (I : Ideal (𝓞 K))} => P (absNorm (I : Ideal (𝓞 K))))
79     _ ≃ {I : (Ideal (𝓞 K))⁰ // (J : Ideal (𝓞 K)) ∣ I ∧
80         IsPrincipal (I : Ideal (𝓞 K)) ∧ P (absNorm (I : Ideal (𝓞 K)))} × torsion K :=
81       Equiv.prodCongrLeft fun _ =>
82         (Equiv.subtypeSubtypeEquivSubtypeInter
83           (fun I : (Ideal (𝓞 K))⁰ => (J : Ideal (𝓞 K)) ∣ I ∧
84             IsPrincipal (I : Ideal (𝓞 K)))
85           (fun I => P (absNorm (I : Ideal (𝓞 K))))).trans
86           (Equiv.subtypeEquivRight fun _ => and_assoc)
87 
88 /-- Exact cardinality for an arbitrary norm filter, without finiteness assumptions. -/
89 theorem card_generators_eq_filtered_principal_mul_torsion
90     (J : (Ideal (𝓞 K))⁰) (P : ℝ → Prop) :
91     Nat.card {a : idealSet K J // P (mixedEmbedding.norm (a : mixedSpace K))} =
92       Nat.card {I : (Ideal (𝓞 K))⁰ // (J : Ideal (𝓞 K)) ∣ I ∧
93         IsPrincipal (I : Ideal (𝓞 K)) ∧ P (absNorm (I : Ideal (𝓞 K)))} * torsionOrder K := by
94   rw [Nat.card_congr (idealSetPrincipalFilterEquiv K J P), Nat.card_prod, torsionOrder]
95 
96 /-- Multiplication by an inverse-class ideal preserves any predicate on product norm. -/
97 theorem filtered_class_eq_filtered_principal {C : ClassGroup (𝓞 K)}
98     {J : (Ideal (𝓞 K))⁰} (hJ : ClassGroup.mk0 J = C⁻¹) (P : ℝ → Prop) :
99     Nat.card {I : (Ideal (𝓞 K))⁰ // ClassGroup.mk0 I = C ∧
100       P ((absNorm (I : Ideal (𝓞 K)) : ℝ) * absNorm (J : Ideal (𝓞 K)))} =
101     Nat.card {I : (Ideal (𝓞 K))⁰ // (J : Ideal (𝓞 K)) ∣ I ∧
102       IsPrincipal (I : Ideal (𝓞 K)) ∧ P (absNorm (I : Ideal (𝓞 K)))} := by
103   simp_rw [← nonZeroDivisors_dvd_iff_dvd_coe]
104   refine Nat.card_congr ?_
105   refine ((Equiv.dvd J).subtypeEquiv fun I => ?_).trans
106     (Equiv.subtypeSubtypeEquivSubtypeInter (fun I : (Ideal (𝓞 K))⁰ => J ∣ I) _)
107   rw [← ClassGroup.mk0_eq_one_iff (SetLike.coe_mem _)]
108   simp_rw [Equiv.dvd_apply, Submonoid.coe_mul, ← Submonoid.mul_def, _root_.map_mul, hJ,
109     inv_mul_eq_one, Nat.cast_mul]
110   simp [mul_comm, eq_comm]
111 
112 /-- The actual bounded norm-filtered generator count has the exact roots-of-unity factor. -/
113 theorem card_bounded_filtered_generators {C : ClassGroup (𝓞 K)}
114     {J : (Ideal (𝓞 K))⁰} (hJ : ClassGroup.mk0 J = C⁻¹)
115     (P : ℝ → Prop) (X : ℝ) :
116     Nat.card {a : idealSet K J //
117       mixedEmbedding.norm (a : mixedSpace K) ≤ X * absNorm (J : Ideal (𝓞 K)) ∧
118       P (mixedEmbedding.norm (a : mixedSpace K))} =
119     Nat.card {I : (Ideal (𝓞 K))⁰ // (absNorm (I : Ideal (𝓞 K)) : ℝ) ≤ X ∧
120       ClassGroup.mk0 I = C ∧
121       P ((absNorm (I : Ideal (𝓞 K)) : ℝ) * absNorm (J : Ideal (𝓞 K)))} * torsionOrder K := by
122   rw [card_generators_eq_filtered_principal_mul_torsion K J
123     (fun y => y ≤ X * absNorm (J : Ideal (𝓞 K)) ∧ P y),
124     ← filtered_class_eq_filtered_principal K hJ
125       (fun y => y ≤ X * absNorm (J : Ideal (𝓞 K)) ∧ P y)]
126   congr 1
127   apply Nat.card_congr
128   apply Equiv.subtypeEquivRight
129   intro I
130   have hN : (0 : ℝ) < absNorm (J : Ideal (𝓞 K)) := by
131     exact_mod_cast absNorm_pos_of_nonZeroDivisors J
132   rw [mul_le_mul_iff_left₀ hN]
133   exact and_left_comm
134 
135 end PaperX.IdealNormFilter

Back to source controls