Theorems · Theorem · number theory

RingOfIntegers.isPrincipalIdealRing_of_isPrincipal_of_pow_le_of_mem_primesOver_of_mem_Icc

∀ {K : Type u_1} [inst : Field K] [inst_1 : NumberField K],
  (∀
      p ∈
        Finset.Icc 1
          ⌊(4 / Real.pi) ^ NumberField.InfinitePlace.nrComplexPlaces K *
              (↑(Module.finrank ℚ K).factorial / ↑(Module.finrank ℚ K) ^ Module.finrank ℚ K *
                √|↑(NumberField.discr K)|)⌋₊,
      Nat.Prime p →
        ∀ P ∈ (Ideal.span {↑p}).primesOver (NumberField.RingOfIntegers K),
          p ^ P.inertiaDeg ℤ ≤
              ⌊(4 / Real.pi) ^ NumberField.InfinitePlace.nrComplexPlaces K *
                  (↑(Module.finrank ℚ K).factorial / ↑(Module.finrank ℚ K) ^ Module.finrank ℚ K *
                    √|↑(NumberField.discr K)|)⌋₊ →
            Submodule.IsPrincipal P) →
    IsPrincipalIdealRing (NumberField.RingOfIntegers K)

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.

Defined in

Mathlib.NumberTheory.NumberField.ClassNumber

Cited by

1 results in Mathlib

Foundations

Depth 316 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

FieldNumberField