From 9447d9412c134efea7aa5609c02867cae77a852b Mon Sep 17 00:00:00 2001 From: Xavier Roblot Date: Sun, 15 Sep 2024 07:39:46 +0000 Subject: [PATCH] feat(NumberField/CanonicalEmbedding): define an action of the units on 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 <46200072+xroblot@users.noreply.github.com> --- Mathlib.lean | 1 + .../NumberField/CanonicalEmbedding/Basic.lean | 15 +++- .../CanonicalEmbedding/ConvexBody.lean | 4 +- .../CanonicalEmbedding/FundamentalCone.lean | 70 +++++++++++++++++++ 4 files changed, 86 insertions(+), 4 deletions(-) create mode 100644 Mathlib/NumberTheory/NumberField/CanonicalEmbedding/FundamentalCone.lean diff --git a/Mathlib.lean b/Mathlib.lean index c062f7957b5c4..c83a7532fc074 100644 --- a/Mathlib.lean +++ b/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 diff --git a/Mathlib/NumberTheory/NumberField/CanonicalEmbedding/Basic.lean b/Mathlib/NumberTheory/NumberField/CanonicalEmbedding/Basic.lean index d305dd5290f95..8463e5681fcb9 100644 --- a/Mathlib/NumberTheory/NumberField/CanonicalEmbedding/Basic.lean +++ b/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,7 +318,7 @@ 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 @@ -326,6 +326,13 @@ theorem normAtPlace_eq_zero {x : mixedSpace K} : · 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 diff --git a/Mathlib/NumberTheory/NumberField/CanonicalEmbedding/ConvexBody.lean b/Mathlib/NumberTheory/NumberField/CanonicalEmbedding/ConvexBody.lean index 77f970b7e0ebe..be75dd9a3e776 100644 --- a/Mathlib/NumberTheory/NumberField/CanonicalEmbedding/ConvexBody.lean +++ b/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 diff --git a/Mathlib/NumberTheory/NumberField/CanonicalEmbedding/FundamentalCone.lean b/Mathlib/NumberTheory/NumberField/CanonicalEmbedding/FundamentalCone.lean new file mode 100644 index 0000000000000..8efe7b356ae10 --- /dev/null +++ b/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