1.6. Injectivity of the class-group map and the definition of h-minus
The descent theorem immediately gives injectivity on class groups.
-
BernoulliRegular.classGroupMap_injective[complete]
The extension map
\mathrm{Cl}(\mathcal{O}_{\mathbb{Q}(\zeta_p)^+}) \longrightarrow \mathrm{Cl}(\mathcal{O}_{\mathbb{Q}(\zeta_p)})
is injective.
Lean code for Theorem1.6.1●1 theorem
Associated Lean declarations
-
BernoulliRegular.classGroupMap_injective[complete]
-
BernoulliRegular.classGroupMap_injective[complete]
-
theoremdefined in BernoulliRegular/TotallyRealSubfield/ClassGroup.leancomplete
theorem BernoulliRegular.classGroupMap_injective.{u_1} (p : ℕ) [hp : Fact (Nat.Prime p)] (hp_odd : p ≠ 2) (K : Type u_1) [Field K] [NumberField K] [IsCyclotomicExtension {p} ℚ K] [NumberField.IsCMField K] : Function.Injective ⇑(BernoulliRegular.classGroupMap K)
theorem BernoulliRegular.classGroupMap_injective.{u_1} (p : ℕ) [hp : Fact (Nat.Prime p)] (hp_odd : p ≠ 2) (K : Type u_1) [Field K] [NumberField K] [IsCyclotomicExtension {p} ℚ K] [NumberField.IsCMField K] : Function.Injective ⇑(BernoulliRegular.classGroupMap K)
**Diekmann Prop 55**, monoid-hom form. The class-group map `Cl(𝒪_{K⁺}) → Cl(𝒪_K)` is injective for `K = ℚ(ζ_p)`.
A homomorphism of groups is injective iff its kernel is trivial. An element
[I] \in \mathrm{Cl}(\mathcal{O}^+) goes to the identity in
\mathrm{Cl}(\mathcal{O}) exactly when I \mathcal{O} is principal in
\mathcal{O}. Theorem 1.5.2.3 says that this forces
I itself to be principal, i.e. [I] = 1 in \mathrm{Cl}(\mathcal{O}^+). Thus
the kernel is trivial.
Since both class groups are finite, injectivity implies divisibility of their cardinalities.
-
BernoulliRegular.hPlus_dvd_h[complete]
\hplus divides h(\mathbb{Q}(\zeta_p)). The class number \hplus of
\mathbb{Q}(\zeta_p)^+ divides the class number h(\mathbb{Q}(\zeta_p)) of
\mathbb{Q}(\zeta_p).
Lean code for Theorem1.6.2●1 theorem
Associated Lean declarations
-
BernoulliRegular.hPlus_dvd_h[complete]
-
BernoulliRegular.hPlus_dvd_h[complete]
-
theoremdefined in BernoulliRegular/TotallyRealSubfield/ClassGroup.leancomplete
theorem BernoulliRegular.hPlus_dvd_h.{u_1} (p : ℕ) [hp : Fact (Nat.Prime p)] (hp_odd : p ≠ 2) (K : Type u_1) [Field K] [NumberField K] [IsCyclotomicExtension {p} ℚ K] [NumberField.IsCMField K] : BernoulliRegular.hPlus K ∣ BernoulliRegular.h K
theorem BernoulliRegular.hPlus_dvd_h.{u_1} (p : ℕ) [hp : Fact (Nat.Prime p)] (hp_odd : p ≠ 2) (K : Type u_1) [Field K] [NumberField K] [IsCyclotomicExtension {p} ℚ K] [NumberField.IsCMField K] : BernoulliRegular.hPlus K ∣ BernoulliRegular.h K
The class number of `K⁺` divides the class number of `K`.
By Theorem 1.6.1 the extension map
\mathrm{Cl}(\mathcal{O}^+) \to \mathrm{Cl}(\mathcal{O}) is an injective
homomorphism of finite groups. Its image is a subgroup of \mathrm{Cl}(\mathcal{O})
of order \hplus, and by Lagrange's theorem the order of any subgroup of a finite
group divides the order of the ambient group.
This justifies the definition of the relative class number.
The relative class number is defined by
\hminus \;:=\; h(\mathbb{Q}(\zeta_p)) / \hplus.
Lean code for Definition1.6.3●1 definition
Associated Lean declarations
-
BernoulliRegular.hMinus[complete]
-
BernoulliRegular.hMinus[complete]
-
defdefined in BernoulliRegular/TotallyRealSubfield/ClassGroup.leancomplete
def BernoulliRegular.hMinus.{u_1} (K : Type u_1) [Field K] [NumberField K] [NumberField.IsCMField K] : ℕ
def BernoulliRegular.hMinus.{u_1} (K : Type u_1) [Field K] [NumberField K] [NumberField.IsCMField K] : ℕ
The *relative class number* `h⁻ := h / h⁺`, written locally as `h⁻`.
We shall also use the factorisation and positivity statements below.
-
BernoulliRegular.h_eq_hPlus_mul_hMinus[complete]
One has h(\mathbb{Q}(\zeta_p)) = \hplus\,\hminus.
Lean code for Theorem1.6.4●1 theorem
Associated Lean declarations
-
BernoulliRegular.h_eq_hPlus_mul_hMinus[complete]
-
BernoulliRegular.h_eq_hPlus_mul_hMinus[complete]
-
theoremdefined in BernoulliRegular/TotallyRealSubfield/ClassGroup.leancomplete
theorem BernoulliRegular.h_eq_hPlus_mul_hMinus.{u_1} (p : ℕ) [hp : Fact (Nat.Prime p)] (hp_odd : p ≠ 2) (K : Type u_1) [Field K] [NumberField K] [IsCyclotomicExtension {p} ℚ K] [NumberField.IsCMField K] : BernoulliRegular.h K = BernoulliRegular.hPlus K * BernoulliRegular.hMinus K
theorem BernoulliRegular.h_eq_hPlus_mul_hMinus.{u_1} (p : ℕ) [hp : Fact (Nat.Prime p)] (hp_odd : p ≠ 2) (K : Type u_1) [Field K] [NumberField K] [IsCyclotomicExtension {p} ℚ K] [NumberField.IsCMField K] : BernoulliRegular.h K = BernoulliRegular.hPlus K * BernoulliRegular.hMinus K
Immediate from Definition 1.6.3 and
Theorem 1.6.2: dividing h(\mathbb{Q}(\zeta_p)) by the divisor
\hplus yields \hminus, and multiplying back recovers h(\mathbb{Q}(\zeta_p)).
The relative class number \hminus is strictly positive.
Lean code for Theorem1.6.5●1 theorem
Associated Lean declarations
-
BernoulliRegular.hMinus_pos[complete]
-
BernoulliRegular.hMinus_pos[complete]
-
theoremdefined in BernoulliRegular/TotallyRealSubfield/ClassGroup.leancomplete
theorem BernoulliRegular.hMinus_pos.{u_1} (p : ℕ) [hp : Fact (Nat.Prime p)] (hp_odd : p ≠ 2) (K : Type u_1) [Field K] [NumberField K] [IsCyclotomicExtension {p} ℚ K] [NumberField.IsCMField K] : 0 < BernoulliRegular.hMinus K
theorem BernoulliRegular.hMinus_pos.{u_1} (p : ℕ) [hp : Fact (Nat.Prime p)] (hp_odd : p ≠ 2) (K : Type u_1) [Field K] [NumberField K] [IsCyclotomicExtension {p} ℚ K] [NumberField.IsCMField K] : 0 < BernoulliRegular.hMinus K
The relative class number is positive.
Both h(\mathbb{Q}(\zeta_p)) and \hplus are positive integers (cardinalities of
nonempty finite groups), and \hplus \mid h(\mathbb{Q}(\zeta_p)), so the quotient
h(\mathbb{Q}(\zeta_p)) / \hplus is a positive integer.