The ray class group of ℚ modulo (n)·∞

For a positive integer n, the modulus (n)·∞ of ℚ has finite part the ideal generated by n and infinite part the unique real place. Its ray class group is (ZMod n)ˣ: a fractional ideal of ℚ prime to n has exactly one positive generator, and the class of the ideal is the residue of that generator modulo n. In particular the ray class of a nonzero integral ideal prime to n is its absolute norm modulo n.

The real place is essential. For the modulus (n) without it, both a and -a generate the same ideal, so the ray class group is only (ZMod n)ˣ ⧸ {±1}. For n > 2 this has half the order of (ZMod n)ˣ, so the two moduli give genuinely different ray class groups.

The equivalence is read off from the ray class exact sequence. The class group of ℚ is trivial, so every ray class is the class of a residue unit modulo n and a sign at the real place. The only integer units are ±1, so the sign of a class can be absorbed into its residue and a class with positive sign is determined by its residue.

Main definitions

• TauCeti.GlobalNumberFields.ratModulus: the modulus (n)·∞ of ℚ.
• TauCeti.GlobalNumberFields.ratModulusResidueEquiv: the residue ring of 𝓞 ℚ modulo the finite part of ratModulus n hn is ZMod n.
• TauCeti.GlobalNumberFields.ratModulusEquivZMod: the ray class group of ratModulus n hn is (ZMod n)ˣ.
• TauCeti.GlobalNumberFields.ratFiniteModulus: the modulus (n) of ℚ without the real place.
• TauCeti.GlobalNumberFields.ratFiniteModulusEquivZMod: the ray class group of ratFiniteModulus n hn is (ZMod n)ˣ ⧸ {±1}.

Main results

• TauCeti.GlobalNumberFields.asIdeal_mem_integralIdealsPrimeTo_ratModulus_iff: a height-one prime is prime to (n)·∞ exactly when it does not contain n.
• TauCeti.GlobalNumberFields.ratModulusEquivZMod_symm_apply: a unit u modulo n corresponds to the principal ray class of a positive rational number with residue u.
• TauCeti.GlobalNumberFields.coe_ratModulusEquivZMod_idealClass: the ray class of a nonzero integral ideal prime to n is its absolute norm modulo n.
• TauCeti.GlobalNumberFields.ratModulusEquivZMod_classMap: the transition map from (n)·∞ to (d)·∞ is reduction modulo d.
• TauCeti.GlobalNumberFields.ratModulusEquivZMod_residueSignRayClass_neg_one: the class of the sign -1 at the real place is -1 ∈ (ZMod n)ˣ.
• TauCeti.GlobalNumberFields.ratModulus_dvd_ratModulus_iff and TauCeti.GlobalNumberFields.ratFiniteModulus_dvd_ratModulus_iff: divisibility of the moduli (d)·∞ and (d) into (n)·∞ is d ∣ n.
• TauCeti.GlobalNumberFields.dvd_ratModulus_iff: a modulus of ℚ divides (n)·∞ exactly when the absolute norm of its finite part divides n.
• TauCeti.GlobalNumberFields.dvd_ratModulus_absNorm: every modulus of ℚ divides (N)·∞, where N is the absolute norm of its finite part.
• TauCeti.GlobalNumberFields.ratFiniteModulusEquivZMod_classMap: the transition map from (n)·∞ to (d) is reduction modulo d followed by the quotient by ±1.
• TauCeti.GlobalNumberFields.ratFiniteModulusEquivZMod_idealClass: the ray class modulo (n) of a nonzero integral ideal prime to n is its absolute norm modulo n, up to sign.
• TauCeti.GlobalNumberFields.two_mul_card_rayClassGroup_ratFiniteModulus: for n > 2, the ray class group modulo (n) has order φ(n) / 2.

References

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

noncomputable def TauCeti.GlobalNumberFields.ratModulus (n : ℕ) (hn : n ≠ 0) : Modulus ℚ

The modulus (n)·∞ of ℚ: its finite part is the ideal of 𝓞 ℚ generated by n, and its infinite part is the real place of ℚ.

@[simp]

theorem TauCeti.GlobalNumberFields.ratModulus_finitePart (n : ℕ) (hn : n ≠ 0) : (ratModulus n hn).finitePart = Ideal.span {↑n}

@[simp]

theorem TauCeti.GlobalNumberFields.ratModulus_infinitePart (n : ℕ) (hn : n ≠ 0) : (ratModulus n hn).infinitePart = {⟨Rat.infinitePlace, Rat.isReal_infinitePlace⟩}

