The narrow class group of a number field is finite

The narrow class group Cl⁺(K) is finite. It surjects onto the finite ordinary class group Cl(K) (NarrowClassGroup.toClassGroup), and by exactness (toClassGroup_ker) the kernel of that surjection is the image of the principal-class map mkPrincipal, which factors through Kˣ ⧸ totallyPositiveUnits — finite because totallyPositiveUnits has finite index (finiteIndex_totallyPositiveUnits).

Main results

• NumberField.NarrowClassGroup.instFinite: Cl⁺(K) is finite.
• NumberField.NarrowClassGroup.exists_card_eq_card_classGroup_mul_two_pow: the narrow class number is the ordinary class number times a power of 2.

instance NumberField.NarrowClassGroup.instFinite {K : Type u_1} [Field K] [NumberField K] : Finite (NarrowClassGroup K)

The narrow class group is finite.

theorem NumberField.NarrowClassGroup.isPGroup_two_ker_toClassGroup {K : Type u_1} [Field K] [NumberField K] : IsPGroup 2 ↥toClassGroup.ker

The kernel of the forgetful map Cl⁺(K) → Cl(K) is a 2-group: it is 2-torsion (sq_eq_one_of_mem_ker_toClassGroup).

theorem NumberField.NarrowClassGroup.card_eq_card_classGroup_mul_card_ker {K : Type u_1} [Field K] [NumberField K] : Nat.card (NarrowClassGroup K) = Nat.card (ClassGroup (RingOfIntegers K)) * Nat.card ↥toClassGroup.ker

The narrow class number is the ordinary class number times the order of the kernel of the forgetful map Cl⁺(K) → Cl(K).

theorem NumberField.NarrowClassGroup.exists_card_eq_card_classGroup_mul_two_pow {K : Type u_1} [Field K] [NumberField K] : ∃ (k : ℕ), Nat.card (NarrowClassGroup K) = Nat.card (ClassGroup (RingOfIntegers K)) * 2 ^ k

The narrow class number is the ordinary class number times a power of 2. The extra factor is the order of the elementary abelian 2-group ker(Cl⁺(K) → Cl(K)).