feat(NumberField/CanonicalEmbedding): define an action of the units o…

…n the mixed space (#16762)

Define an action of the units on the mixed space of a number field. In a latter PR #12268, we construct a cone in the mixed space that is a fundamental domain for the action of the units modulo torsion. 

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



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

Mathlib.lean

@@ -3461,6 +3461,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/Basic.lean

@@ -4,8 +4,8 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Xavier Roblot
 -/
 import Mathlib.Algebra.Module.ZLattice.Basic
-import Mathlib.NumberTheory.NumberField.Embeddings
 import Mathlib.NumberTheory.NumberField.FractionalIdeal
+import Mathlib.NumberTheory.NumberField.Units.Basic
 
 /-!
 # Canonical embedding of a number field
@@ -318,14 +318,21 @@ theorem normAtPlace_apply (w : InfinitePlace K) (x : K) :
     RingHom.prod_apply, Pi.ringHom_apply, norm_embedding_of_isReal, norm_embedding_eq, dite_eq_ite,
     ite_id]
 
-theorem normAtPlace_eq_zero {x : mixedSpace K} :
+theorem forall_normAtPlace_eq_zero_iff {x : mixedSpace K} :
     (∀ w, normAtPlace w x = 0) ↔ x = 0 := by
   refine ⟨fun h ↦ ?_, fun h ↦ ?_⟩
   · ext w
     · exact norm_eq_zero'.mp (normAtPlace_apply_isReal w.prop _ ▸ h w.1)
     · exact norm_eq_zero'.mp (normAtPlace_apply_isComplex w.prop _ ▸ h w.1)
   · simp_rw [h, map_zero, implies_true]
 
+@[deprecated (since := "2024-09-13")] alias normAtPlace_eq_zero := forall_normAtPlace_eq_zero_iff
+
+@[simp]
+theorem exists_normAtPlace_ne_zero_iff {x : mixedSpace K} :
+    (∃ w, normAtPlace w x ≠ 0) ↔ x ≠ 0 := by
+  rw [ne_eq, ← forall_normAtPlace_eq_zero_iff, not_forall]
+
 variable [NumberField K]
 
 theorem nnnorm_eq_sup_normAtPlace (x : mixedSpace K) :
@@ -389,6 +396,10 @@ theorem norm_eq_norm (x : K) :
     mixedEmbedding.norm (mixedEmbedding K x) = |Algebra.norm ℚ x| := by
   simp_rw [mixedEmbedding.norm_apply, normAtPlace_apply, prod_eq_abs_norm]
 
+theorem norm_unit (u : (𝓞 K)ˣ) :
+    mixedEmbedding.norm (mixedEmbedding K u) = 1 := by
+  rw [norm_eq_norm, Units.norm, Rat.cast_one]
+
 theorem norm_eq_zero_iff' {x : mixedSpace K} (hx : x ∈ Set.range (mixedEmbedding K)) :
     mixedEmbedding.norm x = 0 ↔ x = 0 := by
   obtain ⟨a, rfl⟩ := hx

Mathlib/NumberTheory/NumberField/CanonicalEmbedding/ConvexBody.lean

@@ -312,8 +312,8 @@ theorem convexBodySumFun_smul (c : ℝ) (x : mixedSpace K) :
 
 theorem convexBodySumFun_eq_zero_iff (x : mixedSpace K) :
     convexBodySumFun x = 0 ↔ x = 0 := by
-  rw [← normAtPlace_eq_zero, convexBodySumFun, Finset.sum_eq_zero_iff_of_nonneg fun _ _ =>
-    mul_nonneg (Nat.cast_pos.mpr mult_pos).le (normAtPlace_nonneg _ _)]
+  rw [← forall_normAtPlace_eq_zero_iff, convexBodySumFun, Finset.sum_eq_zero_iff_of_nonneg
+    fun _ _ ↦ mul_nonneg (Nat.cast_pos.mpr mult_pos).le (normAtPlace_nonneg _ _)]
   conv =>
     enter [1, w, hw]
     rw [mul_left_mem_nonZeroDivisors_eq_zero_iff

Mathlib/NumberTheory/NumberField/CanonicalEmbedding/FundamentalCone.lean

@@ -0,0 +1,70 @@
+/-
+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.CanonicalEmbedding.Basic
+
+/-!
+# 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`.
+
+## 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`.
+
+## Tags
+
+number field, canonical embedding, units
+-/
+
+variable (K : Type*) [Field K]
+
+namespace NumberField.mixedEmbedding
+
+open NumberField NumberField.InfinitePlace
+
+noncomputable section UnitSMul
+
+/-- The action of `(𝓞 K)ˣ` on the mixed space `ℝ^r₁ × ℂ^r₂` defined, for `u : (𝓞 K)ˣ`, by
+multiplication component by component with `mixedEmbedding K u`. -/
+@[simps]
+instance unitSMul : SMul (𝓞 K)ˣ (mixedSpace K) where
+  smul u x := mixedEmbedding K u * x
+
+instance : MulAction (𝓞 K)ˣ (mixedSpace K) where
+  one_smul := fun _ ↦ by simp_rw [unitSMul_smul, Units.coe_one, map_one, one_mul]
+  mul_smul := fun _ _ _ ↦ by simp_rw [unitSMul_smul, Units.coe_mul, map_mul, mul_assoc]
+
+instance : SMulZeroClass (𝓞 K)ˣ (mixedSpace K) where
+  smul_zero := fun _ ↦ by simp_rw [unitSMul_smul, mul_zero]
+
+variable {K}
+
+theorem unit_smul_eq_zero (u : (𝓞 K)ˣ) (x : mixedSpace K) :
+    u • x = 0 ↔ x = 0 := by
+  refine ⟨fun h ↦ ?_, fun h ↦ by rw [h, smul_zero]⟩
+  contrapose! h
+  obtain ⟨w, h⟩ := exists_normAtPlace_ne_zero_iff.mpr h
+  refine exists_normAtPlace_ne_zero_iff.mp ⟨w, ?_⟩
+  rw [unitSMul_smul, map_mul]
+  exact mul_ne_zero (by simp) h
+
+variable [NumberField K]
+
+theorem unit_smul_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, ← RingOfIntegers.coe_eq_algebraMap,
+    ← map_mul, ← RingOfIntegers.ext_iff]
+  exact mixedEmbedding_injective K
+
+theorem norm_unit_smul (u : (𝓞 K)ˣ) (x : mixedSpace K) :
+    mixedEmbedding.norm (u • x) = mixedEmbedding.norm x := by
+  rw [unitSMul_smul, map_mul, norm_unit, one_mul]
+
+end UnitSMul
+
+end NumberField.mixedEmbedding