The narrow class group of a number field #
The narrow class group Cl⁺(K) of a number field K is the group of invertible fractional
ideals of 𝓞 K modulo the principal ones admitting a totally positive generator. It refines the
ordinary class group Cl(K), which quotients by all principal ideals: forgetting the positivity
condition on generators gives a surjection Cl⁺(K) → Cl(K).
This construction adapts Mathlib's ClassGroup (Mathlib.RingTheory.ClassGroup.Basic): where
ClassGroup R is (FractionalIdeal R⁰ (FractionRing R))ˣ ⧸ (toPrincipalIdeal R _).range, the
narrow class group quotients the invertible fractional ideals over K by the smaller subgroup
narrowPrincipalSubgroup of principal ideals with a totally positive generator.
The narrow class group is the object whose 2-rank the genus-theory t - 1 formula computes for a
real quadratic field (Layer 3 of the multiquadratic roadmap); for imaginary fields, where every unit
is totally positive (there are no real places), Cl⁺(K) and Cl(K) coincide.
Main definitions and results #
NumberField.narrowPrincipalSubgroup: the subgroup of principal fractional ideals with a totally positive generator, withmem_narrowPrincipalSubgroup.NumberField.NarrowClassGroup: the quotientCl⁺(K), aCommGroup.NumberField.NarrowClassGroup.mk: the class of an invertible fractional ideal, withmk_surjective,mk_eq_one_iff,mk_eq_mk_iff, and the eliminatorinduction.NumberField.NarrowClassGroup.lift: the universal property — a homomorphism trivial onnarrowPrincipalSubgroupdescends toCl⁺(K), withlift_mkandlift_unique.NumberField.NarrowClassGroup.toClassGroup: the surjectionCl⁺(K) → Cl(K)forgetting positivity, withtoClassGroup_surjective.NumberField.NarrowClassGroup.mkPrincipalandtoClassGroup_ker: the principal-class mapKˣ → Cl⁺(K)and exactness atCl⁺(K)ofKˣ → Cl⁺(K) → Cl(K) → 1(ker toClassGroup = mkPrincipal.range), with the triviality criterionmkPrincipal_eq_one_iff.NumberField.NarrowClassGroup.mkPrincipal_sqandsq_eq_one_of_mem_ker_toClassGroup:mkPrincipalis2-torsion, soker(Cl⁺ → Cl)is an elementary abelian2-group.NumberField.NarrowClassGroup.mkPrincipal_eq_one_of_isTotallyPositiveandNumberField.NarrowClassGroup.mkPrincipal_neg: the principal class is trivial on totally positive generators and blind to the sign of its generator.NumberField.NarrowClassGroup.mk0: the narrow class of a nonzero integral ideal, withtoClassGroup_mk0,mk0_surjective, the triviality criterionmk0_eq_one_iff, the2-torsion of principal classesmk0_sq_eq_one_of_eq_span_singleton,mkPrincipal_coe_eq_mk0, and the comparisonmk0_eq_mk0_iff.
The subgroup of (FractionalIdeal (𝓞 K)⁰ K)ˣ of principal fractional ideals with a totally
positive generator: the image of totallyPositiveUnits under toPrincipalIdeal. The narrow class
group quotients by this subgroup.
Equations
Instances For
A fractional ideal lies in narrowPrincipalSubgroup exactly when it is toPrincipalIdeal of a
totally positive unit.
The narrow class group Cl⁺(K): invertible fractional ideals of 𝓞 K modulo the principal
ones with a totally positive generator.
Equations
Instances For
Equations
- One or more equations did not get rendered due to their size.
Equations
- NumberField.instInhabitedNarrowClassGroup K = { default := 1 }
The class of an invertible fractional ideal in the narrow class group.
Equations
Instances For
Induction on the narrow class group: to prove a property of every class it suffices to prove it
for the class mk I of every invertible fractional ideal.
Every narrow ideal class is represented by an invertible fractional ideal.
A fractional ideal has trivial narrow class exactly when it has a totally positive generator.
Two fractional ideals have the same narrow class exactly when they differ by a principal ideal with a totally positive generator.
Universal property of the narrow class group. A homomorphism φ out of the invertible
fractional ideals whose kernel contains narrowPrincipalSubgroup (i.e. φ is trivial on principal
ideals with a totally positive generator) descends to a homomorphism Cl⁺(K) → M.
Equations
Instances For
The descended homomorphism lift φ h agrees with φ on the class of each representative.
The lift is the unique homomorphism Cl⁺(K) → M factoring φ through mk.
The surjection Cl⁺(K) → Cl(K) onto the ordinary class group, forgetting the positivity
condition on generators.
Equations
Instances For
Forgetting positivity sends the narrow class of I to its ordinary ideal class.
The forgetful homomorphism Cl⁺(K) → Cl(K) onto the ordinary class group is surjective.
The narrow ideal class of the principal fractional ideal (x) generated by a unit x : Kˣ.
Equations
Instances For
The narrow principal class of x is trivial exactly when a unit of 𝓞 K scales x to a
totally positive element. Two elements of Kˣ generate the same fractional ideal precisely when
they differ by a unit of 𝓞 K, so the narrow class of (x) is trivial iff one of the generators
w · x of that ideal is totally positive.
The composition Cl⁺(K) → Cl(K) after mkPrincipal is trivial: forgetting positivity kills the
class of a principal ideal. This is the "composition is one" half of exactness at Cl⁺(K).
Exactness at Cl⁺(K) of Kˣ → Cl⁺(K) → Cl(K) → 1: the kernel of the forgetful map to the
ordinary class group is exactly the image of the principal-class map. Together with
toClassGroup_surjective this expresses exactness of the whole sequence.
The principal-class map is 2-torsion: mkPrincipal x ^ 2 = 1, since x ^ 2 is totally
positive and so (x ^ 2) is a principal ideal with a totally positive generator.
A totally positive generator makes the principal class trivial.
The principal class is insensitive to the sign of its generator, because -1 is a unit of
𝓞 K, so (x) and (-x) are the same fractional ideal. This is what makes the image of
mkPrincipal a quotient of the group of sign patterns modulo the global sign.
The kernel of the forgetful map Cl⁺(K) → Cl(K) is killed by 2: by exactness it is the image
of mkPrincipal, which is 2-torsion. So the narrow-vs-ordinary defect is an elementary abelian
2-group.
Classes of integral ideals #
The narrow class of a nonzero integral ideal of 𝓞 K, the narrow counterpart of
ClassGroup.mk0.
Equations
Instances For
Forgetting positivity sends the narrow class of an integral ideal to its ordinary class.
An integral ideal has trivial narrow class exactly when it has a nonzero totally positive generator.
A principal ideal with a totally positive generator has trivial narrow class.
The narrow class of a principal ideal is 2-torsion, since the square of any generator is
totally positive.
The narrow class of the principal ideal generated by a nonzero algebraic integer is the principal narrow class of that integer.
Every narrow ideal class is the class of an integral ideal. An ordinary integral representative differs from the given class by a principal class, and a principal class is the class of an integral ideal because it is its own inverse.
When two integral ideals have the same narrow class. They do exactly when they differ by a
principal ideal with a totally positive generator, written as a ratio x / y of algebraic integers;
the ratio is totally positive precisely when the product x * y is.