RayCountingUnits.lean

1 import Mathlib.NumberTheory.NumberField.Units.Regulator
2 
3 /-!
4 An actual arithmetic input for ray-class counting: powers of the existing fundamental units
5 are congruent to one modulo a nonzero integral ideal and positive at every real embedding.
6 Their logarithms still form a full-rank family. This does not prove a ray-class ideal-count
7 estimate, nor identify a fundamental domain for the complete ray-unit group.
8 -/
9 
10 set_option autoImplicit false
11 noncomputable section
12 
13 namespace PaperX.RayCountingUnits
14 
15 open NumberField NumberField.Units
16 open scoped NumberField
17 
18 variable (K : Type*) [Field K] [NumberField K]
19 
20 /-- The actual reduction homomorphism on integral units. -/
21 def unitReduction (m : Ideal (𝓞 K)) : (𝓞 K)ˣ →* (𝓞 K ⧸ m)ˣ :=
22   Units.map (Ideal.Quotient.mk m).toMonoidHom
23 
24 /-- The finite-modulus congruence subgroup. -/
25 def congruenceUnits (m : Ideal (𝓞 K)) : Subgroup (𝓞 K)ˣ :=
26   (unitReduction K m).ker
27 
28 omit [NumberField K] in
29 theorem mem_congruenceUnits_iff (m : Ideal (𝓞 K)) (u : (𝓞 K)ˣ) :
30     u ∈ congruenceUnits K m ↔ (u : 𝓞 K) - 1 ∈ m := by
31   change unitReduction K m u = 1 ↔ _
32   rw [← Units.val_inj]
33   exact Ideal.Quotient.mk_eq_one_iff_sub_mem (u : 𝓞 K)
34 
35 theorem congruenceUnits_finiteIndex (m : Ideal (𝓞 K)) (hm : m ≠ ⊥) :
36     (congruenceUnits K m).FiniteIndex := by
37   let : Finite (𝓞 K ⧸ m) := Ring.HasFiniteQuotients.finiteQuotient hm
38   exact Subgroup.finiteIndex_ker (unitReduction K m)
39 
40 /-- Doubling the order of the finite residue-unit group also imposes total positivity. -/
41 def rayExponent (m : Ideal (𝓞 K)) : ℕ := 2 * Nat.card (𝓞 K ⧸ m)ˣ
42 
43 theorem rayExponent_pos (m : Ideal (𝓞 K)) (hm : m ≠ ⊥) :
44     0 < rayExponent K m := by
45   let : Finite (𝓞 K ⧸ m) := Ring.HasFiniteQuotients.finiteQuotient hm
46   exact Nat.mul_pos (by decide) Nat.card_pos
47 
48 omit [NumberField K] in
49 theorem pow_rayExponent_mem (m : Ideal (𝓞 K)) (u : (𝓞 K)ˣ) :
50     u ^ rayExponent K m ∈ congruenceUnits K m := by
51   change unitReduction K m (u ^ rayExponent K m) = 1
52   rw [map_pow, rayExponent, Nat.mul_comm 2, pow_mul, pow_card_eq_one', one_pow]
53 
54 omit [NumberField K] in
55 theorem pow_rayExponent_real_pos (m : Ideal (𝓞 K)) (u : (𝓞 K)ˣ)
56     (σ : K →+* ℝ) :
57     0 < σ ((u ^ rayExponent K m : (𝓞 K)ˣ) : K) := by
58   rw [NumberField.Units.coe_pow, map_pow, rayExponent, Nat.mul_comm 2, pow_mul]
59   exact sq_pos_of_ne_zero (pow_ne_zero _ ((map_ne_zero σ).mpr (NumberField.Units.coe_ne_zero u)))
60 
61 theorem isMaxRank_pow {u : Fin (rank K) → (𝓞 K)ˣ} (hu : IsMaxRank u)
62     {n : ℕ} (hn : n ≠ 0) : IsMaxRank (fun i => u i ^ n) := by
63   have hn' : (n : ℝ) ≠ 0 := Nat.cast_ne_zero.mpr hn
64   convert hu.units_smul (fun _ => Units.mk0 (n : ℝ) hn') using 1
65   funext i
66   change logEmbedding K (Additive.ofMul (u i ^ n)) =
67     (n : ℝ) • logEmbedding K (Additive.ofMul (u i))
68   rw [ofMul_pow, map_nsmul, Nat.cast_smul_eq_nsmul]
69 
70 /-- A concrete full-rank family satisfying the finite and all real-place ray conditions. -/
71 def rayFamily (m : Ideal (𝓞 K)) : Fin (rank K) → (𝓞 K)ˣ :=
72   fun i => fundSystem K i ^ rayExponent K m
73 
74 theorem rayFamily_isMaxRank (m : Ideal (𝓞 K)) (hm : m ≠ ⊥) :
75     IsMaxRank (rayFamily K m) :=
76   isMaxRank_pow K (isMaxRank_fundSystem K) (rayExponent_pos K m hm).ne'
77 
78 theorem rayFamily_mem (m : Ideal (𝓞 K)) (i : Fin (rank K)) :
79     (rayFamily K m i : 𝓞 K) - 1 ∈ m :=
80   (mem_congruenceUnits_iff K m _).mp (pow_rayExponent_mem K m _)
81 
82 theorem rayFamily_real_pos (m : Ideal (𝓞 K)) (i : Fin (rank K)) (σ : K →+* ℝ) :
83     0 < σ (rayFamily K m i : K) :=
84   pow_rayExponent_real_pos K m _ σ
85 
86 theorem rayFamily_closure_finiteIndex (m : Ideal (𝓞 K)) (hm : m ≠ ⊥) :
87     (Subgroup.closure (Set.range (rayFamily K m))).FiniteIndex :=
88   isMaxRank_iff_closure_finiteIndex.mp (rayFamily_isMaxRank K m hm)
89 
90 theorem rayFamily_regulator_pos (m : Ideal (𝓞 K)) (hm : m ≠ ⊥) :
91     0 < regOfFamily (rayFamily K m) :=
92   regOfFamily_pos (rayFamily_isMaxRank K m hm)
93 
94 /-- Positivity is imposed on actual real field embeddings, rather than on local labels. -/
95 def totallyPositiveUnits : Subgroup (𝓞 K)ˣ where
96   carrier := {u | ∀ σ : K →+* ℝ, 0 < σ (u : K)}
97   one_mem' := by intro σ; simp
98   mul_mem' := by
99     intro u v hu hv σ
100     rw [NumberField.Units.coe_mul, map_mul]
101     exact mul_pos (hu σ) (hv σ)
102   inv_mem' := by
103     intro u hu σ
104     rw [← zpow_neg_one u, NumberField.Units.coe_zpow, map_zpow₀, zpow_neg_one]
105     exact inv_pos.mpr (hu σ)
106 
107 /-- The actual ray-unit subgroup for finite modulus `m` and every real place. -/
108 def rayUnits (m : Ideal (𝓞 K)) : Subgroup (𝓞 K)ˣ :=
109   congruenceUnits K m ⊓ totallyPositiveUnits K
110 
111 omit [NumberField K] in
112 theorem mem_rayUnits_iff (m : Ideal (𝓞 K)) (u : (𝓞 K)ˣ) :
113     u ∈ rayUnits K m ↔
114       (u : 𝓞 K) - 1 ∈ m ∧ ∀ σ : K →+* ℝ, 0 < σ (u : K) := by
115   exact and_congr_left (fun _ => mem_congruenceUnits_iff K m u)
116 
117 theorem rayFamily_mem_rayUnits (m : Ideal (𝓞 K)) (i : Fin (rank K)) :
118     rayFamily K m i ∈ rayUnits K m :=
119   ⟨pow_rayExponent_mem K m _, rayFamily_real_pos K m i⟩
120 
121 theorem rayUnits_finiteIndex (m : Ideal (𝓞 K)) (hm : m ≠ ⊥) :
122     (rayUnits K m).FiniteIndex := by
123   let := rayFamily_closure_finiteIndex K m hm
124   apply Subgroup.finiteIndex_of_le (H := Subgroup.closure (Set.range (rayFamily K m)))
125   rw [Subgroup.closure_le]
126   rintro _ ⟨i, rfl⟩
127   exact rayFamily_mem_rayUnits K m i
128 
129 /-- The real-place condition is not the automatically nonnegative absolute-value map. -/
130 theorem neg_one_not_rayUnits_rat (m : Ideal (𝓞 ℚ)) :
131     (-1 : (𝓞 ℚ)ˣ) ∉ rayUnits ℚ m := by
132   intro h
133   have hp := h.2 (algebraMap ℚ ℝ)
134   norm_num [NumberField.Units.coe_neg_one] at hp
135 
136 end PaperX.RayCountingUnits

Back to source controls