Class numbers of number fields

This file defines the class number of a number field as the (finite) cardinality of the class group of its ring of integers. It also proves some elementary results on the class number.

Main definitions

We denote by M K the Minkowski bound of a number field K, defined as (4 / π) ^ nrComplexPlaces K * ((finrank ℚ K)! / (finrank ℚ K) ^ (finrank ℚ K) * √|discr K|).

• NumberField.classNumber: the class number of a number field is the (finite) cardinality of the class group of its ring of integers
• isPrincipalIdealRing_of_isPrincipal_of_pow_le_of_mem_primesOver_of_mem_Icc: let K be a number field. 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 [MS77], 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.
• isPrincipalIdealRing_of_isPrincipal_of_lt_or_isPrincipal_of_mem_primesOver_of_mem_Icc: let K be a number field such that K/ℚ is Galois. 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 [MS77], 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.

noncomputable instance NumberField.RingOfIntegers.instFintypeClassGroup (K : Type u_1) [Field K] [NumberField K] : Fintype (ClassGroup (RingOfIntegers K))

Equations

• NumberField.RingOfIntegers.instFintypeClassGroup K = ClassGroup.fintypeOfAdmissibleOfFinite ℚ K AbsoluteValue.absIsAdmissible

noncomputable def NumberField.classNumber (K : Type u_1) [Field K] [NumberField K] : ℕ

The class number of a number field is the (finite) cardinality of the class group.

Equations

• NumberField.classNumber K = Fintype.card (ClassGroup (NumberField.RingOfIntegers K))

theorem NumberField.classNumber_ne_zero (K : Type u_1) [Field K] [NumberField K] : classNumber K ≠ 0

theorem NumberField.classNumber_pos (K : Type u_1) [Field K] [NumberField K] : 0 < classNumber K

theorem NumberField.classNumber_eq_one_iff {K : Type u_1} [Field K] [NumberField K] : classNumber K = 1 ↔ IsPrincipalIdealRing (RingOfIntegers K)

The class number of a number field is 1 iff the ring of integers is a PID.

theorem NumberField.exists_ideal_in_class_of_norm_le {K : Type u_1} [Field K] [NumberField K] (C : ClassGroup (RingOfIntegers K)) : ∃ (I : ↥(nonZeroDivisors (Ideal (RingOfIntegers K)))), ClassGroup.mk0 I = C ∧ ↑(Ideal.absNorm ↑I) ≤ (4 / Real.pi) ^ InfinitePlace.nrComplexPlaces K * (↑(Module.finrank ℚ K).factorial / ↑(Module.finrank ℚ K) ^ Module.finrank ℚ K * √|↑(discr K)|)

theorem RingOfIntegers.isPrincipalIdealRing_of_isPrincipal_of_norm_le {K : Type u_1} [Field K] [NumberField K] (h : ∀ ⦃I : ↥(nonZeroDivisors (Ideal (NumberField.RingOfIntegers K)))⦄, ↑(Ideal.absNorm ↑I) ≤ (4 / Real.pi) ^ NumberField.InfinitePlace.nrComplexPlaces K * (↑(Module.finrank ℚ K).factorial / ↑(Module.finrank ℚ K) ^ Module.finrank ℚ K * √|↑(NumberField.discr K)|) → Submodule.IsPrincipal ↑I) : IsPrincipalIdealRing (NumberField.RingOfIntegers K)

theorem RingOfIntegers.isPrincipalIdealRing_of_isPrincipal_of_norm_le_of_isPrime {K : Type u_1} [Field K] [NumberField K] (h : ∀ ⦃I : ↥(nonZeroDivisors (Ideal (NumberField.RingOfIntegers K)))⦄, (↑I).IsPrime → ↑(Ideal.absNorm ↑I) ≤ (4 / Real.pi) ^ NumberField.InfinitePlace.nrComplexPlaces K * (↑(Module.finrank ℚ K).factorial / ↑(Module.finrank ℚ K) ^ Module.finrank ℚ K * √|↑(NumberField.discr K)|) → Submodule.IsPrincipal ↑I) : IsPrincipalIdealRing (NumberField.RingOfIntegers K)

theorem RingOfIntegers.isPrincipalIdealRing_of_isPrincipal_of_pow_le_of_mem_primesOver_of_mem_Icc {K : Type u_1} [Field K] [NumberField K] (h : ∀ 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 ^ (Ideal.span {↑p}).inertiaDeg P ≤ ⌊(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 [MS77], 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 RingOfIntegers.isPrincipalIdealRing_of_isPrincipal_of_lt_or_isPrincipal_of_mem_primesOver_of_mem_Icc {K : Type u_1} [Field K] [NumberField K] [IsGalois ℚ K] (h : ∀ 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), ⌊(4 / Real.pi) ^ NumberField.InfinitePlace.nrComplexPlaces K * (↑(Module.finrank ℚ K).factorial / ↑(Module.finrank ℚ K) ^ Module.finrank ℚ K * √|↑(NumberField.discr K)|)⌋₊ < p ^ (Ideal.span {↑p}).inertiaDeg P ∨ Submodule.IsPrincipal P) : IsPrincipalIdealRing (NumberField.RingOfIntegers K)

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 [MS77], 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 RingOfIntegers.isPrincipalIdealRing_of_abs_discr_lt {K : Type u_1} [Field K] [NumberField K] (h : ↑|NumberField.discr K| < (2 * (Real.pi / 4) ^ NumberField.InfinitePlace.nrComplexPlaces K * (↑(Module.finrank ℚ K) ^ Module.finrank ℚ K / ↑(Module.finrank ℚ K).factorial)) ^ 2) : IsPrincipalIdealRing (NumberField.RingOfIntegers K)

theorem Rat.classNumber_eq : NumberField.classNumber ℚ = 1