feat(NumberField/CanonicalEmbedding): Define the fundamental cone for…

… the action of the units of a number field (#12268)

Let `K` be a number field of signature `(r₁, r₂)`. This PR defines the fundamental cone: it is a cone in the mixed space that is a fundamental domain for the action of `(𝓞 K)ˣ` modulo torsion. 

In a later PR #12333, we prove that points in the fundamental cone coming from `(𝓞 K)` modulo torsion are in a norm-preserving correspondence with the non-zero principal ideals of `(𝓞 K)`. 

This PR is part of the proof of the Analytic Class Number Formula. 



Co-authored-by: Xavier Roblot <[email protected]>

Mathlib/Algebra/Module/ZLattice/Basic.lean

@@ -36,7 +36,7 @@ of `ℤ`-rank equal to the `K`-rank of `E`
 ## Implementation Notes
 
 A `ZLattice` could be defined either as a `AddSubgroup E` or a `Submodule ℤ E`. However, the module
-aspects appears to be the most useful one (especially in computations involving basis) and is also
+aspect appears to be the more useful one (especially in computations involving basis) and is also
 consistent with the `ZSpan` construction of `ℤ`-lattices.
 
 -/

Mathlib/NumberTheory/NumberField/CanonicalEmbedding/Basic.lean

@@ -187,6 +187,16 @@ noncomputable def _root_.NumberField.mixedEmbedding : K →+* (mixedSpace K) :=
   RingHom.prod (Pi.ringHom fun w => embedding_of_isReal w.prop)
     (Pi.ringHom fun w => w.val.embedding)
 
+@[simp]
+theorem mixedEmbedding_apply_ofIsReal (x : K) (w : {w // IsReal w}) :
+    (mixedEmbedding K x).1 w = embedding_of_isReal w.prop x := by
+  simp_rw [mixedEmbedding, RingHom.prod_apply, Pi.ringHom_apply]
+
+@[simp]
+theorem mixedEmbedding_apply_ofIsComplex (x : K) (w : {w // IsComplex w}) :
+    (mixedEmbedding K x).2 w = w.val.embedding x := by
+  simp_rw [mixedEmbedding, RingHom.prod_apply, Pi.ringHom_apply]
+
 instance [NumberField K] : Nontrivial (mixedSpace K) := by
   obtain ⟨w⟩ := (inferInstance : Nonempty (InfinitePlace K))
   obtain hw | hw := w.isReal_or_isComplex

Mathlib/NumberTheory/NumberField/CanonicalEmbedding/FundamentalCone.lean

@@ -9,16 +9,22 @@ import Mathlib.NumberTheory.NumberField.Units.DirichletTheorem
 # Fundamental Cone
 
 Let `K` be a number field of signature `(r₁, r₂)`. We define an action of the units `(𝓞 K)ˣ` on
-the mixed space `ℝ^r₁ × ℂ^r₂` via the `mixedEmbedding`.
+the mixed space `ℝ^r₁ × ℂ^r₂` via the `mixedEmbedding`. The fundamental cone is a cone in the
+mixed space that is a fundamental domain for the action of `(𝓞 K)ˣ` modulo torsion.
 
 ## Main definitions and results
 
 * `NumberField.mixedEmbedding.unitSMul`: the action of `(𝓞 K)ˣ` on the mixed space defined, for
 `u : (𝓞 K)ˣ`, by multiplication component by component with `mixedEmbedding K u`.
 
+* `NumberField.mixedEmbedding.fundamentalCone`: a cone in the mixed space, ie. a subset stable
+by multiplication by a nonzero real number, see `smul_mem_of_mem`, that is also a fundamental
+domain for the action of `(𝓞 K)ˣ` modulo torsion, see `exists_unit_smul_mem` and
+`torsion_unit_smul_mem_of_mem`.
+
 ## Tags
 
-number field, canonical embedding, units
+number field, canonical embedding, units, principal ideals
 -/
 
 variable (K : Type*) [Field K]
@@ -113,13 +119,14 @@ theorem logMap_apply_of_norm_one (hx : mixedEmbedding.norm x = 1)
 
 @[simp]
 theorem logMap_eq_logEmbedding (u : (𝓞 K)ˣ) :
-    logMap (mixedEmbedding K u) = logEmbedding K u := by
+    logMap (mixedEmbedding K u) = logEmbedding K (Additive.ofMul u) := by
   ext; simp
 
 theorem logMap_unit_smul (u : (𝓞 K)ˣ) (hx : mixedEmbedding.norm x ≠ 0) :
-    logMap (u • x) = logEmbedding K u + logMap x := by
+    logMap (u • x) = logEmbedding K (Additive.ofMul u) + logMap x := by
   rw [unitSMul_smul, logMap_mul (by rw [norm_unit]; norm_num) hx, logMap_eq_logEmbedding]
 
+variable (x) in
 theorem logMap_torsion_smul {ζ : (𝓞 K)ˣ} (hζ : ζ ∈ torsion K) :
     logMap (ζ • x) = logMap x := by
   ext
@@ -147,4 +154,88 @@ theorem logMap_eq_of_normAtPlace_eq (h : ∀ w, normAtPlace w x = normAtPlace w
 
 end logMap
 
+noncomputable section
+
+open NumberField.Units NumberField.Units.dirichletUnitTheorem
+
+variable [NumberField K]
+
+open Classical in
+/-- The fundamental cone is a cone in the mixed space, ie. a subset fixed by multiplication by
+a nonzero real number, see `smul_mem_of_mem`, that is also a fundamental domain for the action
+of `(𝓞 K)ˣ` modulo torsion, see `exists_unit_smul_mem` and `torsion_smul_mem_of_mem`. -/
+def fundamentalCone : Set (mixedSpace K) :=
+  logMap⁻¹' (ZSpan.fundamentalDomain ((basisUnitLattice K).ofZLatticeBasis ℝ _)) \
+      {x | mixedEmbedding.norm x = 0}
+
+namespace fundamentalCone
+
+variable {K} {x y : mixedSpace K} {c : ℝ}
+
+theorem norm_pos_of_mem (hx : x ∈ fundamentalCone K) :
+    0 < mixedEmbedding.norm x :=
+  lt_of_le_of_ne (mixedEmbedding.norm_nonneg _) (Ne.symm hx.2)
+
+theorem normAtPlace_pos_of_mem (hx : x ∈ fundamentalCone K) (w : InfinitePlace K) :
+    0 < normAtPlace w x :=
+  lt_of_le_of_ne (normAtPlace_nonneg _ _)
+    (mixedEmbedding.norm_ne_zero_iff.mp (norm_pos_of_mem hx).ne' w).symm
+
+theorem mem_of_normAtPlace_eq (hx : x ∈ fundamentalCone K)
+    (hy : ∀ w, normAtPlace w y = normAtPlace w x) :
+    y ∈ fundamentalCone K := by
+  refine ⟨?_, by simpa [norm_eq_of_normAtPlace_eq hy] using hx.2⟩
+  rw [Set.mem_preimage, logMap_eq_of_normAtPlace_eq hy]
+  exact hx.1
+
+theorem smul_mem_of_mem (hx : x ∈ fundamentalCone K) (hc : c ≠ 0) :
+    c • x ∈ fundamentalCone K := by
+  refine ⟨?_, ?_⟩
+  · rw [Set.mem_preimage, logMap_real_smul hx.2 hc]
+    exact hx.1
+  · rw [Set.mem_setOf_eq, mixedEmbedding.norm_smul, mul_eq_zero, not_or]
+    exact ⟨pow_ne_zero _ (abs_ne_zero.mpr hc), hx.2⟩
+
+theorem smul_mem_iff_mem (hc : c ≠ 0) :
+    c • x ∈ fundamentalCone K ↔ x ∈ fundamentalCone K := by
+  refine ⟨fun h ↦ ?_, fun h ↦ smul_mem_of_mem h hc⟩
+  convert smul_mem_of_mem h (inv_ne_zero hc)
+  rw [eq_inv_smul_iff₀ hc]
+
+theorem exists_unit_smul_mem (hx : mixedEmbedding.norm x ≠ 0) :
+    ∃ u : (𝓞 K)ˣ, u • x ∈ fundamentalCone K := by
+  classical
+  let B := (basisUnitLattice K).ofZLatticeBasis ℝ
+  rsuffices ⟨⟨_, ⟨u, _, rfl⟩⟩, hu⟩ : ∃ e : unitLattice K, e + logMap x ∈ ZSpan.fundamentalDomain B
+  · exact ⟨u, by rwa [Set.mem_preimage, logMap_unit_smul u hx], by simp [hx]⟩
+  · obtain ⟨⟨e, h₁⟩, h₂, -⟩ := ZSpan.exist_unique_vadd_mem_fundamentalDomain B (logMap x)
+    exact ⟨⟨e, by rwa [← Basis.ofZLatticeBasis_span ℝ (unitLattice K)]⟩, h₂⟩
+
+theorem torsion_smul_mem_of_mem (hx : x ∈ fundamentalCone K) {ζ : (𝓞 K)ˣ} (hζ : ζ ∈ torsion K) :
+    ζ • x ∈ fundamentalCone K := by
+  constructor
+  · rw [Set.mem_preimage, logMap_torsion_smul _ hζ]
+    exact hx.1
+  · rw [Set.mem_setOf_eq, unitSMul_smul, map_mul, norm_unit, one_mul]
+    exact hx.2
+
+theorem unit_smul_mem_iff_mem_torsion (hx : x ∈ fundamentalCone K) (u : (𝓞 K)ˣ) :
+    u • x ∈ fundamentalCone K ↔ u ∈ torsion K := by
+  classical
+  refine ⟨fun h ↦ ?_, fun h ↦ torsion_smul_mem_of_mem hx h⟩
+  rw [← logEmbedding_eq_zero_iff]
+  let B := (basisUnitLattice K).ofZLatticeBasis ℝ
+  refine (Subtype.mk_eq_mk (h := ?_) (h' := Submodule.zero_mem _)).mp <|
+    (ZSpan.exist_unique_vadd_mem_fundamentalDomain B (logMap x)).unique ?_ ?_
+  · rw [Basis.ofZLatticeBasis_span ℝ (unitLattice K)]
+    exact ⟨u, trivial, rfl⟩
+  · rw [AddSubmonoid.mk_vadd, vadd_eq_add, ← logMap_unit_smul _ hx.2]
+    exact h.1
+  · rw [AddSubmonoid.mk_vadd, vadd_eq_add, zero_add]
+    exact hx.1
+
+end fundamentalCone
+
+end
+
 end NumberField.mixedEmbedding

Mathlib/NumberTheory/NumberField/Units/DirichletTheorem.lean

@@ -84,10 +84,11 @@ variable {K}
 
 @[simp]
 theorem logEmbedding_component (x : (𝓞 K)ˣ) (w : {w : InfinitePlace K // w ≠ w₀}) :
-    (logEmbedding K x) w = mult w.val * Real.log (w.val x) := rfl
+    (logEmbedding K (Additive.ofMul x)) w = mult w.val * Real.log (w.val x) := rfl
 
 theorem sum_logEmbedding_component (x : (𝓞 K)ˣ) :
-    ∑ w, logEmbedding K x w = - mult (w₀ : InfinitePlace K) * Real.log (w₀ (x : K)) := by
+    ∑ w, logEmbedding K (Additive.ofMul x) w =
+      - mult (w₀ : InfinitePlace K) * Real.log (w₀ (x : K)) := by
   have h := congr_arg Real.log (prod_eq_abs_norm (x : K))
   rw [Units.norm, Rat.cast_one, Real.log_one, Real.log_prod] at h
   · simp_rw [Real.log_pow] at h
@@ -112,7 +113,7 @@ theorem mult_log_place_eq_zero {x : (𝓞 K)ˣ} {w : InfinitePlace K} :
 variable [NumberField K]
 
 theorem logEmbedding_eq_zero_iff {x : (𝓞 K)ˣ} :
-    logEmbedding K x = 0 ↔ x ∈ torsion K := by
+    logEmbedding K (Additive.ofMul x) = 0 ↔ x ∈ torsion K := by
   rw [mem_torsion]
   refine ⟨fun h w => ?_, fun h => ?_⟩
   · by_cases hw : w = w₀
@@ -126,13 +127,14 @@ theorem logEmbedding_eq_zero_iff {x : (𝓞 K)ˣ} :
     rw [logEmbedding_component, h w.val, Real.log_one, mul_zero, Pi.zero_apply]
 
 theorem logEmbedding_component_le {r : ℝ} {x : (𝓞 K)ˣ} (hr : 0 ≤ r) (h : ‖logEmbedding K x‖ ≤ r)
-    (w : {w : InfinitePlace K // w ≠ w₀}) : |logEmbedding K x w| ≤ r := by
+    (w : {w : InfinitePlace K // w ≠ w₀}) : |logEmbedding K (Additive.ofMul x) w| ≤ r := by
   lift r to NNReal using hr
   simp_rw [Pi.norm_def, NNReal.coe_le_coe, Finset.sup_le_iff, ← NNReal.coe_le_coe] at h
   exact h w (mem_univ _)
 
-theorem log_le_of_logEmbedding_le {r : ℝ} {x : (𝓞 K)ˣ} (hr : 0 ≤ r) (h : ‖logEmbedding K x‖ ≤ r)
-    (w : InfinitePlace K) : |Real.log (w x)| ≤ (Fintype.card (InfinitePlace K)) * r := by
+theorem log_le_of_logEmbedding_le {r : ℝ} {x : (𝓞 K)ˣ} (hr : 0 ≤ r)
+    (h : ‖logEmbedding K (Additive.ofMul x)‖ ≤ r) (w : InfinitePlace K) :
+    |Real.log (w x)| ≤ (Fintype.card (InfinitePlace K)) * r := by
   have tool : ∀ x : ℝ, 0 ≤ x → x ≤ mult w * x := fun x hx => by
     nth_rw 1 [← one_mul x]
     refine mul_le_mul ?_ le_rfl hx ?_
@@ -320,7 +322,8 @@ theorem unitLattice_span_eq_top :
   -- The standard basis
   let B := Pi.basisFun ℝ {w : InfinitePlace K // w ≠ w₀}
   -- The image by log_embedding of the family of units constructed above
-  let v := fun w : { w : InfinitePlace K // w ≠ w₀ } => logEmbedding K (exists_unit K w).choose
+  let v := fun w : { w : InfinitePlace K // w ≠ w₀ } =>
+    logEmbedding K (Additive.ofMul (exists_unit K w).choose)
   -- To prove the result, it is enough to prove that the family `v` is linearly independent
   suffices B.det v ≠ 0 by
     rw [← isUnit_iff_ne_zero, ← is_basis_iff_det] at this
@@ -388,12 +391,12 @@ def logEmbeddingQuot :
       (QuotientGroup.quotientMulEquivOfEq (by
         ext
         rw [MonoidHom.mem_ker, AddMonoidHom.toMultiplicative'_apply_apply, ofAdd_eq_one,
-          ← logEmbedding_eq_zero_iff]
-        rfl)).toMonoidHom
+          ← logEmbedding_eq_zero_iff])).toMonoidHom
 
 @[simp]
 theorem logEmbeddingQuot_apply (x : (𝓞 K)ˣ) :
-    logEmbeddingQuot K ⟦x⟧ = logEmbedding K x := rfl
+    logEmbeddingQuot K (Additive.ofMul (QuotientGroup.mk x)) =
+      logEmbedding K (Additive.ofMul x) := rfl
 
 theorem logEmbeddingQuot_injective :
     Function.Injective (logEmbeddingQuot K) := by
@@ -429,7 +432,8 @@ def logEmbeddingEquiv :
 
 @[simp]
 theorem logEmbeddingEquiv_apply (x : (𝓞 K)ˣ) :
-    logEmbeddingEquiv K ⟦x⟧ = logEmbedding K x := rfl
+    logEmbeddingEquiv K (Additive.ofMul (QuotientGroup.mk x)) =
+      logEmbedding K (Additive.ofMul x) := rfl
 
 instance : Module.Free ℤ (Additive ((𝓞 K)ˣ ⧸ (torsion K))) :=
   Module.Free.of_equiv (logEmbeddingEquiv K).symm
@@ -466,17 +470,23 @@ def basisModTorsion : Basis (Fin (rank K)) ℤ (Additive ((𝓞 K)ˣ ⧸ (torsio
   Basis.reindex (Module.Free.chooseBasis ℤ _) (Fintype.equivOfCardEq <| by
     rw [← FiniteDimensional.finrank_eq_card_chooseBasisIndex, rank_modTorsion, Fintype.card_fin])
 
+/-- The basis of the `unitLattice` obtained by mapping `basisModTorsion` via `logEmbedding`. -/
+def basisUnitLattice : Basis (Fin (rank K)) ℤ (unitLattice K) :=
+  (basisModTorsion K).map (logEmbeddingEquiv K)
+
 /-- A fundamental system of units of `K`. The units of `fundSystem` are arbitrary lifts of the
 units in `basisModTorsion`. -/
 def fundSystem : Fin (rank K) → (𝓞 K)ˣ :=
   -- `:)` prevents the `⧸` decaying to a quotient by `leftRel` when we unfold this later
   fun i => Quotient.out' (Additive.toMul (basisModTorsion K i):)
 
 theorem fundSystem_mk (i : Fin (rank K)) :
-    Additive.ofMul ⟦fundSystem K i⟧ = (basisModTorsion K i) := by
-  rw [fundSystem, Equiv.apply_eq_iff_eq_symm_apply, @Quotient.mk_eq_iff_out,
-    Quotient.out', Quotient.out_equiv_out]
-  rfl
+    Additive.ofMul (QuotientGroup.mk (fundSystem K i)) = (basisModTorsion K i) := by
+  simp_rw [fundSystem, Equiv.apply_eq_iff_eq_symm_apply, Additive.ofMul_symm_eq, Quotient.out_eq']
+
+theorem logEmbedding_fundSystem (i : Fin (rank K)) :
+    logEmbedding K (Additive.ofMul (fundSystem K i)) = basisUnitLattice K i := by
+  rw [basisUnitLattice, Basis.map_apply, ← fundSystem_mk, logEmbeddingEquiv_apply]
 
 /-- The exponents that appear in the unique decomposition of a unit as the product of
 a root of unity and powers of the units of the fundamental system `fundSystem` (see
@@ -514,5 +524,4 @@ theorem exist_unique_eq_mul_prod (x : (𝓞 K)ˣ) : ∃! ζe : torsion K × (Fin
 
 end statements
 
-
 end NumberField.Units

Mathlib/NumberTheory/NumberField/Units/Regulator.lean

@@ -57,11 +57,11 @@ local instance : CommGroup (𝓞 K)ˣ := inferInstance
 set_option maxSynthPendingDepth 2 -- Note this is active for the remainder of the file.
 
 theorem regulator_eq_det' (e : {w : InfinitePlace K // w ≠ w₀} ≃ Fin (rank K)) :
-    regulator K = |(Matrix.of fun i ↦ (logEmbedding K) (fundSystem K (e i))).det| := by
+    regulator K = |(Matrix.of fun i ↦
+      logEmbedding K (Additive.ofMul (fundSystem K (e i)))).det| := by
   simp_rw [regulator, ZLattice.covolume_eq_det _
     (((basisModTorsion K).map (logEmbeddingEquiv K)).reindex e.symm), Basis.coe_reindex,
-    Function.comp_def, Basis.map_apply, ← fundSystem_mk, Equiv.symm_symm]
-  rfl
+    Function.comp_def, Basis.map_apply, ← fundSystem_mk, Equiv.symm_symm, logEmbeddingEquiv_apply]
 
 /-- Let `u : Fin (rank K) → (𝓞 K)ˣ` be a family of units and let `w₁` and `w₂` be two infinite
 places. Then, the two square matrices with entries `(mult w * log w (u i))_i, {w ≠ w_i}`, `i = 1,2`,