1.2. The class numbers h, h-plus, and h-minus
The class number of \mathbb{Q}(\zeta_p) is
h(\mathbb{Q}(\zeta_p)) \;:=\; \bigl|\mathrm{Cl}(\mathcal{O}_{\mathbb{Q}(\zeta_p)})\bigr|.
Lean code for Definition1.2.1●1 definition
Associated Lean declarations
-
BernoulliRegular.h[complete]
-
BernoulliRegular.h[complete]
-
defdefined in BernoulliRegular/TotallyRealSubfield/Basic.leancomplete
def BernoulliRegular.h.{u_1} (K : Type u_1) [Field K] [NumberField K] : ℕ
def BernoulliRegular.h.{u_1} (K : Type u_1) [Field K] [NumberField K] : ℕ
The class number of `K`, written locally as `h`.
The plus class number is the class number of the maximal real subfield:
\hplus \;:=\; \bigl|\mathrm{Cl}(\mathcal{O}_{\mathbb{Q}(\zeta_p)^+})\bigr|.
Lean code for Definition1.2.2●1 definition
Associated Lean declarations
-
BernoulliRegular.hPlus[complete]
-
BernoulliRegular.hPlus[complete]
-
defdefined in BernoulliRegular/TotallyRealSubfield/Basic.leancomplete
def BernoulliRegular.hPlus.{u_1} (K : Type u_1) [Field K] [NumberField K] [NumberField.IsCMField K] : ℕ
def BernoulliRegular.hPlus.{u_1} (K : Type u_1) [Field K] [NumberField K] [NumberField.IsCMField K] : ℕ
The class number of the totally real subfield `K⁺`, written locally as `h⁺`.
The crucial foundational fact is that \hplus divides h(\mathbb{Q}(\zeta_p)).
Only after this has been proved can one define the relative class number by honest
division. The proof, occupying the rest of this chapter, follows Diekmann's
Proposition 55 (Washington's Theorem 4.14). The strategy is to show that the
natural extension-of-ideals map
\mathrm{Cl}(\mathcal{O}_{\mathbb{Q}(\zeta_p)^+}) \longrightarrow \mathrm{Cl}(\mathcal{O}_{\mathbb{Q}(\zeta_p)})
is injective; divisibility of the orders then follows from the fact that an
injective homomorphism of finite groups has image of order dividing the codomain.