feat(NumberField/CanonicalEmbedding/FundamentalCone): Prove equivalen…

…ce with principal ideals (#12333)

We prove that there is an equiv between the nonzero integral points in the fundamental cone and the nonzero integral ideals of `K` and that this equiv preserves norm. 

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



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

Mathlib/NumberTheory/NumberField/CanonicalEmbedding/FundamentalCone.lean

@@ -3,6 +3,7 @@ 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.RingTheory.Ideal.IsPrincipal
 import Mathlib.NumberTheory.NumberField.Units.DirichletTheorem
 
 /-!
@@ -25,6 +26,14 @@ domain for the action of `(𝓞 K)ˣ` modulo torsion, see `exists_unit_smul_mem`
 * `NumberField.mixedEmbedding.fundamentalCone.integralPoint`: the subset of elements of the
 fundamental cone that are images of algebraic integers of `K`.
 
+* `NumberField.mixedEmbedding.fundamentalCone.integralPointEquiv`: the equivalence between
+`fundamentalCone.integralPoint K` and the principal nonzero ideals of `𝓞 K` times the
+torsion of `K`.
+
+* `NumberField.mixedEmbedding.fundamentalCone.card_isPrincipal_norm_eq_mul_torsion`: the number of
+principal nonzero ideals in `𝓞 K` of norm `n` multiplied by the order of the torsion of `K` is
+equal to the number of `fundamentalCone.integralPoint K` of norm `n`.
+
 ## Tags
 
 number field, canonical embedding, units, principal ideals
@@ -262,8 +271,10 @@ theorem integralPoint_ne_zero (a : integralPoint K) :  (a : mixedSpace K) ≠ 0
 
 open scoped nonZeroDivisors
 
-/-- For `a : integralPoint K`, the unique nonzero algebraic integer whose image by
-`mixedEmbedding` is equal to `a`, see `mixedEmbedding_preimageOfIntegralPoint`. -/
+/-- For `a : fundamentalCone K`, the unique nonzero algebraic integer `x` such that its image by
+`mixedEmbedding` is equal to `a`. Note that we state the fact that `x ≠ 0` by saying that `x` is
+a nonzero divisors since we will use later on the isomorphism
+`Ideal.associatesNonZeroDivisorsEquivIsPrincipal`, see `integralPointEquiv`. -/
 def preimageOfIntegralPoint (a : integralPoint K) : (𝓞 K)⁰ :=
   ⟨(mem_integralPoint.mp a.prop).2.choose, mem_nonZeroDivisors_of_ne_zero (by
   simp_rw [ne_eq, ← RingOfIntegers.coe_injective.eq_iff, ← (mixedEmbedding_injective K).eq_iff,
@@ -330,6 +341,160 @@ def quotIntNorm :
 @[simp]
 theorem quotIntNorm_apply (a : integralPoint K) : quotIntNorm ⟦a⟧ = intNorm a := rfl
 
+variable (K) in
+/-- The map that sends an element of `a : integralPoint K` to the associates class
+of its preimage in `(𝓞 K)⁰`. By quotienting by the kernel of the map, which is equal to the
+subgroup of torsion, we get the equivalence `integralPointQuotEquivAssociates`. -/
+def integralPointToAssociates (a : integralPoint K) : Associates (𝓞 K)⁰ :=
+  ⟦preimageOfIntegralPoint a⟧
+
+@[simp]
+theorem integralPointToAssociates_apply (a : integralPoint K) :
+    integralPointToAssociates K a = ⟦preimageOfIntegralPoint a⟧ := rfl
+
+variable (K) in
+theorem integralPointToAssociates_surjective :
+    Function.Surjective (integralPointToAssociates K) := by
+  rintro ⟨x⟩
+  obtain ⟨u, hu⟩ : ∃ u : (𝓞 K)ˣ, u • mixedEmbedding K (x : 𝓞 K) ∈ integralPoint K := by
+    refine exists_unitSMul_mem_integralPoint ?_ ⟨(x : 𝓞 K), Set.mem_range_self _, rfl⟩
+    exact (map_ne_zero _).mpr <| RingOfIntegers.coe_ne_zero_iff.mpr (nonZeroDivisors.coe_ne_zero _)
+  refine ⟨⟨u • mixedEmbedding K (x : 𝓞 K), hu⟩,
+    Quotient.sound ⟨unitsNonZeroDivisorsEquiv.symm u⁻¹, ?_⟩⟩
+  simp_rw [Subtype.ext_iff, RingOfIntegers.ext_iff, ← (mixedEmbedding_injective K).eq_iff,
+    Submonoid.coe_mul, map_mul, mixedEmbedding_preimageOfIntegralPoint,
+    unitSMul_smul, ← map_mul, mul_comm, map_inv, val_inv_unitsNonZeroDivisorsEquiv_symm_apply_coe,
+    Units.mul_inv_cancel_right]
+
+theorem integralPointToAssociates_eq_iff (a b : integralPoint K) :
+    integralPointToAssociates K a = integralPointToAssociates K b ↔
+      ∃ ζ : torsion K, ζ • a = b := by
+  simp_rw [integralPointToAssociates_apply, Associates.quotient_mk_eq_mk,
+    Associates.mk_eq_mk_iff_associated, Associated, mul_comm, Subtype.ext_iff,
+    RingOfIntegers.ext_iff, ← (mixedEmbedding_injective K).eq_iff, Submonoid.coe_mul, map_mul,
+    mixedEmbedding_preimageOfIntegralPoint, integralPoint_torsionSMul_smul_coe]
+  refine ⟨fun ⟨u, h⟩ ↦  ⟨⟨unitsNonZeroDivisorsEquiv u, ?_⟩, by simpa using h⟩,
+    fun ⟨⟨u, _⟩, h⟩ ↦ ⟨unitsNonZeroDivisorsEquiv.symm u, by simpa using h⟩⟩
+  exact (unit_smul_mem_iff_mem_torsion a.prop.1 _).mp (by simpa [h] using b.prop.1)
+
+variable (K) in
+/-- The equivalence between `integralPoint K` modulo `torsion K` and `Associates (𝓞 K)⁰`. -/
+def integralPointQuotEquivAssociates :
+    Quotient (MulAction.orbitRel (torsion K) (integralPoint K)) ≃ Associates (𝓞 K)⁰ :=
+  Equiv.ofBijective
+    (Quotient.lift (integralPointToAssociates K)
+      fun _ _ h ↦ ((integralPointToAssociates_eq_iff _ _).mpr h).symm)
+    ⟨by convert Setoid.ker_lift_injective (integralPointToAssociates K)
+        all_goals
+        · ext a b
+          rw [Setoid.ker_def, eq_comm, integralPointToAssociates_eq_iff b a,
+            MulAction.orbitRel_apply, MulAction.mem_orbit_iff],
+        (Quot.surjective_lift _).mpr (integralPointToAssociates_surjective K)⟩
+
+@[simp]
+theorem integralPointQuotEquivAssociates_apply (a : integralPoint K) :
+    integralPointQuotEquivAssociates K ⟦a⟧ = ⟦preimageOfIntegralPoint a⟧ := rfl
+
+theorem integralPoint_torsionSMul_stabilizer (a : integralPoint K) :
+    MulAction.stabilizer (torsion K) a = ⊥ := by
+  refine (Subgroup.eq_bot_iff_forall _).mpr fun ζ hζ ↦ ?_
+  rwa [MulAction.mem_stabilizer_iff, Subtype.ext_iff, integralPoint_torsionSMul_smul_coe,
+    unitSMul_smul, ← mixedEmbedding_preimageOfIntegralPoint, ← map_mul,
+    (mixedEmbedding_injective K).eq_iff, ← map_mul, ← RingOfIntegers.ext_iff, mul_eq_right₀,
+    Units.val_eq_one, OneMemClass.coe_eq_one] at hζ
+  exact nonZeroDivisors.coe_ne_zero _
+
+open Submodule Ideal
+
+variable (K) in
+/-- The equivalence between `integralPoint K` and the product of the set of nonzero principal
+ideals of `K` and the torsion of `K`. -/
+def integralPointEquiv :
+    integralPoint K ≃ {I : (Ideal (𝓞 K))⁰ // IsPrincipal I.val} × torsion K :=
+  (MulAction.selfEquivSigmaOrbitsQuotientStabilizer (torsion K) (integralPoint K)).trans
+    ((Equiv.sigmaEquivProdOfEquiv (by
+        intro _
+        simp_rw [integralPoint_torsionSMul_stabilizer]
+        exact QuotientGroup.quotientBot.toEquiv)).trans
+      (Equiv.prodCongrLeft (fun _ ↦ (integralPointQuotEquivAssociates K).trans
+        (Ideal.associatesNonZeroDivisorsEquivIsPrincipal (𝓞 K)))))
+
+@[simp]
+theorem integralPointEquiv_apply_fst (a : integralPoint K) :
+    ((integralPointEquiv K a).1 : Ideal (𝓞 K)) = span {(preimageOfIntegralPoint a : 𝓞 K)} := rfl
+
+variable (K) in
+/-- For an integer `n`, The equivalence between the `integralPoint K` of norm `n` and the product
+of the set of nonzero principal ideals of `K` of norm `n` and the torsion of `K`. -/
+def integralPointEquivNorm (n : ℕ) :
+    {a : integralPoint K // intNorm a = n} ≃
+      {I : (Ideal (𝓞 K))⁰ // IsPrincipal (I : Ideal (𝓞 K)) ∧
+        absNorm (I : Ideal (𝓞 K)) = n} × (torsion K) :=
+  calc {a // intNorm a = n}
+      ≃ {I : {I : (Ideal (𝓞 K))⁰ // IsPrincipal I.1} × torsion K //
+          absNorm (I.1 : Ideal (𝓞 K)) = n} :=
+      (Equiv.subtypeEquiv (integralPointEquiv K) fun _ ↦ by simp [intNorm, absNorm_span_singleton])
+    _ ≃ {I : {I : (Ideal (𝓞 K))⁰ // IsPrincipal I.1} // absNorm (I.1 : Ideal (𝓞 K)) = n} ×
+          torsion K :=
+      Equiv.prodSubtypeFstEquivSubtypeProd (p := fun I : {I : (Ideal (𝓞 K))⁰ // IsPrincipal I.1} ↦
+        absNorm (I : Ideal (𝓞 K)) = n)
+    _ ≃ {I : (Ideal (𝓞 K))⁰ // IsPrincipal (I : Ideal (𝓞 K)) ∧
+          absNorm (I : Ideal (𝓞 K)) = n} × (torsion K) :=
+      Equiv.prodCongrLeft fun _ ↦ (Equiv.subtypeSubtypeEquivSubtypeInter
+        (fun I : (Ideal (𝓞 K))⁰ ↦ IsPrincipal I.1) (fun I ↦ absNorm I.1 = n))
+
+@[simp]
+theorem integralPointEquivNorm_apply_fst {n : ℕ} {a : integralPoint K} (ha : intNorm a = n) :
+    ((integralPointEquivNorm K n ⟨a, ha⟩).1 : Ideal (𝓞 K)) =
+      span {(preimageOfIntegralPoint a : 𝓞 K)} := by
+  simp_rw [integralPointEquivNorm, Equiv.prodSubtypeFstEquivSubtypeProd, Equiv.instTrans_trans,
+    Equiv.prodCongrLeft, Equiv.trans_apply, Equiv.subtypeEquiv_apply, Equiv.coe_fn_mk,
+    Equiv.subtypeSubtypeEquivSubtypeInter_apply_coe, integralPointEquiv_apply_fst]
+
+variable (K)
+
+/-- For `n` positive, the number of principal ideals in `𝓞 K` of norm `n` multiplied by the order
+of the torsion of `K` is equal to the number of `integralPoint K` of norm `n`. -/
+theorem card_isPrincipal_norm_eq_mul_torsion (n : ℕ) :
+    Nat.card {I : (Ideal (𝓞 K))⁰ | IsPrincipal (I : Ideal (𝓞 K)) ∧
+      absNorm (I : Ideal (𝓞 K)) = n} * torsionOrder K =
+        Nat.card {a : integralPoint K | intNorm a = n} := by
+  rw [torsionOrder, PNat.mk_coe, ← Nat.card_eq_fintype_card, ← Nat.card_prod]
+  exact Nat.card_congr (integralPointEquivNorm K n).symm
+
+/-- For `s : ℝ`, the number of principal nonzero ideals in `𝓞 K` of norm `≤ s` multiplied by the
+order of the torsion of `K` is equal to the number of `integralPoint K` of norm `≤ s`. -/
+theorem card_isPrincipal_norm_le_mul_torsion (s : ℝ) :
+    Nat.card {I : (Ideal (𝓞 K))⁰ | IsPrincipal (I : Ideal (𝓞 K)) ∧
+      absNorm (I : Ideal (𝓞 K)) ≤ s} * torsionOrder K =
+        Nat.card {a : integralPoint K | intNorm a ≤ s} := by
+  obtain hs | hs := le_or_gt 0 s
+  · simp_rw [← Nat.le_floor_iff hs]
+    rw [torsionOrder, PNat.mk_coe, ← Nat.card_eq_fintype_card, ← Nat.card_prod]
+    refine Nat.card_congr <| @Equiv.ofFiberEquiv _ (γ := Finset.Iic _) _
+      (fun I ↦ ⟨absNorm (I.1 : Ideal (𝓞 K)), Finset.mem_Iic.mpr I.1.2.2⟩)
+      (fun a ↦ ⟨intNorm a.1, Finset.mem_Iic.mpr a.2⟩) fun ⟨i, hi⟩ ↦ ?_
+    simp_rw [Subtype.mk.injEq]
+    calc
+    _ ≃ {I : {I : (Ideal (𝓞 K))⁰ // IsPrincipal I.1 ∧ absNorm I.1 ≤ _} // absNorm I.1.1 = i}
+          × torsion K := Equiv.prodSubtypeFstEquivSubtypeProd
+    _ ≃ {I : (Ideal (𝓞 K))⁰ // (IsPrincipal I.1 ∧ absNorm I.1 ≤ _) ∧ absNorm I.1 = i}
+          × torsion K :=
+      Equiv.prodCongrLeft fun _ ↦ (Equiv.subtypeSubtypeEquivSubtypeInter
+        (p := fun I : (Ideal (𝓞 K))⁰ ↦ IsPrincipal I.1 ∧ absNorm I.1 ≤ _)
+        (q := fun I ↦ absNorm I.1 = i))
+    _ ≃ {I : (Ideal (𝓞 K))⁰ // IsPrincipal I.1 ∧ absNorm I.1 = i ∧ absNorm I.1 ≤ _}
+          × torsion K :=
+      Equiv.prodCongrLeft fun _ ↦ (Equiv.subtypeEquivRight fun _ ↦ by aesop)
+    _ ≃ {I : (Ideal (𝓞 K))⁰ // IsPrincipal I.1 ∧ absNorm I.1 = i} × torsion K :=
+      Equiv.prodCongrLeft fun _ ↦ (Equiv.subtypeEquivRight fun _ ↦ by
+      rw [and_iff_left_of_imp (a := absNorm _ = _) fun h ↦ Finset.mem_Iic.mp (h ▸ hi)])
+    _ ≃ {a : integralPoint K // intNorm a = i} := (integralPointEquivNorm K i).symm
+    _ ≃ {a : {a : integralPoint K // intNorm a ≤ _} // intNorm a.1 = i} :=
+      (Equiv.subtypeSubtypeEquivSubtype fun h ↦ Finset.mem_Iic.mp (h ▸ hi)).symm
+  · simp_rw [lt_iff_not_le.mp (lt_of_lt_of_le hs (Nat.cast_nonneg _)), and_false, Set.setOf_false,
+      Nat.card_eq_fintype_card, Fintype.card_ofIsEmpty, zero_mul]
+
 end fundamentalCone
 
 end