Integral ideals of a number field #
We prove several results about integral ideals of a number field.
Main results #
NumberField.ideal.tendsto_norm_le_and_mk_eq_div_atTop: asymptotics for the number of (nonzero) integral ideals of bounded norm in a fixed class of the class group.NumberField.ideal.tendsto_norm_le_div_atTop: asymptotics for the number of integral ideals of bounded norm.
theorem
NumberField.Ideal.tendsto_norm_le_and_mk_eq_div_atTop
(K : Type u_1)
[Field K]
[NumberField K]
(C : ClassGroup (RingOfIntegers K))
:
Filter.Tendsto
(fun (s : ℝ) =>
↑(Nat.card
{ I : ↥(nonZeroDivisors (Ideal (RingOfIntegers K))) // ↑(Ideal.absNorm ↑I) ≤ s ∧ ClassGroup.mk0 I = C }) / s)
Filter.atTop
(nhds
(2 ^ InfinitePlace.nrRealPlaces K * (2 * Real.pi) ^ InfinitePlace.nrComplexPlaces K * Units.regulator K / (↑(Units.torsionOrder K) * √|↑(discr K)|)))
The limit of the number of nonzero integral ideals of norm ≤ s in a fixed class C of the
class group divided by s when s → +∞.
theorem
NumberField.Ideal.tendsto_norm_le_div_atTop₀
(K : Type u_1)
[Field K]
[NumberField K]
:
Filter.Tendsto
(fun (s : ℝ) => ↑(Nat.card { I : ↥(nonZeroDivisors (Ideal (RingOfIntegers K))) // ↑(Ideal.absNorm ↑I) ≤ s }) / s)
Filter.atTop
(nhds
(2 ^ InfinitePlace.nrRealPlaces K * (2 * Real.pi) ^ InfinitePlace.nrComplexPlaces K * Units.regulator K * ↑(classNumber K) / (↑(Units.torsionOrder K) * √|↑(discr K)|)))
The limit of the number of nonzero integral ideals of norm ≤ s divided by s when s → +∞.
theorem
NumberField.Ideal.tendsto_norm_le_div_atTop
(K : Type u_1)
[Field K]
[NumberField K]
:
Filter.Tendsto (fun (s : ℝ) => ↑(Nat.card { I : Ideal (RingOfIntegers K) // ↑(Ideal.absNorm I) ≤ s }) / s) Filter.atTop
(nhds
(2 ^ InfinitePlace.nrRealPlaces K * (2 * Real.pi) ^ InfinitePlace.nrComplexPlaces K * Units.regulator K * ↑(classNumber K) / (↑(Units.torsionOrder K) * √|↑(discr K)|)))
The limit of the number of integral ideals of norm ≤ s divided by s when s → +∞.