Integral representatives of ray classes

Every ray class of a modulus 𝔪 of a number field is the class of a nonzero integral ideal prime to 𝔪, and such an ideal has trivial class exactly when it is generated by an algebraic integer congruent to one modulo 𝔪, equivalently when it satisfies an integral equation I · (b) = (a) whose two generators are congruent to one modulo 𝔪. The construction behind both is that inside a nonzero ideal D comaximal with the finite part 𝔪₀ there is an algebraic integer congruent to one modulo 𝔪₀ and positive at every real place (exists_mem_isCongrOne). Its existence combines the comaximality, which supplies an element of D congruent to one, with NumberField.exists_isTotallyPositive_sub_mem, which corrects the archimedean signs without leaving the residue class modulo D · 𝔪₀.

Applying that construction to an integral ideal I prime to 𝔪 produces a principal ideal (α) = I · J generated by an element congruent to one, so J is again prime to 𝔪 and the ray class of J inverts the ray class of I. The image of idealClass 𝔪 is therefore a subgroup of the ray class group, and since it contains the class of every prime not dividing 𝔪 it is everything: this is the moving lemma, idealClass_surjective.

Main results

• TauCeti.GlobalNumberFields.exists_mem_isCongrOne: an ideal comaximal with the finite part of 𝔪 contains a nonzero element whose image in Kˣ is congruent to one modulo 𝔪.
• TauCeti.GlobalNumberFields.exists_isCongrOne_span_eq_mul: an integral ideal prime to 𝔪 divides a principal ideal whose generator is congruent to one modulo 𝔪, with complementary ideal again prime to 𝔪.
• TauCeti.GlobalNumberFields.exists_idealClass_mul_eq_one: the ray class of an integral ideal prime to 𝔪 is inverted by the ray class of another such ideal.
• TauCeti.GlobalNumberFields.idealClass_surjective: the moving lemma, that every ray class is the class of a nonzero integral ideal prime to the modulus.
• TauCeti.GlobalNumberFields.idealClass_eq_one_iff_exists_generator: the generator form of idealClass_eq_one_iff, with the generator kept inside 𝓞 K and its two defining conditions spelled out.
• TauCeti.GlobalNumberFields.idealClass_eq_one_iff_exists_integral: the denominator-cleared form of idealClass_eq_one_iff, an equation I · (b) = (a) between integral ideals whose generators are congruent to one modulo 𝔪.

References

• J. Neukirch, Algebraic Number Theory, Chapter VI, §1.
• S. Lang, Algebraic Number Theory, Chapter VI, §1.

Generators congruent to one modulo a modulus

theorem TauCeti.GlobalNumberFields.isCongrOne_of_sub_one_mem {K : Type u_1} [Field K] [NumberField K] {𝔪 : Modulus K} {x : Kˣ} {a : NumberField.RingOfIntegers K} (hxa : ↑x = ↑a) (hmem : a - 1 ∈ 𝔪.finitePart) (hpos : ∀ w ∈ 𝔪.infinitePart, 0 < (NumberField.InfinitePlace.embedding_of_isReal ⋯) ↑x) : IsCongrOne 𝔪 x

An algebraic integer in 1 + 𝔪₀ is congruent to one modulo 𝔪. Membership of a - 1 in the finite part gives the valuation bound at every finite place, since the prime power prescribed by the exponent divides the finite part (Modulus.pow_exponent_dvd_finitePart); the real conditions are carried over unchanged.

theorem TauCeti.GlobalNumberFields.sub_one_mem_of_isCongrOne {K : Type u_1} [Field K] [NumberField K] {𝔪 : Modulus K} {x : Kˣ} {a : NumberField.RingOfIntegers K} (hxa : ↑x = ↑a) (h : IsCongrOne 𝔪 x) : a - 1 ∈ 𝔪.finitePart

Congruence to one, read back on an algebraic integer. The converse of isCongrOne_of_sub_one_mem at the finite places: a unit congruent to one modulo 𝔪 that is the image of a : 𝓞 K has a - 1 in the finite part.

theorem TauCeti.GlobalNumberFields.exists_mem_isCongrOne {K : Type u_1} [Field K] [NumberField K] {𝔪 : Modulus K} {D : Ideal (NumberField.RingOfIntegers K)} (hD : D ≠ ⊥) (hcop : D ⊔ 𝔪.finitePart = ⊤) : ∃ (a : NumberField.RingOfIntegers K) (x : Kˣ), a ∈ D ∧ ↑x = ↑a ∧ IsCongrOne 𝔪 x

A generator congruent to one inside an ideal comaximal with the finite part. For a nonzero ideal D with D ⊔ 𝔪₀ = ⊤ there is an algebraic integer a ∈ D whose image in Kˣ is congruent to one modulo 𝔪.

Comaximality produces an element of D congruent to one modulo 𝔪₀, and NumberField.exists_isTotallyPositive_sub_mem moves it inside D * 𝔪₀ — hence without changing either condition — to make it nonzero and positive at every real place.

