Coprime representatives of narrow ideal classes #
Every narrow ideal class of a number field has an integral representative coprime to any prescribed nonzero ideal. This is the finite-place approximation input needed to evaluate genus characters on narrow ideal classes in Layer 3 of the multiquadratic roadmap.
The proof starts with the Dedekind-domain approximation
IsDedekindDomain.exists_sup_span_eq, applied to I * M ≤ I. It gives an element a ∈ I such
that I * M + (a) = I; consequently the quotient (a) / I is coprime to M. Moving a inside
I * M by NumberField.exists_isTotallyPositive_sub_mem makes it nonzero and totally positive
without changing this ideal identity. Thus (a) / I represents the inverse narrow class of I.
This is the usual finite-prime form of strong approximation for ideal classes. See J. W. S. Cassels and A. Fröhlich, Algebraic Number Theory, Chapter II.
Main results #
NumberField.exists_isTotallyPositive_span_eq_mul_isCoprime: a totally positive principal multiple of a nonzero ideal whose quotient is coprime to a prescribed ideal.NumberField.NarrowClassGroup.exists_mk0_eq_and_isCoprime: every narrow ideal class has a nonzero integral representative coprime to a prescribed nonzero ideal.NumberField.NarrowClassGroup.exists_mk0_eq_and_isCoprime_absNorm: the representative may be chosen with absolute norm coprime to a prescribed nonzero integer.
A totally positive coprime quotient of an ideal. Given nonzero integral ideals I and M,
there are a nonzero totally positive algebraic integer a and a nonzero ideal J, coprime to M,
such that (a) = I * J.
Equivalently, J = (a) / I. The element a may be chosen totally positive while retaining the
finite-place coprimality because NumberField.exists_isTotallyPositive_sub_mem moves it inside
I * M, which does not change the ideal it generates together with I * M.
Every narrow ideal class has a coprime integral representative. For every class C and
nonzero integral ideal M, there is a nonzero integral ideal J, coprime to M, whose narrow
class is C.
This is the strong-approximation input used to define ideal-class characters from arithmetic functions that are only multiplicative away from a fixed modulus.
Every narrow ideal class has a representative of norm coprime to a modulus. For a nonzero
integer m, every narrow ideal class is represented by a nonzero integral ideal J whose absolute
norm is coprime to m.
This is the integer-modulus form consumed by genus characters, whose value on J is evaluated at
Ideal.absNorm J.