English
Assume K/ℚ is Galois. If for every p in the Minkowski interval there exists a prime P over p with inertia-degree condition or P is principal, then 𝓞_K is a PID.
Русский
Пусть K/ℚ является галуа. Если для каждого простого p в интервале Минковского существует над p простый идеал P такой, что выполняется соответствие степени инерции или P является главным, тогда 𝓞_K — ПИД.
LaTeX
$$$\forall p \in \mathrm{Finset.Interv}(1, \lfloor M(K) \rfloor_+),\; p \text{ prime} \Rightarrow \exists P \in primesOver(\mathrm{span}\{p\})\,(\mathcal{O}_K) :\; (\lfloor M(K) \rfloor_+ < p^{( \mathrm{inertiaDeg} P)}) \lor P\text{ principal} \\Rightarrow \mathrm{IsPrincipalIdealRing}(\mathcal{O}_K)$$$
Lean4
/-- Let `K` be a number field such that `K/ℚ` is Galois 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)⌋₊`, there is an ideal `P` above `p` such that
either `⌊(M K)⌋₊ < p ^ (span ({p}).inertiaDeg P)` or `P` is principal. This is the standard
technique to prove that `𝓞 K` is principal in the Galois case, see [marcus1977number], discussion
after Theorem 37.
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_lt_or_isPrincipal_of_mem_primesOver_of_mem_Icc [IsGalois ℚ K]
(h :
∀ p ∈ Finset.Icc 1 ⌊(M K)⌋₊,
p.Prime →
∃ P ∈ primesOver (span {(p : ℤ)}) (𝓞 K),
⌊(M K)⌋₊ < p ^ ((span ({↑p} : Set ℤ)).inertiaDeg P) ∨ Submodule.IsPrincipal P) :
IsPrincipalIdealRing (𝓞 K) :=
by
refine
isPrincipalIdealRing_of_isPrincipal_of_pow_le_of_mem_primesOver_of_mem_Icc (fun p hpmem hp P ⟨hP1, hP2⟩ hple ↦ ?_)
obtain ⟨Q, ⟨hQ1, hQ2⟩, H⟩ := h p hpmem hp
have := (isPrime_of_prime (prime_span_singleton_iff.mpr (prime_iff_prime_int.mp hp))).isMaximal (by simp [hp.ne_zero])
by_cases h : ⌊(M K)⌋₊ < p ^ ((span ({↑p} : Set ℤ)).inertiaDeg P)
· linarith
rw [inertiaDeg_eq_of_isGalois _ Q P ℚ K] at H
obtain ⟨σ, rfl⟩ := exists_map_eq_of_isGalois (span ({↑p} : Set ℤ)) Q P ℚ K
exact (H.resolve_left h).map_ringHom σ
