The ray class group of ℚ modulo (n)·∞ and the Galois group of ℚ(ζ_n) #
Let F be the n-th cyclotomic field over ℚ. Both RayClassGroup (ratModulus n _) and
Gal(F/ℚ) are identified with (ZMod n)ˣ: the first by ratModulusEquivZMod, which sends the
class of an ideal prime to n to its absolute norm modulo n, and the second by Mathlib's
IsCyclotomicExtension.Rat.galEquivZMod, which records the exponent by which an automorphism
acts on the n-th roots of unity. Composing them gives
ratModulusEquivGal n F : RayClassGroup (ratModulus n _) ≃* Gal(F/ℚ).
This file shows that the identification is the arithmetic one. An arithmetic Frobenius at a prime
of 𝓞 F above p ∤ n acts on ζ_n by ζ_n ↦ ζ_n ^ p, and the ray class of (p) is p mod n,
so ratModulusEquivGal sends the class of (p) to the Frobenius at p. Since the ideals prime
to n are generated by such primes, the ideal-theoretic Artin map of F/ℚ away from n factors
through the ray class group of (n)·∞, and the induced map is ratModulusEquivGal. The
identification is also compatible with lowering the level: for d ∣ n, the transition map
classMap corresponds to restricting automorphisms to the d-th cyclotomic field.
The orientation is the arithmetic one: the class of (p) goes to the automorphism raising roots of
unity to the p-th power, not to its inverse.
Main definitions #
TauCeti.GlobalNumberFields.ratModulusEquivGal: the identification of the ray class group ofℚmodulo(n)·∞withGal(ℚ(ζ_n)/ℚ).
Main results #
TauCeti.GlobalNumberFields.isArithFrobAt_iff_eq_ratModulusEquivGal_idealClass: an automorphism ofℚ(ζ_n)is an arithmetic Frobenius at a prime abovep ∤ nexactly when it is the image of the ray class of(p).TauCeti.GlobalNumberFields.ratModulusEquivGal_comp_rayClassMk: the Artin map ofℚ(ζ_n)/ℚon the fractional ideals prime tonis the ray class map followed byratModulusEquivGal.TauCeti.GlobalNumberFields.restrictNormal_ratModulusEquivGal: ford ∣ n, restriction toℚ(ζ_d)corresponds to the transition map from(n)·∞to(d)·∞.
References #
- J. Neukirch, Algebraic Number Theory, Chapter I, §10 and Chapter VI, §1.
The ray class group of ℚ modulo (n)·∞ is the Galois group of ℚ(ζ_n). The
composite of ratModulusEquivZMod with the inverse of Mathlib's galEquivZMod: a ray class with
residue a ∈ (ZMod n)ˣ goes to the automorphism acting on the n-th roots of unity by
ζ ↦ ζ ^ a. It sends the ray class of a prime p ∤ n to the arithmetic Frobenius at p
(isArithFrobAt_iff_eq_ratModulusEquivGal_idealClass).
Instances For
The image of a ray class is the automorphism whose galEquivZMod exponent is the residue of
the class.
galEquivZMod undoes ratModulusEquivGal down to ratModulusEquivZMod. This is not a
simp lemma: galEquivZMod is a reducible abbreviation, which simp unfolds first.
The inverse of ratModulusEquivGal reads an automorphism through galEquivZMod.
Frobenius elements #
The ray class of a prime is its Frobenius. For a height-one prime v = (p) of 𝓞 ℚ with
p ∤ n and a prime Q of 𝓞 F above it, an automorphism of F = ℚ(ζ_n) is an arithmetic
Frobenius at Q exactly when it is the image under ratModulusEquivGal of the ray class of
(p).
The image under ratModulusEquivGal of the ray class of a prime p ∤ n is an arithmetic
Frobenius at every prime of 𝓞 F above p.
Lowering the level #
Restriction to ℚ(ζ_d) is the transition map from (n)·∞ to (d)·∞. For d ∣ n and
F' the d-th cyclotomic field inside F, restricting the image of a ray class to F' gives
the image of its class modulo (d)·∞.
The Artin map #
Every prime of 𝓞 F above a prime of 𝓞 ℚ outside the support of (n)·∞, that is, not
dividing n, is unramified in F = ℚ(ζ_n). This is the unramifiedness hypothesis of the Artin
map of F/ℚ away from n.
The Artin map of ℚ(ζ_n)/ℚ factors through the ray class group of (n)·∞, and the
induced map is ratModulusEquivGal. On the fractional ideals of ℚ prime to n, the
ideal-theoretic Artin map artinHomAway is the ray class map rayClassMk followed by
ratModulusEquivGal. Thus the Artin map is trivial on the ray of (n)·∞ and induces an
isomorphism of the ray class group with Gal(F/ℚ). The commutativity and unramifiedness inputs
of the Artin map are supplied by IsCyclotomicExtension.isMulCommutative and
isUnramifiedAt_of_notMem_ratModulus_support.
The Artin automorphism of an integral ideal prime to n is the image of its ray class.
This is ratModulusEquivGal_comp_rayClassMk read on the integral ideals prime to n.