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

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_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