Skip to content

Commit df8fb03

Browse files
xroblotxroblot
committed
feat: Prove some results on bases of fractional ideals of number fields (#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`
1 parent 8b0b0e7 commit df8fb03

File tree

3 files changed

+129
-2
lines changed

3 files changed

+129
-2
lines changed

‎Mathlib.lean‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -2827,6 +2827,7 @@ import Mathlib.NumberTheory.NumberField.CanonicalEmbedding
28272827
import Mathlib.NumberTheory.NumberField.ClassNumber
28282828
import Mathlib.NumberTheory.NumberField.Discriminant
28292829
import Mathlib.NumberTheory.NumberField.Embeddings
2830+
import Mathlib.NumberTheory.NumberField.FractionalIdeal
28302831
import Mathlib.NumberTheory.NumberField.Norm
28312832
import Mathlib.NumberTheory.NumberField.Units
28322833
import Mathlib.NumberTheory.Padics.Harmonic

‎Mathlib/NumberTheory/NumberField/FractionalIdeal.lean‎

Lines changed: 115 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,115 @@
1+
/-
2+
Copyright (c) 2024 Xavier Roblot. All rights reserved.
3+
Released under Apache 2.0 license as described in the file LICENSE.
4+
Authors: Xavier Roblot
5+
-/
6+
import Mathlib.NumberTheory.NumberField.Basic
7+
import Mathlib.RingTheory.FractionalIdeal.Norm
8+
import Mathlib.RingTheory.FractionalIdeal.Operations
9+
10+
/-!
11+
12+
# Fractional ideals of number fields
13+
14+
Prove some results on the fractional ideals of number fields.
15+
16+
## Main definitions and results
17+
18+
* `NumberField.basisOfFractionalIdeal`: A `ℚ`-basis of `K` that spans `I` over `ℤ` where `I` is
19+
a fractional ideal of a number field `K`.
20+
* `NumberField.det_basisOfFractionalIdeal_eq_absNorm`: for `I` a fractional ideal of a number
21+
field `K`, the absolute value of the determinant of the base change from `integralBasis` to
22+
`basisOfFractionalIdeal I` is equal to the norm of `I`.
23+
-/
24+
25+
variable (K : Type*) [Field K] [NumberField K]
26+
27+
namespace NumberField
28+
29+
open scoped nonZeroDivisors
30+
31+
section Basis
32+
33+
open Module
34+
35+
-- This is necessary to avoid several timeouts
36+
attribute [local instance 2000] Submodule.module
37+
38+
instance (I : FractionalIdeal (𝓞 K)⁰ K) : Module.Free ℤ I := by
39+
refine Free.of_equiv (LinearEquiv.restrictScalars ℤ (I.equivNum ?_)).symm
40+
exact nonZeroDivisors.coe_ne_zero I.den
41+
42+
instance (I : FractionalIdeal (𝓞 K)⁰ K) : Module.Finite ℤ I := by
43+
refine Module.Finite.of_surjective
44+
(LinearEquiv.restrictScalars ℤ (I.equivNum ?_)).symm.toLinearMap (LinearEquiv.surjective _)
45+
exact nonZeroDivisors.coe_ne_zero I.den
46+
47+
instance (I : (FractionalIdeal (𝓞 K)⁰ K)ˣ) :
48+
IsLocalizedModule ℤ⁰ ((Submodule.subtype (I : Submodule (𝓞 K) K)).restrictScalars ℤ) where
49+
map_units x := by
50+
rw [← (Algebra.lmul _ _).commutes, Algebra.lmul_isUnit_iff, isUnit_iff_ne_zero, eq_intCast,
51+
Int.cast_ne_zero]
52+
exact nonZeroDivisors.coe_ne_zero x
53+
surj' x := by
54+
obtain ⟨⟨a, _, d, hd, rfl⟩, h⟩ := IsLocalization.surj (Algebra.algebraMapSubmonoid (𝓞 K) ℤ⁰) x
55+
refine ⟨⟨⟨Ideal.absNorm I.1.num * a, I.1.num_le ?_⟩, d * Ideal.absNorm I.1.num, ?_⟩ , ?_⟩
56+
· simp_rw [FractionalIdeal.val_eq_coe, FractionalIdeal.coe_coeIdeal]
57+
refine (IsLocalization.mem_coeSubmodule _ _).mpr ⟨Ideal.absNorm I.1.num * a, ?_, ?_⟩
58+
· exact Ideal.mul_mem_right _ _ I.1.num.absNorm_mem
59+
· rw [map_mul, map_natCast]; rfl
60+
· refine Submonoid.mul_mem _ hd (mem_nonZeroDivisors_of_ne_zero ?_)
61+
rw [Nat.cast_ne_zero, ne_eq, Ideal.absNorm_eq_zero_iff]
62+
exact FractionalIdeal.num_eq_zero_iff.not.mpr <| Units.ne_zero I
63+
· simp_rw [LinearMap.coe_restrictScalars, Submodule.coeSubtype] at h ⊢
64+
rw [show (a : K) = algebraMap (𝓞 K) K a by rfl, ← h]
65+
simp only [Submonoid.mk_smul, zsmul_eq_mul, Int.cast_mul, Int.cast_ofNat, algebraMap_int_eq,
66+
eq_intCast, map_intCast]
67+
ring
68+
exists_of_eq h :=
69+
⟨1, by rwa [one_smul, one_smul, ← (Submodule.injective_subtype I.1.coeToSubmodule).eq_iff]⟩
70+
71+
/-- A `ℤ`-basis of a fractional ideal. -/
72+
noncomputable def fractionalIdealBasis (I : FractionalIdeal (𝓞 K)⁰ K) :
73+
Basis (Free.ChooseBasisIndex ℤ I) ℤ I := Free.chooseBasis ℤ I
74+
75+
/-- A `ℚ`-basis of `K` that spans `I` over `ℤ`, see `mem_span_basisOfFractionalIdeal` below. -/
76+
noncomputable def basisOfFractionalIdeal (I : (FractionalIdeal (𝓞 K)⁰ K)ˣ) :
77+
Basis (Free.ChooseBasisIndex ℤ I) ℚ K :=
78+
(fractionalIdealBasis K I.1).ofIsLocalizedModule ℚ ℤ⁰
79+
((Submodule.subtype (I : Submodule (𝓞 K) K)).restrictScalars ℤ)
80+
81+
theorem basisOfFractionalIdeal_apply (I : (FractionalIdeal (𝓞 K)⁰ K)ˣ)
82+
(i : Free.ChooseBasisIndex ℤ I) :
83+
basisOfFractionalIdeal K I i = fractionalIdealBasis K I.1 i :=
84+
(fractionalIdealBasis K I.1).ofIsLocalizedModule_apply ℚ ℤ⁰ _ i
85+
86+
theorem mem_span_basisOfFractionalIdeal {I : (FractionalIdeal (𝓞 K)⁰ K)ˣ} {x : K} :
87+
x ∈ Submodule.span ℤ (Set.range (basisOfFractionalIdeal K I)) ↔ x ∈ (I : Set K) := by
88+
rw [basisOfFractionalIdeal, (fractionalIdealBasis K I.1).ofIsLocalizedModule_span ℚ ℤ⁰ _]
89+
simp
90+
91+
open FiniteDimensional in
92+
theorem fractionalIdeal_rank (I : (FractionalIdeal (𝓞 K)⁰ K)ˣ) :
93+
finrank ℤ I = finrank ℤ (𝓞 K) := by
94+
rw [finrank_eq_card_chooseBasisIndex, RingOfIntegers.rank,
95+
finrank_eq_card_basis (basisOfFractionalIdeal K I)]
96+
97+
end Basis
98+
99+
section Norm
100+
101+
open Module
102+
103+
/-- The absolute value of the determinant of the base change from `integralBasis` to
104+
`basisOfFractionalIdeal I` is equal to the norm of `I`. -/
105+
theorem det_basisOfFractionalIdeal_eq_absNorm (I : (FractionalIdeal (𝓞 K)⁰ K)ˣ)
106+
(e : (Free.ChooseBasisIndex ℤ (𝓞 K)) ≃ (Free.ChooseBasisIndex ℤ I)) :
107+
|(integralBasis K).det ((basisOfFractionalIdeal K I).reindex e.symm)| =
108+
FractionalIdeal.absNorm I.1 := by
109+
rw [← FractionalIdeal.abs_det_basis_change (RingOfIntegers.basis K) I.1
110+
((fractionalIdealBasis K I.1).reindex e.symm)]
111+
congr
112+
ext
113+
simpa using basisOfFractionalIdeal_apply K I _
114+
115+
end Norm

‎Mathlib/RingTheory/FractionalIdeal/Operations.lean‎

Lines changed: 13 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -359,6 +359,10 @@ theorem coeIdeal_ne_one {I : Ideal R} : (I : FractionalIdeal R⁰ K) ≠ 1 ↔ I
359359
not_iff_not.mpr coeIdeal_eq_one
360360
#align fractional_ideal.coe_ideal_ne_one FractionalIdeal.coeIdeal_ne_one
361361

362+
theorem num_eq_zero_iff [Nontrivial R] {I : FractionalIdeal R⁰ K} : I.num = 0 ↔ I = 0 :=
363+
⟨fun h ↦ zero_of_num_eq_bot zero_not_mem_nonZeroDivisors h,
364+
fun h ↦ h ▸ num_zero_eq (IsFractionRing.injective R K)⟩
365+
362366
end IsFractionRing
363367

364368
section Quotient
@@ -569,7 +573,7 @@ theorem eq_zero_or_one_of_isField (hF : IsField R₁) (I : FractionalIdeal R₁
569573

570574
end Field
571575

572-
section PrincipalIdealRing
576+
section PrincipalIdeal
573577

574578
variable {R₁ : Type*} [CommRing R₁] {K : Type*} [Field K]
575579

@@ -886,7 +890,14 @@ theorem eq_spanSingleton_mul {x : P} {I J : FractionalIdeal S P} :
886890
simp only [le_antisymm_iff, le_spanSingleton_mul_iff, spanSingleton_mul_le_iff]
887891
#align fractional_ideal.eq_span_singleton_mul FractionalIdeal.eq_spanSingleton_mul
888892

889-
end PrincipalIdealRing
893+
theorem num_le (I : FractionalIdeal S P) :
894+
(I.num : FractionalIdeal S P) ≤ I := by
895+
rw [← I.den_mul_self_eq_num', spanSingleton_mul_le_iff]
896+
intro _ h
897+
rw [← Algebra.smul_def]
898+
exact Submodule.smul_mem _ _ h
899+
900+
end PrincipalIdeal
890901

891902
variable {R₁ : Type*} [CommRing R₁]
892903

0 commit comments

Comments
 (0)