The narrow class group of a totally complex field

For a totally complex number field K (no real infinite places) the positivity condition is vacuous: every unit is totally positive (totallyPositiveUnits_eq_top), so the forgetful surjection Cl⁺(K) → Cl(K) is also injective. Hence the narrow and ordinary class groups coincide — as the multiquadratic roadmap notes, for imaginary fields narrow = ordinary. (The t - 1 genus-theory rank formula concerns the real case, where the two can differ.)

Main results

• NumberField.NarrowClassGroup.toClassGroup_injective: for a totally complex field the forgetful map Cl⁺(K) → Cl(K) is injective.
• NumberField.NarrowClassGroup.toClassGroupEquiv: the isomorphism Cl⁺(K) ≃* Cl(K).

theorem NumberField.NarrowClassGroup.toClassGroup_injective {K : Type u_1} [Field K] [NumberField K] [IsTotallyComplex K] : Function.Injective ⇑toClassGroup

For a totally complex field the forgetful map Cl⁺(K) → Cl(K) is injective: by exactness its kernel is mkPrincipal.range, and every principal class is already trivial because principal ideals have a (vacuously totally positive) generator.

noncomputable def NumberField.NarrowClassGroup.toClassGroupEquiv {K : Type u_1} [Field K] [NumberField K] [IsTotallyComplex K] : NarrowClassGroup K ≃* ClassGroup (RingOfIntegers K)

For a totally complex number field the narrow and ordinary class groups coincide: Cl⁺(K) ≃* Cl(K), forgetting positivity.

Equations

• NumberField.NarrowClassGroup.toClassGroupEquiv = MulEquiv.ofBijective NumberField.NarrowClassGroup.toClassGroup ⋯

@[simp]

theorem NumberField.NarrowClassGroup.toClassGroupEquiv_apply {K : Type u_1} [Field K] [NumberField K] [IsTotallyComplex K] (z : NarrowClassGroup K) : toClassGroupEquiv z = toClassGroup z