English
If the absolute discriminant is below a certain bound depending on nrComplexPlaces(K) and the degree [K:ℚ], then 𝓞_K is a PID.
Русский
Если модуль дискриминант по абсолютному значению меньше некоторой границы, зависящей от nrComplexPlaces(K) и степени [K:ℚ], то 𝓞_K — PID.
LaTeX
$$$\left| \mathrm{discr}(K) \right| < \left( 2 \cdot (\tfrac{\pi}{4})^{nrComplexPlaces(K)} \cdot \frac{(\mathrm{finrank}\mathbb{Q}K)^{\mathrm{finrank}\mathbb{Q}K}}{(\mathrm{finrank}\mathbb{Q}K)!} \right)^{2} \Rightarrow \mathrm{IsPrincipalIdeaI}(\mathcal{O}_K)$$$
Lean4
/-- Let `K` be a number field and let `M K` be the Minkowski bound of `K`.
To show that `𝓞 K` is a PID it is enough to show that, for all (natural) primes
`p ∈ Finset.Icc 1 ⌊(M K)⌋₊`, all ideals `P` above `p` such that
`p ^ (span ({p}).inertiaDeg P) ≤ ⌊(M K)⌋₊` are principal. This is the standard technique to prove
that `𝓞 K` is principal, see [marcus1977number], discussion after Theorem 37.
If `K/ℚ` is Galois, one can use the more convenient
`RingOfIntegers.isPrincipalIdealRing_of_isPrincipal_of_lt_or_isPrincipal_of_mem_primesOver_of_mem_Icc`
below.
The way this theorem should be used is to first compute `⌊(M K)⌋₊` and then to use `fin_cases`
to deal with the finite number of primes `p` in the interval. -/
theorem isPrincipalIdealRing_of_isPrincipal_of_pow_le_of_mem_primesOver_of_mem_Icc
(h :
∀ p ∈ Finset.Icc 1 ⌊(M K)⌋₊,
p.Prime →
∀ (P : Ideal (𝓞 K)),
P ∈ primesOver (span {(p : ℤ)}) (𝓞 K) →
p ^ ((span ({↑p} : Set ℤ)).inertiaDeg P) ≤ ⌊(M K)⌋₊ → Submodule.IsPrincipal P) :
IsPrincipalIdealRing (𝓞 K) :=
by
refine isPrincipalIdealRing_of_isPrincipal_of_norm_le_of_isPrime <| fun ⟨P, HP⟩ hP hPN ↦ ?_
obtain ⟨p, hp⟩ := IsPrincipalIdealRing.principal <| under ℤ P
have hp0 : p ≠ 0 := fun h ↦
nonZeroDivisors.coe_ne_zero ⟨P, HP⟩ <|
eq_bot_of_comap_eq_bot (R := ℤ) <| by simpa only [hp, submodule_span_eq, span_singleton_eq_bot]
have hpprime := (span_singleton_prime hp0).mp
simp only [← submodule_span_eq, ← hp] at hpprime
have hlies : P.LiesOver (span { p }) := by
rcases abs_choice p with h | h <;> simpa [h, span_singleton_neg p, ← submodule_span_eq, ← hp] using over_under P
have hspan : span {↑p.natAbs} = span { p } := by rcases abs_choice p with h | h <;> simp [h]
have hple : p.natAbs ^ (span {(p.natAbs : ℤ)}).inertiaDeg P ≤ ⌊(M K)⌋₊ :=
by
refine le_floor ?_
simpa only [hspan, ← cast_pow, ← absNorm_eq_pow_inertiaDeg P (hpprime (hP.under _))] using hPN
have hpabsprime := Int.prime_iff_natAbs_prime.mp (hpprime (hP.under _))
refine h _ ?_ hpabsprime _ ⟨hP, ?_⟩ hple
· suffices 0 < (span {(p.natAbs : ℤ)}).inertiaDeg P by
exact Finset.mem_Icc.mpr ⟨hpabsprime.one_le, le_trans (le_pow this) hple⟩
have :=
(isPrime_of_prime (prime_span_singleton_iff.mpr <| hpprime (hP.under _))).isMaximal <| by
simp [((hpprime (hP.under _))).ne_zero]
exact hspan ▸ inertiaDeg_pos ..
· exact hspan ▸ hlies
