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

• NumberField.classNumber: the class number of a number field is the (finite) cardinality of the class group of its ring of integers
• RingOfIntegers.isPrincipalIdealRing_of_isPrincipal_of_mem_primesOver_of_le: to show that the ring of integer of a number field is a PID it is enough to show that all ideals above any (natural) prime p smaller than Minkowski bound are principal. This is the standard technique to prove that 𝓞 K is principal, see [MS77], discussion after Theorem 37.

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_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_mem_primesOver_of_le {K : Type u_1} [Field K] [NumberField K] (h : ∀ ⦃p : ℕ⦄, Nat.Prime p → ↑p ≤ (4 / Real.pi) ^ NumberField.InfinitePlace.nrComplexPlaces K * (↑(Module.finrank ℚ K).factorial / ↑(Module.finrank ℚ K) ^ Module.finrank ℚ K * √|↑(NumberField.discr K)|) → ∀ I ∈ (Ideal.span {↑p}).primesOver (NumberField.RingOfIntegers K), Submodule.IsPrincipal I) : IsPrincipalIdealRing (NumberField.RingOfIntegers K)

To show that the ring of integer of a number field is a PID it is enough to show that all ideals above any (natural) prime p smaller than Minkowski bound are principal.

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