feat: Prove some results on bases of fractional ideals of number fiel…

…ds (#9836)

- Add the instances that fractional ideals of number fields are finite and free $\mathbb{Z}$-modules
- For `I : (FractionalIdeal (𝓞 K)⁰ K)ˣ` with `K` a number field, define a basis of `K` that spans `I` over $\mathbb{Z}$
- Prove that the determinant of that basis over an integral basis of `K` is the absolute norm of `I`

Mathlib.lean

@@ -2827,6 +2827,7 @@ import Mathlib.NumberTheory.NumberField.CanonicalEmbedding
 import Mathlib.NumberTheory.NumberField.ClassNumber
 import Mathlib.NumberTheory.NumberField.Discriminant
 import Mathlib.NumberTheory.NumberField.Embeddings
+import Mathlib.NumberTheory.NumberField.FractionalIdeal
 import Mathlib.NumberTheory.NumberField.Norm
 import Mathlib.NumberTheory.NumberField.Units
 import Mathlib.NumberTheory.Padics.Harmonic

Mathlib/NumberTheory/NumberField/FractionalIdeal.lean

@@ -0,0 +1,115 @@
+/-
+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.Basic
+import Mathlib.RingTheory.FractionalIdeal.Norm
+import Mathlib.RingTheory.FractionalIdeal.Operations
+
+/-!
+
+# Fractional ideals of number fields
+
+Prove some results on the fractional ideals of number fields.
+
+## Main definitions and results
+
+  * `NumberField.basisOfFractionalIdeal`: A `ℚ`-basis of `K` that spans `I` over `ℤ` where `I` is
+  a fractional ideal of a number field `K`.
+  * `NumberField.det_basisOfFractionalIdeal_eq_absNorm`: for `I` a fractional ideal of a number
+  field `K`, the absolute value of the determinant of the base change from `integralBasis` to
+  `basisOfFractionalIdeal I` is equal to the norm of `I`.
+-/
+
+variable (K : Type*) [Field K] [NumberField K]
+
+namespace NumberField
+
+open scoped nonZeroDivisors
+
+section Basis
+
+open Module
+
+-- This is necessary to avoid several timeouts
+attribute [local instance 2000] Submodule.module
+
+instance (I : FractionalIdeal (𝓞 K)⁰ K) : Module.Free ℤ I := by
+  refine Free.of_equiv (LinearEquiv.restrictScalars ℤ (I.equivNum ?_)).symm
+  exact nonZeroDivisors.coe_ne_zero I.den
+
+instance (I : FractionalIdeal (𝓞 K)⁰ K) : Module.Finite ℤ I := by
+  refine Module.Finite.of_surjective
+    (LinearEquiv.restrictScalars ℤ (I.equivNum ?_)).symm.toLinearMap (LinearEquiv.surjective _)
+  exact nonZeroDivisors.coe_ne_zero I.den
+
+instance (I : (FractionalIdeal (𝓞 K)⁰ K)ˣ) :
+    IsLocalizedModule ℤ⁰ ((Submodule.subtype (I : Submodule (𝓞 K) K)).restrictScalars ℤ) where
+  map_units x := by
+    rw [← (Algebra.lmul _ _).commutes, Algebra.lmul_isUnit_iff, isUnit_iff_ne_zero, eq_intCast,
+      Int.cast_ne_zero]
+    exact nonZeroDivisors.coe_ne_zero x
+  surj' x := by
+    obtain ⟨⟨a, _, d, hd, rfl⟩, h⟩ := IsLocalization.surj (Algebra.algebraMapSubmonoid (𝓞 K) ℤ⁰) x
+    refine ⟨⟨⟨Ideal.absNorm I.1.num * a, I.1.num_le ?_⟩, d * Ideal.absNorm I.1.num, ?_⟩ , ?_⟩
+    · simp_rw [FractionalIdeal.val_eq_coe, FractionalIdeal.coe_coeIdeal]
+      refine (IsLocalization.mem_coeSubmodule _ _).mpr ⟨Ideal.absNorm I.1.num * a, ?_, ?_⟩
+      · exact Ideal.mul_mem_right _ _ I.1.num.absNorm_mem
+      · rw [map_mul, map_natCast]; rfl
+    · refine Submonoid.mul_mem _ hd (mem_nonZeroDivisors_of_ne_zero ?_)
+      rw [Nat.cast_ne_zero, ne_eq, Ideal.absNorm_eq_zero_iff]
+      exact FractionalIdeal.num_eq_zero_iff.not.mpr <| Units.ne_zero I
+    · simp_rw [LinearMap.coe_restrictScalars, Submodule.coeSubtype] at h ⊢
+      rw [show (a : K) = algebraMap (𝓞 K) K a by rfl, ← h]
+      simp only [Submonoid.mk_smul, zsmul_eq_mul, Int.cast_mul, Int.cast_ofNat, algebraMap_int_eq,
+        eq_intCast, map_intCast]
+      ring
+  exists_of_eq h :=
+    ⟨1, by rwa [one_smul, one_smul, ← (Submodule.injective_subtype I.1.coeToSubmodule).eq_iff]⟩
+
+/-- A `ℤ`-basis of a fractional ideal. -/
+noncomputable def fractionalIdealBasis (I : FractionalIdeal (𝓞 K)⁰ K) :
+    Basis (Free.ChooseBasisIndex ℤ I) ℤ I := Free.chooseBasis ℤ I
+
+/-- A `ℚ`-basis of `K` that spans `I` over `ℤ`, see `mem_span_basisOfFractionalIdeal` below. -/
+noncomputable def basisOfFractionalIdeal (I : (FractionalIdeal (𝓞 K)⁰ K)ˣ) :
+    Basis (Free.ChooseBasisIndex ℤ I) ℚ K :=
+  (fractionalIdealBasis K I.1).ofIsLocalizedModule ℚ ℤ⁰
+    ((Submodule.subtype (I : Submodule (𝓞 K) K)).restrictScalars ℤ)
+
+theorem basisOfFractionalIdeal_apply (I : (FractionalIdeal (𝓞 K)⁰ K)ˣ)
+    (i : Free.ChooseBasisIndex ℤ I) :
+    basisOfFractionalIdeal K I i = fractionalIdealBasis K I.1 i :=
+  (fractionalIdealBasis K I.1).ofIsLocalizedModule_apply ℚ ℤ⁰ _ i
+
+theorem mem_span_basisOfFractionalIdeal {I : (FractionalIdeal (𝓞 K)⁰ K)ˣ} {x : K} :
+    x ∈ Submodule.span ℤ (Set.range (basisOfFractionalIdeal K I)) ↔ x ∈ (I : Set K) := by
+  rw [basisOfFractionalIdeal, (fractionalIdealBasis K I.1).ofIsLocalizedModule_span ℚ ℤ⁰ _]
+  simp
+
+open FiniteDimensional in
+theorem fractionalIdeal_rank (I : (FractionalIdeal (𝓞 K)⁰ K)ˣ) :
+    finrank ℤ I = finrank ℤ (𝓞 K) := by
+  rw [finrank_eq_card_chooseBasisIndex, RingOfIntegers.rank,
+    finrank_eq_card_basis (basisOfFractionalIdeal K I)]
+
+end Basis
+
+section Norm
+
+open Module
+
+/-- The absolute value of the determinant of the base change from `integralBasis` to
+`basisOfFractionalIdeal I` is equal to the norm of `I`. -/
+theorem det_basisOfFractionalIdeal_eq_absNorm  (I : (FractionalIdeal (𝓞 K)⁰ K)ˣ)
+    (e : (Free.ChooseBasisIndex ℤ (𝓞 K)) ≃ (Free.ChooseBasisIndex ℤ I)) :
+    |(integralBasis K).det ((basisOfFractionalIdeal K I).reindex e.symm)| =
+      FractionalIdeal.absNorm I.1 := by
+  rw [← FractionalIdeal.abs_det_basis_change (RingOfIntegers.basis K) I.1
+    ((fractionalIdealBasis K I.1).reindex e.symm)]
+  congr
+  ext
+  simpa using basisOfFractionalIdeal_apply K I _
+
+end Norm

Mathlib/RingTheory/FractionalIdeal/Operations.lean

@@ -359,6 +359,10 @@ theorem coeIdeal_ne_one {I : Ideal R} : (I : FractionalIdeal R⁰ K) ≠ 1 ↔ I
   not_iff_not.mpr coeIdeal_eq_one
 #align fractional_ideal.coe_ideal_ne_one FractionalIdeal.coeIdeal_ne_one
 
+theorem num_eq_zero_iff [Nontrivial R] {I : FractionalIdeal R⁰ K} : I.num = 0 ↔ I = 0 :=
+   ⟨fun h ↦ zero_of_num_eq_bot zero_not_mem_nonZeroDivisors h,
+     fun h ↦ h ▸ num_zero_eq (IsFractionRing.injective R K)⟩
+
 end IsFractionRing
 
 section Quotient
@@ -569,7 +573,7 @@ theorem eq_zero_or_one_of_isField (hF : IsField R₁) (I : FractionalIdeal R₁
 
 end Field
 
-section PrincipalIdealRing
+section PrincipalIdeal
 
 variable {R₁ : Type*} [CommRing R₁] {K : Type*} [Field K]
 
@@ -886,7 +890,14 @@ theorem eq_spanSingleton_mul {x : P} {I J : FractionalIdeal S P} :
   simp only [le_antisymm_iff, le_spanSingleton_mul_iff, spanSingleton_mul_le_iff]
 #align fractional_ideal.eq_span_singleton_mul FractionalIdeal.eq_spanSingleton_mul
 
-end PrincipalIdealRing
+theorem num_le (I : FractionalIdeal S P) :
+    (I.num : FractionalIdeal S P) ≤ I := by
+  rw [← I.den_mul_self_eq_num', spanSingleton_mul_le_iff]
+  intro _ h
+  rw [← Algebra.smul_def]
+  exact Submodule.smul_mem _ _ h
+
+end PrincipalIdeal
 
 variable {R₁ : Type*} [CommRing R₁]