[Merged by Bors] - feat(NumberField/CanonicalEmbedding): Define the fundamental cone for the action of the units of a number field

Mathlib.lean

@@ -3053,6 +3053,7 @@ import Mathlib.NumberTheory.Multiplicity
 import Mathlib.NumberTheory.NumberField.Basic
 import Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic
 import Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody
+import Mathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone
 import Mathlib.NumberTheory.NumberField.ClassNumber
 import Mathlib.NumberTheory.NumberField.Discriminant
 import Mathlib.NumberTheory.NumberField.Embeddings

Mathlib/NumberTheory/NumberField/CanonicalEmbedding/FundamentalCone.lean

@@ -0,0 +1,209 @@
+/-
+Copyright (c) 2024 Xavier Roblot. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Xavier Roblot
+-/
+import Mathlib.NumberTheory.NumberField.Units
+
+/-!
+# Fundamental Cone
+
+Let `K` be a number field of signature `(r₁, r₂)`. We define an action of the group of units
+`(𝓞 K)ˣ` of `K` on the space `ℝ^r₁ × ℂ^r₂`. The fundamental cone is a cone in `ℝ^r₁ × ℂ^r₂`
+that is a fundamental domain for the action of `(𝓞 K)ˣ` up to roots of unity.
+
+## Main definitions and results
+
+* `NumberField.mixedEmbedding.unitSMul`: The action of `(𝓞 K)ˣ` on `ℝ^r₁ × ℂ^r₂` defined, for
+`u : (𝓞 K)ˣ`, by multiplication component by component with `mixedEmbedding K u`.
+
+* `NumberField.mixedEmbedding.fundamentalCone`: A cone in `ℝ^r₁ × ℂ^r₂` --that is a subset stable
+under multiplication by a real number, see `smul_mem_of_mem`--, that is also a fundamental domain
+for the action of `(𝓞 K)ˣ` up to roots of unity, see `exists_unitSMul_me` and
+`torsion_unitSMul_mem_of_mem`.
+
+## Tags
+
+number field, canonical embedding, units
+-/
+
+variable (K : Type*) [Field K]
+
+namespace NumberField.mixedEmbedding
+
+open NumberField NumberField.InfinitePlace
+
+/-- The space `ℝ^r₁ × ℂ^r₂` with `(r₁, r₂)` the signature of `K`. -/
+local notation "E" K =>
+  ({w : InfinitePlace K // IsReal w} → ℝ) × ({w : InfinitePlace K // IsComplex w} → ℂ)
+
+noncomputable section UnitSMul
+
+/-- The action of `(𝓞 K)ˣ` on `ℝ^r₁ × ℂ^r₂` defined, for `u : (𝓞 K)ˣ`, by multiplication component
+by component with `mixedEmbedding K u`. -/
+@[simps]
+instance unitSMul : SMul (𝓞 K)ˣ (E K) where
+  smul := fun u x ↦ (mixedEmbedding K u) * x
+
+instance : MulAction (𝓞 K)ˣ (E K) where
+  one_smul := fun _ ↦ by simp_rw [HSMul.hSMul, SMul.smul, Units.coe_one, map_one, one_mul]
+  mul_smul := fun _ _ _ ↦ by simp_rw [HSMul.hSMul, SMul.smul, Units.coe_mul, map_mul, mul_assoc]
+
+instance : SMulZeroClass (𝓞 K)ˣ (E K) where
+  smul_zero := fun _ ↦ by simp_rw [HSMul.hSMul, SMul.smul, mul_zero]
+
+variable [NumberField K]
+
+theorem unitSMul_eq_iff_mul_eq {x y : (𝓞 K)} {u : (𝓞 K)ˣ} :
+    u • mixedEmbedding K x = mixedEmbedding K y ↔ u * x = y := by
+  rw [unitSMul_smul, ← map_mul, Function.Injective.eq_iff, ← Submonoid.coe_mul, Subtype.mk_eq_mk]
+  exact mixedEmbedding_injective K
+
+theorem norm_unit (u : (𝓞 K)ˣ) :
+    mixedEmbedding.norm (mixedEmbedding K u) = 1 := by
+  rw [norm_eq_norm, show |(Algebra.norm ℚ) (u : K)| = 1
+      by exact NumberField.isUnit_iff_norm.mp (Units.isUnit u), Rat.cast_one]
+
+theorem norm_unitSMul (u : (𝓞 K)ˣ) (x : E K) :
+    mixedEmbedding.norm (u • x) = mixedEmbedding.norm x := by
+  rw [unitSMul_smul, map_mul, norm_unit, one_mul]
+
+end UnitSMul
+
+noncomputable section logMap
+
+open NumberField.Units NumberField.Units.dirichletUnitTheorem FiniteDimensional
+
+variable [NumberField K] {K}
+
+/-- The map from `ℝ^r₁ × ℂ^r₂` to `{w : InfinitePlace K // w ≠ w₀} → ℝ` (with `w₀` a fixed place)
+defined in such way that: 1) it factors the map `logEmbedding`, see `logMap_eq_logEmbedding`;
+2) it is constant on the lines `{c • x | c ∈ ℝ}`, see `logMap_smul`. -/
+def logMap (x : E K) : {w : InfinitePlace K // w ≠ w₀} → ℝ := by
+  classical
+  exact fun w ↦
+    if hw : IsReal w.val then
+      Real.log ‖x.1 ⟨w.val, hw⟩‖ - Real.log (mixedEmbedding.norm x) * (finrank ℚ K : ℝ)⁻¹
+    else
+      2 * (Real.log ‖x.2 ⟨w.val, not_isReal_iff_isComplex.mp hw⟩‖ -
+        Real.log (mixedEmbedding.norm x) * (finrank ℚ K : ℝ)⁻¹)
+
+theorem logMap_zero : logMap (0 : E K) = 0 := by
+  ext
+  simp_rw [logMap, Prod.fst_zero, Prod.snd_zero, map_zero, Pi.zero_apply, norm_zero, Real.log_zero,
+    zero_mul, sub_zero, mul_zero, dite_eq_ite, ite_self]
+
+theorem logMap_mul {x y : E K} (hx : mixedEmbedding.norm x ≠ 0) (hy : mixedEmbedding.norm y ≠ 0) :
+    logMap (x * y) = logMap x + logMap y := by
+  ext w
+  simp_rw [Pi.add_apply, logMap]
+  split_ifs with hw
+  · rw [Prod.fst_mul, Pi.mul_apply, norm_mul, map_mul, Real.log_mul, Real.log_mul hx hy, add_mul]
+    · ring
+    · exact norm_ne_zero_iff.mpr <| (mixedEmbedding.norm_ne_zero_iff.mp hx).1 ⟨_, hw⟩
+    · exact norm_ne_zero_iff.mpr <| (mixedEmbedding.norm_ne_zero_iff.mp hy).1 ⟨_, hw⟩
+  · replace hw := not_isReal_iff_isComplex.mp hw
+    rw [Prod.snd_mul, Pi.mul_apply, norm_mul, map_mul, Real.log_mul, Real.log_mul hx hy, add_mul]
+    · ring
+    · exact norm_ne_zero_iff.mpr <| (mixedEmbedding.norm_ne_zero_iff.mp hx).2 ⟨_, hw⟩
+    · exact norm_ne_zero_iff.mpr <| (mixedEmbedding.norm_ne_zero_iff.mp hy).2 ⟨_, hw⟩
+
+theorem logMap_eq_logEmbedding (u : (𝓞 K)ˣ) :
+    logMap (mixedEmbedding K u) = logEmbedding K u := by
+  ext
+  simp_rw [logMap, mixedEmbedding.norm_unit, Real.log_one, zero_mul, sub_zero, logEmbedding,
+    AddMonoidHom.coe_mk, ZeroHom.coe_mk, mult, Nat.cast_ite, ite_mul, Nat.cast_one, one_mul,
+    Nat.cast_ofNat, mixedEmbedding, RingHom.prod_apply, Pi.ringHom_apply, norm_embedding_eq,
+    norm_embedding_of_isReal]
+  rfl
+
+theorem logMap_unitSMul (u : (𝓞 K)ˣ) {x : E K} (hx : mixedEmbedding.norm x ≠ 0) :
+    logMap (u • x) = logEmbedding K u + logMap x := by
+  rw [unitSMul_smul, logMap_mul (by rw [norm_unit]; norm_num) hx, logMap_eq_logEmbedding]
+
+theorem logMap_torsion_unitSMul (x : E K) {ζ : (𝓞 K)ˣ} (hζ : ζ ∈ torsion K) :
+    logMap (ζ • x) = logMap x := by
+  ext
+  simp_rw [logMap, unitSMul_smul, Prod.fst_mul, Prod.snd_mul, Pi.mul_apply, norm_mul, map_mul,
+    norm_eq_norm, mixedEmbedding, RingHom.prod_apply, Pi.ringHom_apply,
+    show |(Algebra.norm ℚ) (ζ : K)| = 1 by exact NumberField.isUnit_iff_norm.mp (Units.isUnit ζ),
+    Rat.cast_one, one_mul, norm_embedding_eq, norm_embedding_of_isReal, (mem_torsion K).mp hζ,
+    one_mul]
+
+theorem logMap_smul {x : E K} {c : ℝ} (hx : mixedEmbedding.norm x ≠ 0) (hc : c ≠ 0) :
+    logMap (c • x) = logMap x := by
+  rw [show c • x = ((fun _ ↦ c, fun _ ↦ c) : (E K)) * x by rfl, logMap_mul _ hx, add_left_eq_self]
+  ext
+  have hr : (finrank ℚ K : ℝ) ≠ 0 :=  Nat.cast_ne_zero.mpr (ne_of_gt finrank_pos)
+  simp_rw [logMap, Pi.zero_apply, norm_real, Real.log_pow, mul_comm, inv_mul_cancel_left₀ hr,
+    Real.norm_eq_abs, Complex.norm_eq_abs,  Complex.abs_ofReal, sub_self, mul_zero, dite_eq_ite,
+    ite_self]
+  rw [norm_real]
+  exact pow_ne_zero _ (abs_ne_zero.mpr hc)
+
+end logMap
+
+noncomputable section
+
+open NumberField.Units NumberField.Units.dirichletUnitTheorem
+
+variable [NumberField K]
+
+/-- The fundamental cone is a cone in `ℝ^r₁ × ℂ^r₂` --that is a subset stable under multiplication
+by a real number, see `smul_mem_of_mem`--, that is also a fundamental domain for the action of
+`(𝓞 K)ˣ` up to roots of unity, see `exists_unitSMul_mem` and `torsion_unitSMul_mem_of_mem`. -/
+def fundamentalCone : Set (E K) := by
+  classical
+  let B := (Module.Free.chooseBasis ℤ (unitLattice K)).ofZlatticeBasis ℝ _
+  exact logMap⁻¹' (Zspan.fundamentalDomain B)
+
+namespace fundamentalCone
+
+protected theorem zero_mem : 0 ∈ fundamentalCone K := by
+  simp_rw [fundamentalCone, Set.mem_preimage, Zspan.mem_fundamentalDomain, logMap_zero, map_zero,
+    Finsupp.coe_zero, Pi.zero_apply, Set.left_mem_Ico, zero_lt_one, implies_true]
+
+variable {K}
+
+theorem smul_mem_of_mem {x : E K} (hx : mixedEmbedding.norm x ≠ 0) (hx' : x ∈ fundamentalCone K)
+    (c : ℝ) : c • x ∈ fundamentalCone K := by
+  by_cases hc : c = 0
+  · rw [hc, zero_smul]
+    exact fundamentalCone.zero_mem K
+  · rwa [fundamentalCone, Set.mem_preimage, logMap_smul hx hc]
+
+theorem exists_unitSMul_mem {x : E K} (hx : mixedEmbedding.norm x ≠ 0) :
+    ∃ u : (𝓞 K)ˣ, u • x ∈ fundamentalCone K := by
+  classical
+  let B := (Module.Free.chooseBasis ℤ (unitLattice K)).ofZlatticeBasis ℝ
+  rsuffices ⟨⟨_, ⟨u, _, rfl⟩⟩, hu⟩ : ∃ e : unitLattice K, e + logMap x ∈ Zspan.fundamentalDomain B
+  · exact ⟨u, by rwa [fundamentalCone, Set.mem_preimage, logMap_unitSMul u 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_unitSMul_mem_of_mem {x : E K}
+    (hx' : x ∈ fundamentalCone K) {ζ : (𝓞 K)ˣ} (hζ : ζ ∈ torsion K) :
+    ζ • x ∈ fundamentalCone K := by
+  rwa [fundamentalCone, Set.mem_preimage, logMap_torsion_unitSMul _ hζ]
+
+theorem unitSMul_mem_iff_mem_torsion {x : E K} (hx : mixedEmbedding.norm x ≠ 0)
+    (hx' : x ∈ fundamentalCone K) (u : (𝓞 K)ˣ) :
+    u • x ∈ fundamentalCone K ↔ u ∈ torsion K := by
+  classical
+  refine ⟨fun h ↦ ?_, fun h ↦ ?_⟩
+  · rw [← logEmbedding_eq_zero_iff]
+    let B := (Module.Free.chooseBasis ℤ (unitLattice K)).ofZlatticeBasis ℝ
+    refine (Subtype.mk_eq_mk (h := ?_) (h' := ?_)).mp <|
+      ExistsUnique.unique (Zspan.exist_unique_vadd_mem_fundamentalDomain B (logMap x)) ?_ ?_
+    · change logEmbedding K u ∈ (Submodule.span ℤ (Set.range B)).toAddSubgroup
+      rw [Basis.ofZlatticeBasis_span ℝ (unitLattice K)]
+      exact ⟨u, trivial, rfl⟩
+    · exact Submodule.zero_mem _
+    · rwa [fundamentalCone, Set.mem_preimage, logMap_unitSMul _ hx] at h
+    · rw [AddSubmonoid.mk_vadd, vadd_eq_add, zero_add]
+      rwa [fundamentalCone, Set.mem_preimage] at hx'
+  · exact torsion_unitSMul_mem_of_mem hx' h
+
+end fundamentalCone
+
+end