theorem TauCeti.GlobalNumberFields.mem_ratModulus_support_iff {n : ℕ} {hn : n ≠ 0} {v : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers ℚ)} : v ∈ (ratModulus n hn).support ↔ ↑n ∈ v.asIdeal

A prime lies in the support of ratModulus n hn exactly when it contains n.

theorem TauCeti.GlobalNumberFields.asIdeal_mem_integralIdealsPrimeTo_ratModulus_iff {n : ℕ} {hn : n ≠ 0} {v : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers ℚ)} : v.asIdeal ∈ integralIdealsPrimeTo (ratModulus n hn) ↔ ↑n ∉ v.asIdeal

A height-one prime is prime to ratModulus n hn exactly when it does not contain n.

noncomputable def TauCeti.GlobalNumberFields.ratModulusResidueEquiv (n : ℕ) (hn : n ≠ 0) : NumberField.RingOfIntegers ℚ ⧸ (ratModulus n hn).finitePart ≃+* ZMod n

Reduction modulo the finite part of ratModulus n hn is reduction modulo n, transported along Rat.ringOfIntegersEquiv : 𝓞 ℚ ≃+* ℤ.

@[simp]

theorem TauCeti.GlobalNumberFields.ratModulusResidueEquiv_mk (n : ℕ) (hn : n ≠ 0) (a : NumberField.RingOfIntegers ℚ) : (ratModulusResidueEquiv n hn) ((Ideal.Quotient.mk (ratModulus n hn).finitePart) a) = ↑(Rat.ringOfIntegersEquiv a)

noncomputable def TauCeti.GlobalNumberFields.ratModulusEquivZMod (n : ℕ) (hn : n ≠ 0) : RayClassGroup (ratModulus n hn) ≃* (ZMod n)ˣ

The ray class group of ℚ modulo (n)·∞ is (ZMod n)ˣ. A ray class corresponds to the residue modulo n of the positive generator of any fractional ideal in it.

theorem TauCeti.GlobalNumberFields.ratModulusEquivZMod_symm_apply (n : ℕ) (hn : n ≠ 0) (u : (ZMod n)ˣ) : (ratModulusEquivZMod n hn).symm u = (residueSignRayClass (ratModulus n hn)) ((Units.mapEquiv (ratModulusResidueEquiv n hn).symm.toMulEquiv) u, 1)

A unit u modulo n corresponds to the principal ray class of an element with residue u and positive sign at the real place.

@[simp]

theorem TauCeti.GlobalNumberFields.coe_ratModulusEquivZMod_idealClass (n : ℕ) (hn : n ≠ 0) (I : ↥(integralIdealsPrimeTo (ratModulus n hn))) : ↑((ratModulusEquivZMod n hn) ((idealClass (ratModulus n hn)) I)) = ↑(Ideal.absNorm ↑I)

The ray class of a nonzero integral ideal prime to n is its absolute norm modulo n. Since idealClass is surjective, this characterizes ratModulusEquivZMod.

Divisibility of the moduli (n)·∞ and compatibility of the identification

theorem TauCeti.GlobalNumberFields.ratModulus_dvd_ratModulus_iff {n : ℕ} {hn : n ≠ 0} {d : ℕ} {hd : d ≠ 0} : ratModulus d hd ∣ ratModulus n hn ↔ d ∣ n

The moduli (d)·∞ and (n)·∞ of ℚ divide each other as d and n do.

theorem TauCeti.GlobalNumberFields.dvd_ratModulus_iff {n : ℕ} {hn : n ≠ 0} {𝔪 : Modulus ℚ} : 𝔪 ∣ ratModulus n hn ↔ Ideal.absNorm 𝔪.finitePart ∣ n

A modulus of ℚ divides (n)·∞ exactly when the absolute norm of its finite part divides n: the finite part is generated by its absolute norm, and the real place is the only infinite place of ℚ.

theorem TauCeti.GlobalNumberFields.dvd_ratModulus_absNorm (𝔪 : Modulus ℚ) : 𝔪 ∣ ratModulus (Ideal.absNorm 𝔪.finitePart) ⋯

Every modulus of ℚ divides (N)·∞, where N is the absolute norm of its finite part.

theorem TauCeti.GlobalNumberFields.ratModulusEquivZMod_classMap {n : ℕ} {hn : n ≠ 0} {d : ℕ} {hd : d ≠ 0} (h : ratModulus d hd ∣ ratModulus n hn) (c : RayClassGroup (ratModulus n hn)) : (ratModulusEquivZMod d hd) ((classMap h) c) = (ZMod.unitsMap ⋯) ((ratModulusEquivZMod n hn) c)

