feat: Define the regulator of a number field (#12504)

This PR defines the regulator of a number field `K` as the covolume of its `unitLattice K`. Basic results about the regulator are proved including the fact that it is equal to the absolute value of the matrix with entries `mult w * Real.log w (fundSystem K i)` where `fundSystem K` is the fundamental system of units and `w` runs through all the infinite places of `K` but one.

Author: xroblot

Mathlib.lean

@@ -3213,6 +3213,7 @@ import Mathlib.NumberTheory.NumberField.FractionalIdeal
 import Mathlib.NumberTheory.NumberField.Norm
 import Mathlib.NumberTheory.NumberField.Units.Basic
 import Mathlib.NumberTheory.NumberField.Units.DirichletTheorem
+import Mathlib.NumberTheory.NumberField.Units.Regulator
 import Mathlib.NumberTheory.Ostrowski
 import Mathlib.NumberTheory.Padics.Hensel
 import Mathlib.NumberTheory.Padics.PadicIntegers

Mathlib/Algebra/Ring/NegOnePow.lean

@@ -70,6 +70,10 @@ lemma negOnePow_eq_neg_one_iff (n : ℤ) : n.negOnePow = -1 ↔ Odd n := by
     contradiction
   · exact negOnePow_odd n
 
+@[simp]
+theorem abs_negOnePow (n : ℤ) : |(n.negOnePow : ℤ)| = 1 := by
+  rw [abs_eq_natAbs, Int.units_natAbs, Nat.cast_one]
+
 @[simp]
 lemma negOnePow_neg (n : ℤ) : (-n).negOnePow = n.negOnePow := by
   dsimp [negOnePow]

Mathlib/GroupTheory/Perm/Sign.lean

@@ -462,6 +462,11 @@ theorem sign_prod_list_swap {l : List (Perm α)} (hl : ∀ g ∈ l, IsSwap g) :
   rw [← List.prod_replicate, ← h₁, List.prod_hom _ (@sign α _ _)]
 #align equiv.perm.sign_prod_list_swap Equiv.Perm.sign_prod_list_swap
 
+@[simp]
+theorem sign_abs (f : Perm α) :
+    |(Equiv.Perm.sign f : ℤ)| = 1 := by
+  rw [Int.abs_eq_natAbs, Int.units_natAbs, Nat.cast_one]
+
 variable (α)
 
 theorem sign_surjective [Nontrivial α] : Function.Surjective (sign : Perm α → ℤˣ) := fun a =>

Mathlib/NumberTheory/NumberField/Units/Basic.lean

@@ -93,6 +93,11 @@ end coe
 
 open NumberField.InfinitePlace
 
+@[simp]
+protected theorem norm [NumberField K] (x : (𝓞 K)ˣ) :
+    |Algebra.norm ℚ (x : K)| = 1 := by
+  rw [← RingOfIntegers.coe_norm, isUnit_iff_norm.mp x.isUnit]
+
 section torsion
 
 /-- The torsion subgroup of the group of units. -/

Mathlib/NumberTheory/NumberField/Units/DirichletTheorem.lean

@@ -72,7 +72,8 @@ def w₀ : InfinitePlace K := (inferInstance : Nonempty (InfinitePlace K)).some
 variable (K)
 
 /-- The logarithmic embedding of the units (seen as an `Additive` group). -/
-def logEmbedding : Additive ((𝓞 K)ˣ) →+ ({w : InfinitePlace K // w ≠ w₀} → ℝ) :=
+def _root_.NumberField.Units.logEmbedding :
+    Additive ((𝓞 K)ˣ) →+ ({w : InfinitePlace K // w ≠ w₀} → ℝ) :=
 { toFun := fun x w => mult w.val * Real.log (w.val ↑(Additive.toMul x))
   map_zero' := by simp; rfl
   map_add' := fun _ _ => by simp [Real.log_mul, mul_add]; rfl }
@@ -86,8 +87,7 @@ theorem logEmbedding_component (x : (𝓞 K)ˣ) (w : {w : InfinitePlace K // w 
 theorem sum_logEmbedding_component (x : (𝓞 K)ˣ) :
     ∑ w, logEmbedding K 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 [show |(Algebra.norm ℚ) (x : K)| = 1 from isUnit_iff_norm.mp x.isUnit, Rat.cast_one,
-    Real.log_one, Real.log_prod] at h
+  rw [Units.norm, Rat.cast_one, Real.log_one, Real.log_prod] at h
   · simp_rw [Real.log_pow] at h
     rw [← insert_erase (mem_univ w₀), sum_insert (not_mem_erase w₀ univ), add_comm,
       add_eq_zero_iff_eq_neg] at h
@@ -374,6 +374,29 @@ theorem unitLattice_rank :
     finrank ℤ (unitLattice K) = Units.rank K := by
   rw [← Units.finrank_eq_rank, Zlattice.rank ℝ]
 
+/-- The map obtained by quotienting by the kernel of `logEmbedding`. -/
+def logEmbeddingQuot :
+    Additive ((𝓞 K)ˣ ⧸ (torsion K)) →+ ({w : InfinitePlace K // w ≠ w₀} → ℝ) :=
+  MonoidHom.toAdditive' <|
+    (QuotientGroup.kerLift (AddMonoidHom.toMultiplicative' (logEmbedding K))).comp
+      (QuotientGroup.quotientMulEquivOfEq (by
+        ext
+        rw [MonoidHom.mem_ker, AddMonoidHom.toMultiplicative'_apply_apply, ofAdd_eq_one,
+          ← logEmbedding_eq_zero_iff]
+        rfl)).toMonoidHom
+
+@[simp]
+theorem logEmbeddingQuot_apply (x : (𝓞 K)ˣ) :
+    logEmbeddingQuot K ⟦x⟧ = logEmbedding K x := rfl
+
+theorem logEmbeddingQuot_injective :
+    Function.Injective (logEmbeddingQuot K) := by
+  unfold logEmbeddingQuot
+  intro _ _ h
+  simp_rw [MonoidHom.toAdditive'_apply_apply, MonoidHom.coe_comp, MulEquiv.coe_toMonoidHom,
+    Function.comp_apply, EmbeddingLike.apply_eq_iff_eq] at h
+  exact (EmbeddingLike.apply_eq_iff_eq _).mp <| (QuotientGroup.kerLift_injective _).eq_iff.mp h
+
 #adaptation_note
 /--
 After https://github.com/leanprover/lean4/pull/4119
@@ -386,36 +409,25 @@ local instance : CommGroup (𝓞 K)ˣ := inferInstance
 -/
 set_option maxSynthPendingDepth 2 -- Note this is active for the remainder of the file.
 
-private theorem unitLatticeEquiv_aux1 :
-    (logEmbedding K).ker = (MonoidHom.toAdditive (QuotientGroup.mk' (torsion K))).ker := by
-  ext
-  rw [MonoidHom.coe_toAdditive_ker, QuotientGroup.ker_mk', AddMonoidHom.mem_ker,
-    logEmbedding_eq_zero_iff]
-  rfl
+/-- The linear equivalence between `(𝓞 K)ˣ ⧸ (torsion K)` as an additive `ℤ`-module and
+`unitLattice` . -/
+def logEmbeddingEquiv :
+    Additive ((𝓞 K)ˣ ⧸ (torsion K)) ≃ₗ[ℤ] (unitLattice K) :=
+  (AddEquiv.ofBijective (AddMonoidHom.codRestrict (logEmbeddingQuot K) _
+  (Quotient.ind fun x ↦ logEmbeddingQuot_apply K _ ▸ AddSubgroup.mem_map_of_mem _ trivial))
+  ⟨fun _ _ ↦ by
+    rw [AddMonoidHom.codRestrict_apply, AddMonoidHom.codRestrict_apply, Subtype.mk.injEq]
+    apply logEmbeddingQuot_injective K, fun ⟨a, ⟨b, _, ha⟩⟩ ↦ ⟨⟦b⟧, by simp [ha]⟩⟩).toIntLinearEquiv
 
-private theorem unitLatticeEquiv_aux2 :
-    Function.Surjective (MonoidHom.toAdditive (QuotientGroup.mk' (torsion K))) := by
-  intro x
-  refine ⟨Additive.ofMul x.out', ?_⟩
-  simp only [MonoidHom.toAdditive_apply_apply, toMul_ofMul, QuotientGroup.mk'_apply,
-      QuotientGroup.out_eq']
-  rfl
-
-/-- The linear equivalence between `unitLattice` and `(𝓞 K)ˣ ⧸ (torsion K)` as an additive
-`ℤ`-module. -/
-def unitLatticeEquiv : (unitLattice K) ≃ₗ[ℤ] Additive ((𝓞 K)ˣ ⧸ (torsion K)) :=
-  AddEquiv.toIntLinearEquiv <|
-    (AddEquiv.addSubgroupCongr (AddMonoidHom.range_eq_map (logEmbedding K)).symm).trans <|
-      (QuotientAddGroup.quotientKerEquivRange (logEmbedding K)).symm.trans <|
-          (QuotientAddGroup.quotientAddEquivOfEq (unitLatticeEquiv_aux1  K)).trans <|
-            QuotientAddGroup.quotientKerEquivOfSurjective
-              (MonoidHom.toAdditive (QuotientGroup.mk' (torsion K))) (unitLatticeEquiv_aux2 K)
+@[simp]
+theorem logEmbeddingEquiv_apply (x : (𝓞 K)ˣ) :
+    logEmbeddingEquiv K ⟦x⟧ = logEmbedding K x := rfl
 
 instance : Module.Free ℤ (Additive ((𝓞 K)ˣ ⧸ (torsion K))) :=
-  Module.Free.of_equiv (unitLatticeEquiv K)
+  Module.Free.of_equiv (logEmbeddingEquiv K).symm
 
 instance : Module.Finite ℤ (Additive ((𝓞 K)ˣ ⧸ (torsion K))) :=
-  Module.Finite.equiv (unitLatticeEquiv K)
+  Module.Finite.equiv (logEmbeddingEquiv K).symm
 
 -- Note that we prove this instance first and then deduce from it the instance
 -- `Monoid.FG (𝓞 K)ˣ`, and not the other way around, due to no `Subgroup` version
@@ -439,7 +451,7 @@ instance : Monoid.FG (𝓞 K)ˣ := by
 
 theorem rank_modTorsion :
     FiniteDimensional.finrank ℤ (Additive ((𝓞 K)ˣ ⧸ (torsion K))) = rank K := by
-  rw [← LinearEquiv.finrank_eq (unitLatticeEquiv K), unitLattice_rank]
+  rw [← LinearEquiv.finrank_eq (logEmbeddingEquiv K).symm, unitLattice_rank]
 
 /-- A basis of the quotient `(𝓞 K)ˣ ⧸ (torsion K)` seen as an additive ℤ-module. -/
 def basisModTorsion : Basis (Fin (rank K)) ℤ (Additive ((𝓞 K)ˣ ⧸ (torsion K))) :=
@@ -452,6 +464,12 @@ 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
+
 /-- 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
 `exist_unique_eq_mul_prod`) are given by the representation of the unit on `basisModTorsion`. -/
@@ -488,4 +506,5 @@ theorem exist_unique_eq_mul_prod (x : (𝓞 K)ˣ) : ∃! ζe : torsion K × (Fin
 
 end statements
 
+
 end NumberField.Units

Mathlib/NumberTheory/NumberField/Units/Regulator.lean

@@ -0,0 +1,110 @@
+/-
+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.Algebra.Module.Zlattice.Covolume
+import Mathlib.LinearAlgebra.Matrix.Determinant.Misc
+import Mathlib.NumberTheory.NumberField.Units.DirichletTheorem
+
+/-!
+# Regulator of a number field
+
+We define and prove basic results about the regulator of a number field `K`.
+
+## Main definitions and results
+
+* `NumberField.Units.regulator`: the regulator of the number field `K`.
+
+* `Number.Field.Units.regulator_eq_det`: For any infinite place `w'`, the regulator is equal to
+the absolute value of the determinant of the matrix `(mult w * log w (fundSystem K i)))_i, w`
+where `w` runs through the infinite places distinct from `w'`.
+
+## Tags
+number field, units, regulator
+ -/
+
+open scoped NumberField
+
+noncomputable section
+
+namespace NumberField.Units
+
+variable (K : Type*) [Field K]
+
+open MeasureTheory Classical BigOperators NumberField.InfinitePlace
+  NumberField NumberField.Units.dirichletUnitTheorem
+
+variable [NumberField K]
+
+/-- The regulator of a number fied `K`. -/
+def regulator : ℝ := Zlattice.covolume (unitLattice K)
+
+theorem regulator_ne_zero : regulator K ≠ 0 := Zlattice.covolume_ne_zero (unitLattice K) volume
+
+theorem regulator_pos : 0 < regulator K := Zlattice.covolume_pos (unitLattice K) volume
+
+#adaptation_note
+/--
+After https://github.com/leanprover/lean4/pull/4119
+the `Module ℤ (Additive ((𝓞 K)ˣ ⧸ NumberField.Units.torsion K))` instance required below isn't found
+unless we use `set_option maxSynthPendingDepth 2`, or add
+explicit instances:
+```
+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
+  simp_rw [regulator, Zlattice.covolume_eq_det _
+    (((basisModTorsion K).map (logEmbeddingEquiv K)).reindex e.symm), Basis.coe_reindex,
+    Function.comp, Basis.map_apply, ← fundSystem_mk, Equiv.symm_symm]
+  rfl
+
+/-- 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`,
+have the same determinant in absolute value. -/
+theorem abs_det_eq_abs_det (u : Fin (rank K) → (𝓞 K)ˣ)
+    {w₁ w₂ : InfinitePlace K} (e₁ : {w // w ≠ w₁} ≃ Fin (rank K))
+    (e₂ : {w // w ≠ w₂} ≃ Fin (rank K)) :
+    |(Matrix.of fun i w : {w // w ≠ w₁} ↦ (mult w.val : ℝ) * (w.val (u (e₁ i) : K)).log).det| =
+    |(Matrix.of fun i w : {w // w ≠ w₂} ↦ (mult w.val : ℝ) * (w.val (u (e₂ i) : K)).log).det| := by
+  -- We construct an equiv `Fin (rank K + 1) ≃ InfinitePlace K` from `e₂.symm`
+  let f : Fin (rank K + 1) ≃ InfinitePlace K :=
+    (finSuccEquiv _).trans ((Equiv.optionSubtype _).symm e₁.symm).val
+  -- And `g` corresponds to the restriction of `f⁻¹` to `{w // w ≠ w₂}`
+  let g : {w // w ≠ w₂} ≃ Fin (rank K) :=
+    (Equiv.subtypeEquiv f.symm (fun _ ↦ by simp [f])).trans
+      (finSuccAboveEquiv (f.symm w₂)).toEquiv.symm
+  have h_col := congr_arg abs <| Matrix.det_permute (g.trans e₂.symm)
+    (Matrix.of fun i w : {w // w ≠ w₂} ↦ (mult w.val : ℝ) * (w.val (u (e₂ i) : K)).log)
+  rw [abs_mul, ← Int.cast_abs, Equiv.Perm.sign_abs, Int.cast_one, one_mul] at h_col
+  rw [← h_col]
+  have h := congr_arg abs <| Matrix.submatrix_succAbove_det_eq_negOnePow_submatrix_succAbove_det'
+    (Matrix.of fun i w ↦ (mult (f w) : ℝ) * ((f w) (u i)).log) ?_ 0 (f.symm w₂)
+  rw [← Matrix.det_reindex_self e₁, ← Matrix.det_reindex_self g]
+  · rw [Units.smul_def, abs_zsmul, Int.abs_negOnePow, one_smul] at h
+    convert h
+    · ext; simp only [ne_eq, Matrix.reindex_apply, Matrix.submatrix_apply, Matrix.of_apply,
+        Equiv.apply_symm_apply, Equiv.trans_apply, Fin.succAbove_zero, id_eq, finSuccEquiv_succ,
+        Equiv.optionSubtype_symm_apply_apply_coe, f]
+    · ext; simp only [ne_eq, Equiv.coe_trans, Matrix.reindex_apply, Matrix.submatrix_apply,
+        Function.comp_apply, Equiv.apply_symm_apply, id_eq, Matrix.of_apply]; rfl
+  · intro _
+    simp_rw [Matrix.of_apply, ← Real.log_pow]
+    rw [← Real.log_prod, Equiv.prod_comp f (fun w ↦ (w (u _) ^ (mult w))), prod_eq_abs_norm,
+      Units.norm, Rat.cast_one, Real.log_one]
+    exact fun _ _ ↦ pow_ne_zero _ <| (map_ne_zero _).mpr (coe_ne_zero _)
+
+/-- For any infinite place `w'`, the regulator is equal to the absolute value of the determinant
+of the matrix `(mult w * log w (fundSystem K i)))_i, {w ≠ w'}`. -/
+theorem regulator_eq_det (w' : InfinitePlace K) (e : {w // w ≠ w'} ≃ Fin (rank K)) :
+    regulator K =
+      |(Matrix.of fun i w : {w // w ≠ w'} ↦ (mult w.val : ℝ) *
+        Real.log (w.val (fundSystem K (e i) : K))).det| := by
+  let e' : {w : InfinitePlace K // w ≠ w₀} ≃ Fin (rank K) := Fintype.equivOfCardEq (by
+    rw [Fintype.card_subtype_compl, Fintype.card_ofSubsingleton, Fintype.card_fin, rank])
+  simp_rw [regulator_eq_det' K e', logEmbedding, AddMonoidHom.coe_mk, ZeroHom.coe_mk]
+  exact abs_det_eq_abs_det K (fun i ↦ fundSystem K i) e' e