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

Mathlib/NumberTheory/NumberField/CanonicalEmbedding/FundamentalCone.lean

@@ -119,11 +119,11 @@ 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

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
@@ -381,19 +384,19 @@ theorem unitLattice_rank :
   rw [← Units.finrank_eq_rank, ZLattice.rank ℝ]
 
 /-- The map obtained by quotienting by the kernel of `logEmbedding`. -/
-def logEmbeddingQuot :
+abbrev 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
+          ← 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
@@ -477,15 +481,12 @@ def fundSystem : Fin (rank K) → (𝓞 K)ˣ :=
   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, Additive.ofMul_symm_eq]
-  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 (fundSystem K i) = basisUnitLattice K i := by
-   rw [basisUnitLattice, Basis.map_apply, ← fundSystem_mk, ← logEmbeddingEquiv_apply]
-   rfl
+    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
@@ -519,9 +520,8 @@ theorem exist_unique_eq_mul_prod (x : (𝓞 K)ˣ) : ∃! ζe : torsion K × (Fin
   · rintro ⟨⟨ζ', h_tors'⟩, η⟩ hf
     simp only [ζ, ← fun_eq_repr K h_tors' hf, Prod.mk.injEq, Subtype.mk.injEq, and_true]
     nth_rewrite 1 [hf]
-    rw [_root_.mul_inv_cancel_right]
+    with_reducible rw [_root_.mul_inv_cancel_right]
 
 end statements
 
-
 end NumberField.Units