feat: Add exists_ideal_in_class_of_norm_le (#9084)

Prove that each class of the classgroup of a number field contains an integral ideal of small norm.

Mathlib/LinearAlgebra/Matrix/Basis.lean

@@ -165,6 +165,16 @@ def toMatrixEquiv [Fintype ι] (e : Basis ι R M) : (ι → M) ≃ₗ[R] Matrix
       LinearEquiv.apply_symm_apply]
 #align basis.to_matrix_equiv Basis.toMatrixEquiv
 
+variable (R₂) in
+theorem restrictScalars_toMatrix [Fintype ι] [DecidableEq ι] {S : Type*} [CommRing S] [Nontrivial S]
+    [Algebra R₂ S] [Module S M₂] [IsScalarTower R₂ S M₂] [NoZeroSMulDivisors R₂ S]
+    (b : Basis ι S M₂) (v : ι → span R₂ (Set.range b)) :
+    (algebraMap R₂ S).mapMatrix ((b.restrictScalars R₂).toMatrix v) =
+      b.toMatrix (fun i ↦ (v i : M₂)) := by
+  ext
+  rw [RingHom.mapMatrix_apply, Matrix.map_apply, Basis.toMatrix_apply,
+    Basis.restrictScalars_repr_apply, Basis.toMatrix_apply]
+
 end Basis
 
 section MulLinearMapToMatrix

Mathlib/NumberTheory/NumberField/Basic.lean

@@ -170,6 +170,11 @@ theorem integralBasis_apply (i : Free.ChooseBasisIndex ℤ (𝓞 K)) :
   Basis.localizationLocalization_apply ℚ (nonZeroDivisors ℤ) K (RingOfIntegers.basis K) i
 #align number_field.integral_basis_apply NumberField.integralBasis_apply
 