The transition map from (n)·∞ to (d)·∞ is reduction modulo d on (ZMod n)ˣ.

theorem TauCeti.GlobalNumberFields.ratModulusEquivZMod_residueSignRayClass_neg_one {n : ℕ} {hn : n ≠ 0} : (ratModulusEquivZMod n hn) ((residueSignRayClass (ratModulus n hn)) (1, fun (x : ↥(ratModulus n hn).infinitePart) => -1)) = -1

The class of the sign -1 at the real place corresponds to -1 ∈ (ZMod n)ˣ. The ray class of a negative rational with residue 1 modulo n is the ray class of a positive rational with residue -1: the two differ by the unit -1.

The modulus (n) without the real place

noncomputable def TauCeti.GlobalNumberFields.ratFiniteModulus (n : ℕ) (hn : n ≠ 0) : Modulus ℚ

The modulus (n) of ℚ without the real place. A ray class character of (n)·∞ is induced from it exactly when the corresponding Dirichlet character is even.

@[simp]

theorem TauCeti.GlobalNumberFields.ratFiniteModulus_finitePart (n : ℕ) (hn : n ≠ 0) : (ratFiniteModulus n hn).finitePart = Ideal.span {↑n}

@[simp]

theorem TauCeti.GlobalNumberFields.ratFiniteModulus_infinitePart (n : ℕ) (hn : n ≠ 0) : (ratFiniteModulus n hn).infinitePart = ∅

theorem TauCeti.GlobalNumberFields.ratFiniteModulus_dvd_ratModulus_iff {n : ℕ} {hn : n ≠ 0} {d : ℕ} {hd : d ≠ 0} : ratFiniteModulus d hd ∣ ratModulus n hn ↔ d ∣ n

The modulus (d) divides (n)·∞ exactly when d ∣ n.

theorem TauCeti.GlobalNumberFields.ratFiniteModulus_dvd_ratModulus {n : ℕ} {hn : n ≠ 0} : ratFiniteModulus n hn ∣ ratModulus n hn

The modulus (n) divides (n)·∞.

The ray class group of ℚ modulo (n)

noncomputable def TauCeti.GlobalNumberFields.ratFiniteModulusEquivZMod (n : ℕ) (hn : n ≠ 0) : RayClassGroup (ratFiniteModulus n hn) ≃* (ZMod n)ˣ ⧸ Subgroup.zpowers (-1)

The ray class group of ℚ modulo (n) is (ZMod n)ˣ ⧸ {±1}. Without the real place, a fractional ideal of ℚ prime to n has the two generators ±a on an equal footing, so its ray class is the residue of a generator modulo n, up to sign.

theorem TauCeti.GlobalNumberFields.ratFiniteModulusEquivZMod_classMap {n : ℕ} {hn : n ≠ 0} {d : ℕ} {hd : d ≠ 0} (h : ratFiniteModulus d hd ∣ ratModulus n hn) (c : RayClassGroup (ratModulus n hn)) : (ratFiniteModulusEquivZMod d hd) ((classMap h) c) = ↑((ZMod.unitsMap ⋯) ((ratModulusEquivZMod n hn) c))

Forgetting the real place is reduction modulo ±1. For d ∣ n, the transition map from (n)·∞ to (d) sends the class of u ∈ (ZMod n)ˣ to the class of its reduction modulo d, up to sign.

theorem TauCeti.GlobalNumberFields.ratFiniteModulusEquivZMod_idealClass {n : ℕ} {hn : n ≠ 0} (I : ↥(integralIdealsPrimeTo (ratFiniteModulus n hn))) {u : (ZMod n)ˣ} (hu : ↑u = ↑(Ideal.absNorm ↑I)) : (ratFiniteModulusEquivZMod n hn) ((idealClass (ratFiniteModulus n hn)) I) = ↑u

The ray class modulo (n) of a nonzero integral ideal prime to n is its absolute norm modulo n, up to sign.

theorem TauCeti.GlobalNumberFields.two_mul_card_rayClassGroup_ratFiniteModulus {n : ℕ} {hn : n ≠ 0} (h2 : 2 < n) : 2 * Nat.card (RayClassGroup (ratFiniteModulus n hn)) = n.totient

The ray class group of ℚ modulo (n) has half the order of the one modulo (n)·∞ once n > 2, so that -1 ≠ 1 modulo n: its order is φ(n) / 2, while RayClassGroup (ratModulus n hn) has order φ(n). The real place therefore genuinely enlarges the ray class group.