The moving lemma

theorem TauCeti.GlobalNumberFields.exists_isCongrOne_span_eq_mul {K : Type u_1} [Field K] [NumberField K] {𝔪 : Modulus K} (I : ↥(integralIdealsPrimeTo 𝔪)) : ∃ (J : ↥(integralIdealsPrimeTo 𝔪)) (a : NumberField.RingOfIntegers K) (x : Kˣ), ↑x = ↑a ∧ IsCongrOne 𝔪 x ∧ Ideal.span {a} = ↑I * ↑J

An integral ideal prime to 𝔪 divides a principal ideal with a generator congruent to one. Because the generator a is a unit at every prime dividing the finite part of 𝔪, the complementary ideal J with (a) = I · J is again prime to 𝔪.

This is the ideal-level statement behind exists_idealClass_mul_eq_one; it is the analogue, for a ray-class modulus, of NumberField.exists_isTotallyPositive_span_eq_mul_isCoprime.

theorem TauCeti.GlobalNumberFields.idealClass_mul_eq_one_of_span_eq_mul {K : Type u_1} [Field K] [NumberField K] {𝔪 : Modulus K} {I J : ↥(integralIdealsPrimeTo 𝔪)} {a : NumberField.RingOfIntegers K} {x : Kˣ} (hxa : ↑x = ↑a) (hx : IsCongrOne 𝔪 x) (hJ : Ideal.span {a} = ↑I * ↑J) : (idealClass 𝔪) I * (idealClass 𝔪) J = 1

A product of integral ideals generated by an element congruent to one lies in the ray.

theorem TauCeti.GlobalNumberFields.exists_idealClass_mul_eq_one {K : Type u_1} [Field K] [NumberField K] {𝔪 : Modulus K} (I : ↥(integralIdealsPrimeTo 𝔪)) : ∃ (J : ↥(integralIdealsPrimeTo 𝔪)), (idealClass 𝔪) I * (idealClass 𝔪) J = 1

Every ray class of an integral ideal prime to 𝔪 is inverted by another one. The principal ideal I · J of exists_isCongrOne_span_eq_mul has a generator congruent to one modulo 𝔪, so it lies in the ray. This is what makes the image of idealClass 𝔪 a subgroup.

theorem TauCeti.GlobalNumberFields.idealClass_surjective {K : Type u_1} [Field K] [NumberField K] (𝔪 : Modulus K) : Function.Surjective ⇑(idealClass 𝔪)

The moving lemma. Every ray class of 𝔪 is the class of a nonzero integral ideal prime to 𝔪: the image of idealClass 𝔪 is a subgroup of the ray class group by exists_idealClass_mul_eq_one, and it contains the class of every prime not dividing the finite part, which generate the ideals prime to 𝔪.

Triviality criteria with integral generators

theorem TauCeti.GlobalNumberFields.idealClass_eq_one_iff_exists_generator {K : Type u_1} [Field K] [NumberField K] {𝔪 : Modulus K} (J : ↥(integralIdealsPrimeTo 𝔪)) : (idealClass 𝔪) J = 1 ↔ ∃ (α : NumberField.RingOfIntegers K), α - 1 ∈ 𝔪.finitePart ∧ (∀ w ∈ 𝔪.infinitePart, 0 < (NumberField.InfinitePlace.embedding_of_isReal ⋯) ((algebraMap (NumberField.RingOfIntegers K) K) α)) ∧ ↑J = Ideal.span {α}

Trivial ray class, in generator form. An integral ideal prime to 𝔪 has trivial ray class exactly when it is generated by an algebraic integer that is congruent to one modulo the finite part and positive at every real place of the infinite part. This differs from idealClass_eq_one_iff in keeping the generator inside 𝓞 K, with the two conditions on it spelled out instead of packaged as IsCongrOne.

theorem TauCeti.GlobalNumberFields.idealClass_eq_one_iff_exists_integral {K : Type u_1} [Field K] [NumberField K] {𝔪 : Modulus K} (I : ↥(integralIdealsPrimeTo 𝔪)) : (idealClass 𝔪) I = 1 ↔ ∃ (x : Kˣ) (y : Kˣ) (a : NumberField.RingOfIntegers K) (b : NumberField.RingOfIntegers K), IsCongrOne 𝔪 x ∧ IsCongrOne 𝔪 y ∧ ↑x = ↑a ∧ ↑y = ↑b ∧ ↑I * Ideal.span {b} = Ideal.span {a}

The integral form of the triviality criterion. An integral ideal prime to 𝔪 has trivial ray class exactly when there are x y : Kˣ congruent to one modulo 𝔪 whose underlying values are algebraic integers a and b, with I · (b) = (a).

The fractional criterion idealClass_eq_one_iff is the primary one; this is the denominator-cleared form derived from it. A denominator congruent to one is available because the complementary ideal of exists_isCongrOne_span_eq_mul also has trivial class, hence an integral generator congruent to one.