+@[simp]
+theorem integralBasis_repr_apply (x : (𝓞 K)) (i : Free.ChooseBasisIndex ℤ (𝓞 K)):
+    (integralBasis K).repr x i = (algebraMap ℤ ℚ) ((RingOfIntegers.basis K).repr x i) :=
+  Basis.localizationLocalization_repr_algebraMap ℚ (nonZeroDivisors ℤ) K _ x i
+
 theorem mem_span_integralBasis {x : K} :
     x ∈ Submodule.span ℤ (Set.range (integralBasis K)) ↔ x ∈ 𝓞 K := by
   rw [integralBasis, Basis.localizationLocalization_span, Subalgebra.range_isScalarTower_toAlgHom,

Mathlib/NumberTheory/NumberField/ClassNumber.lean

@@ -5,7 +5,7 @@ Authors: Anne Baanen
 -/
 import Mathlib.NumberTheory.ClassNumber.AdmissibleAbs
 import Mathlib.NumberTheory.ClassNumber.Finite
-import Mathlib.NumberTheory.NumberField.Basic
+import Mathlib.NumberTheory.NumberField.Discriminant
 
 #align_import number_theory.number_field.class_number from "leanprover-community/mathlib"@"d0259b01c82eed3f50390a60404c63faf9e60b1f"
 
@@ -45,6 +45,52 @@ theorem classNumber_eq_one_iff : classNumber K = 1 ↔ IsPrincipalIdealRing (rin
   card_classGroup_eq_one_iff
 #align number_field.class_number_eq_one_iff NumberField.classNumber_eq_one_iff
 
+open FiniteDimensional NumberField.InfinitePlace
+
+open scoped nonZeroDivisors Real
+
+theorem exists_ideal_in_class_of_norm_le (C : ClassGroup (𝓞 K)):
+    ∃ I : (Ideal (𝓞 K))⁰, ClassGroup.mk0 I = C ∧
+      Ideal.absNorm (I : Ideal (𝓞 K)) ≤ (4 / π) ^ NrComplexPlaces K *
+        ((finrank ℚ K).factorial / (finrank ℚ K) ^ (finrank ℚ K) * Real.sqrt |discr K|) := by
+  obtain ⟨J, hJ⟩ := ClassGroup.mk0_surjective C⁻¹
+  obtain ⟨_, ⟨a, ha, rfl⟩, h_nz, h_nm⟩ :=
+    exists_ne_zero_mem_ideal_of_norm_le_mul_sqrt_discr K (FractionalIdeal.mk0 K J)
+  obtain ⟨I₀, hI⟩ := Ideal.dvd_iff_le.mpr ((Ideal.span_singleton_le_iff_mem J).mpr (by convert ha))
+  have : I₀ ≠ 0 := by
+    contrapose! h_nz
+    rw [h_nz, mul_zero, show 0 = (⊥ : Ideal (𝓞 K)) by rfl, Ideal.span_singleton_eq_bot] at hI
+    rw [Algebra.linearMap_apply, hI, map_zero]
+  let I := (⟨I₀, mem_nonZeroDivisors_iff_ne_zero.mpr this⟩ : (Ideal (𝓞 K))⁰)
+  refine ⟨I, ?_, ?_⟩
+  · suffices ClassGroup.mk0 I = (ClassGroup.mk0 J)⁻¹ by rw [this, hJ, inv_inv]
+    exact ClassGroup.mk0_eq_mk0_inv_iff.mpr ⟨a, Subtype.ne_of_val_ne h_nz, by rw [mul_comm, hI]⟩
+  · rw [← FractionalIdeal.absNorm_span_singleton (𝓞 K), Algebra.linearMap_apply,
+      ← FractionalIdeal.coeIdeal_span_singleton, FractionalIdeal.coeIdeal_absNorm, hI, map_mul,
+      Nat.cast_mul, Rat.cast_mul, show Ideal.absNorm I₀ = Ideal.absNorm (I : Ideal (𝓞 K)) by rfl,
+      Rat.cast_coe_nat, Rat.cast_coe_nat, FractionalIdeal.coe_mk0,
+      FractionalIdeal.coeIdeal_absNorm, Rat.cast_coe_nat, mul_div_assoc, mul_assoc, mul_assoc]
+      at h_nm
+    refine le_of_mul_le_mul_of_pos_left h_nm ?_
+    exact Nat.cast_pos.mpr <| Nat.pos_of_ne_zero <| Ideal.absNorm_ne_zero_of_nonZeroDivisors J
+
+theorem _root_.RingOfIntegers.isPrincipalIdealRing_of_abs_discr_lt
+    (h : |discr K| < (2 * (π / 4) ^ NrComplexPlaces K *
+      ((finrank ℚ K) ^ (finrank ℚ K) / (finrank ℚ K).factorial)) ^ 2) :
+    IsPrincipalIdealRing (ringOfIntegers K) := by
+  have : 0 < finrank ℚ K := finrank_pos -- Lean needs to know that for positivity to succeed
+  rw [← Real.sqrt_lt (by positivity) (by positivity), mul_assoc, ← inv_mul_lt_iff' (by positivity),
+    mul_inv, ← inv_pow, inv_div, inv_div, mul_assoc, Int.cast_abs] at h
+  rw [← classNumber_eq_one_iff, classNumber, Fintype.card_eq_one_iff]
+  refine ⟨1, fun C ↦ ?_⟩
+  obtain ⟨I, rfl, hI⟩ := exists_ideal_in_class_of_norm_le C
+  have : Ideal.absNorm I.1 = 1 := by
+    refine le_antisymm (Nat.lt_succ.mp ?_) (Nat.one_le_iff_ne_zero.mpr
+      (Ideal.absNorm_ne_zero_of_nonZeroDivisors I))
+    exact Nat.cast_lt.mp <| lt_of_le_of_lt hI h
+  rw [ClassGroup.mk0_eq_one_iff, Ideal.absNorm_eq_one_iff.mp this]
+  exact top_isPrincipal
+
 end NumberField
 
 namespace Rat

Mathlib/RingTheory/ClassGroup.lean

@@ -415,6 +415,16 @@ theorem ClassGroup.mk0_eq_one_iff [IsDedekindDomain R] {I : Ideal R} (hI : I ∈
   ClassGroup.mk_eq_one_iff.trans (coeSubmodule_isPrincipal R _)
 #align class_group.mk0_eq_one_iff ClassGroup.mk0_eq_one_iff
 
+theorem ClassGroup.mk0_eq_mk0_inv_iff [IsDedekindDomain R] {I J : (Ideal R)⁰} :
+    ClassGroup.mk0 I = (ClassGroup.mk0 J)⁻¹ ↔
+      ∃ x ≠ (0 : R), I * J = Ideal.span {x} := by
+  rw [eq_inv_iff_mul_eq_one, ← _root_.map_mul, ClassGroup.mk0_eq_one_iff,
+    Submodule.isPrincipal_iff, Submonoid.coe_mul]
+  refine ⟨fun ⟨a, ha⟩ ↦ ⟨a, ?_, ha⟩, fun ⟨a, _, ha⟩ ↦ ⟨a, ha⟩⟩
+  by_contra!
+  rw [this, Submodule.span_zero_singleton] at ha
+  exact nonZeroDivisors.coe_ne_zero _ <| J.prop _ ha
+
 /-- The class group of principal ideal domain is finite (in fact a singleton).
 
 See `ClassGroup.fintypeOfAdmissibleOfFinite` for a finiteness proof that works for rings of integers

Mathlib/RingTheory/Ideal/Norm.lean

@@ -408,6 +408,9 @@ theorem absNorm_eq_zero_iff {I : Ideal S} : Ideal.absNorm I = 0 ↔ I = ⊥ := b
   · rintro rfl
     exact absNorm_bot
 
+theorem absNorm_ne_zero_of_nonZeroDivisors (I : (Ideal S)⁰) : Ideal.absNorm (I : Ideal S) ≠ 0 :=
+  Ideal.absNorm_eq_zero_iff.not.mpr <| nonZeroDivisors.coe_ne_zero _
+
 theorem irreducible_of_irreducible_absNorm {I : Ideal S} (hI : Irreducible (Ideal.absNorm I)) :
     Irreducible I :=
   irreducible_iff.mpr