Ray-class reciprocity

Let L/K be a finite abelian extension of number fields and 𝔪 a modulus of K admissible for L/K. The ray class group Cl_𝔪 is the quotient of the idele class group C_K by the ray subgroup of 𝔪 (GlobalNumberFields.rayClassQuotient, with kernel GlobalNumberFields.ker_rayClassQuotient), and admissibility says that the ray subgroup lies in the norm group N_{L/K}(C_L), the kernel of the global Artin map. So the global Artin map factors through Cl_𝔪: this is the ray-class Artin map

rayClassArtinMap 𝔪 h : Cl_𝔪 →* Gal(L/K),

read in Gal(L/K) itself, which is its own abelianization: composed with the ray class map it is the global Artin map ideleClassArtinMap K L (rayClassArtinMap_comp_rayClassQuotient), or, in Gal(L/K)^ab, globalArtinMap (of_rayClassArtinMap_rayClassQuotient). The admissibility proof h is an argument of the definition: for an inadmissible modulus the global Artin map need not factor, as for ℚ(i)/ℚ and the trivial modulus (not_isAdmissibleModulus_one_Qi).

The map is surjective (rayClassArtinMap_surjective), because the global Artin map is, and its kernel is the image of the norm group in Cl_𝔪 (ker_rayClassArtinMap).

On ideals it is the ideal-theoretic Artin map. The prime idele class at a finite place v outside the support of 𝔪 is congruent to one modulo 𝔪, and its ray class is the ray class of the prime v (rayClassQuotient_primeIdeleClass, an instance of GlobalNumberFields.rayClassQuotient_ofAdicCompletion_of_isUniformizer). An admissible modulus contains every ramified prime in its support (IsAdmissibleModulus.isUnramifiedAway), and the global Artin symbol of the prime idele class at an unramified place is the Frobenius there (globalArtinMap_ideal). Since the ideal-theoretic Artin map is determined by its values on primes, the ray-class Artin map, composed with the ray class of an ideal prime to 𝔪, is NumberFieldArithmetic.artinHomAway for the excluded set 𝔪.support (rayClassArtinMap_comp_rayClassMk). This is the splitting law: the ray-class Artin symbol of a prime ideal 𝔭 prime to 𝔪 is an arithmetic Frobenius at every prime of L above 𝔭 (isArithFrobAt_rayClassArtinMap_idealClass), and its conjugacy class is the Artin symbol of 𝔭 (rayClassArtinMap_idealClass). Since 𝔭 is unramified in L (IsAdmissibleModulus.isUnramifiedAt_of_integralIdealsPrimeTo), the order of this Frobenius is the residue degree f of 𝔭 in L (orderOf_rayClassArtinMap_idealClass), so 𝔭 has [L : K] / f primes above it (ncard_primesOver_mul_orderOf_rayClassArtinMap_idealClass). In particular 𝔭 splits completely in L exactly when its ray-class Artin symbol is trivial (ncard_primesOver_eq_finrank_iff_rayClassArtinMap_idealClass_eq_one).

Main definitions

• TauCeti.ClassFieldTheory.rayClassArtinMap: the ray-class Artin map Cl_𝔪 →* Gal(L/K) of an admissible modulus.

Main results

• TauCeti.ClassFieldTheory.rayClassArtinMap_comp_rayClassQuotient, TauCeti.ClassFieldTheory.rayClassArtinMap_rayClassQuotient, TauCeti.ClassFieldTheory.of_rayClassArtinMap_rayClassQuotient: the ray-class Artin map is the factorization of the global Artin map through the ray class group.
• TauCeti.ClassFieldTheory.rayClassArtinMap_surjective: the ray-class Artin map is surjective.
• TauCeti.ClassFieldTheory.ker_rayClassArtinMap: its kernel is the image of the norm group.
• TauCeti.ClassFieldTheory.rayClassQuotient_primeIdeleClass: the ray class of the prime idele class at a place outside the support of 𝔪 is the ray class of the prime.
• TauCeti.ClassFieldTheory.rayClassArtinMap_comp_rayClassMk, TauCeti.ClassFieldTheory.rayClassArtinMap_rayClassMk: on the ideals prime to 𝔪 the ray-class Artin map is the ideal-theoretic Artin map.
• TauCeti.ClassFieldTheory.isArithFrobAt_rayClassArtinMap_idealClass, TauCeti.ClassFieldTheory.rayClassArtinMap_idealClass: the splitting law.
• TauCeti.ClassFieldTheory.orderOf_rayClassArtinMap_idealClass, TauCeti.ClassFieldTheory.ncard_primesOver_mul_orderOf_rayClassArtinMap_idealClass: the decomposition law of a prime ideal prime to 𝔪.
• TauCeti.ClassFieldTheory.ncard_primesOver_eq_finrank_iff_rayClassArtinMap_idealClass_eq_one: a prime ideal prime to 𝔪 splits completely exactly when its ray-class Artin symbol is trivial.

References

• J. Neukirch, Algebraic Number Theory, Chapter VI, §7 (the Artin reciprocity law for ray class groups, Theorem 7.1).
• J. S. Milne, Class Field Theory, v4.03, Chapter V, §3 and Chapter VII, §5.

The ray class of a prime idele class

theorem TauCeti.ClassFieldTheory.rayClassQuotient_primeIdeleClass {K : Type} [Field K] [NumberField K] {𝔪 : GlobalNumberFields.Modulus K} {v : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)} (I : ↥(GlobalNumberFields.idealsPrimeTo 𝔪)) (hI : ↑↑I = ↑v.asIdeal) : (GlobalNumberFields.rayClassQuotient 𝔪) (primeIdeleClass K v) = (GlobalNumberFields.rayClassMk 𝔪) I

The ray class of a prime idele class is the ray class of the prime. For a finite place v of K outside the support of a modulus 𝔪, the prime idele class at v has the ray class of the prime v, as does the class of any uniformizer at v (GlobalNumberFields.rayClassQuotient_ofAdicCompletion_of_isUniformizer).

The ray-class Artin map

noncomputable def TauCeti.ClassFieldTheory.rayClassArtinMap {K L : Type} [Field K] [NumberField K] [Field L] [NumberField L] [Algebra K L] [IsAbelianGalois K L] (𝔪 : GlobalNumberFields.Modulus K) (h : IsAdmissibleModulus K L 𝔪) : GlobalNumberFields.RayClassGroup 𝔪 →* Gal(L/K)

The ray-class Artin map Cl_𝔪 →* Gal(L/K) of a finite abelian extension L/K of number fields and a modulus 𝔪 admissible for L/K: the factorization of the global Artin map through the ray class group of 𝔪, which exists because admissibility puts the ray subgroup inside the norm group, the kernel of the global Artin map. It is characterized by rayClassArtinMap_rayClassQuotient, and on ideals it is the ideal-theoretic Artin map (rayClassArtinMap_comp_rayClassMk).

theorem TauCeti.ClassFieldTheory.rayClassArtinMap_comp_rayClassQuotient {K L : Type} [Field K] [NumberField K] [Field L] [NumberField L] [Algebra K L] [IsAbelianGalois K L] {𝔪 : GlobalNumberFields.Modulus K} (h : IsAdmissibleModulus K L 𝔪) : (rayClassArtinMap 𝔪 h).comp (GlobalNumberFields.rayClassQuotient 𝔪) = ideleClassArtinMap K L

The ray-class Artin map factors the global Artin map: composed with the ray class map C_K → Cl_𝔪, it is the global Artin map ideleClassArtinMap K L of L/K.

@[simp]

theorem TauCeti.ClassFieldTheory.rayClassArtinMap_rayClassQuotient {K L : Type} [Field K] [NumberField K] [Field L] [NumberField L] [Algebra K L] [IsAbelianGalois K L] {𝔪 : GlobalNumberFields.Modulus K} (h : IsAdmissibleModulus K L 𝔪) (c : NumberField.IdeleClassGroup (NumberField.RingOfIntegers K) K) : (rayClassArtinMap 𝔪 h) ((GlobalNumberFields.rayClassQuotient 𝔪) c) = (ideleClassArtinMap K L) c

The ray-class Artin map factors the global Artin map, pointwise: the ray-class Artin symbol of the ray class of c ∈ C_K is the global Artin symbol of c.

theorem TauCeti.ClassFieldTheory.of_rayClassArtinMap_rayClassQuotient {K L : Type} [Field K] [NumberField K] [Field L] [NumberField L] [Algebra K L] [IsAbelianGalois K L] {𝔪 : GlobalNumberFields.Modulus K} (h : IsAdmissibleModulus K L 𝔪) (ι : L →ₐ[K] SeparableClosure K) (c : NumberField.IdeleClassGroup (NumberField.RingOfIntegers K) K) : Abelianization.of ((rayClassArtinMap 𝔪 h) ((GlobalNumberFields.rayClassQuotient 𝔪) c)) = Additive.toMul ((globalArtinMap K L ι) (Additive.ofMul c))

The ray-class Artin map factors the global Artin map: the class in Gal(L/K)^ab of the ray-class Artin symbol of the ray class of c ∈ C_K is the global Artin symbol of c, for every embedding ι of L into the separable closure.

theorem TauCeti.ClassFieldTheory.rayClassArtinMap_surjective {K L : Type} [Field K] [NumberField K] [Field L] [NumberField L] [Algebra K L] [IsAbelianGalois K L] {𝔪 : GlobalNumberFields.Modulus K} (h : IsAdmissibleModulus K L 𝔪) : Function.Surjective ⇑(rayClassArtinMap 𝔪 h)

Ray-class reciprocity is surjective: every automorphism of L/K is the ray-class Artin symbol of a ray class of 𝔪.

theorem TauCeti.ClassFieldTheory.ker_rayClassArtinMap {K L : Type} [Field K] [NumberField K] [Field L] [NumberField L] [Algebra K L] [IsAbelianGalois K L] {𝔪 : GlobalNumberFields.Modulus K} (h : IsAdmissibleModulus K L 𝔪) : (rayClassArtinMap 𝔪 h).ker = Subgroup.map (GlobalNumberFields.rayClassQuotient 𝔪) (↑(GlobalNumberFields.ideleClassNormMap K L)).range

The kernel of ray-class reciprocity is the image in the ray class group of 𝔪 of the idele-class norm group N_{L/K}(C_L).

The splitting law

theorem TauCeti.ClassFieldTheory.rayClassArtinMap_comp_rayClassMk {K L : Type} [Field K] [NumberField K] [Field L] [NumberField L] [Algebra K L] [IsAbelianGalois K L] {𝔪 : GlobalNumberFields.Modulus K} (h : IsAdmissibleModulus K L 𝔪) : (rayClassArtinMap 𝔪 h).comp (GlobalNumberFields.rayClassMk 𝔪) = NumberFieldArithmetic.artinHomAway ⋯ 𝔪.support ⋯

On ideals, ray-class reciprocity is the ideal-theoretic Artin map: the ray-class Artin symbol of the ray class of an invertible fractional ideal prime to 𝔪 is the value of NumberFieldArithmetic.artinHomAway at that ideal, for the excluded set 𝔪.support, outside which L/K is unramified (IsAdmissibleModulus.isUnramifiedAway).

@[simp]

theorem TauCeti.ClassFieldTheory.rayClassArtinMap_rayClassMk {K L : Type} [Field K] [NumberField K] [Field L] [NumberField L] [Algebra K L] [IsAbelianGalois K L] {𝔪 : GlobalNumberFields.Modulus K} (h : IsAdmissibleModulus K L 𝔪) (I : ↥(GlobalNumberFields.idealsPrimeTo 𝔪)) : (rayClassArtinMap 𝔪 h) ((GlobalNumberFields.rayClassMk 𝔪) I) = (NumberFieldArithmetic.artinHomAway ⋯ 𝔪.support ⋯) I

On ideals, ray-class reciprocity is the ideal-theoretic Artin map, pointwise.

theorem TauCeti.ClassFieldTheory.isArithFrobAt_rayClassArtinMap_idealClass {K L : Type} [Field K] [NumberField K] [Field L] [NumberField L] [Algebra K L] [IsAbelianGalois K L] {𝔪 : GlobalNumberFields.Modulus K} (h : IsAdmissibleModulus K L 𝔪) (I : ↥(GlobalNumberFields.integralIdealsPrimeTo 𝔪)) [(↑I).IsMaximal] (Q : Ideal (NumberField.RingOfIntegers L)) [Q.IsPrime] [Q.LiesOver ↑I] : IsArithFrobAt (NumberField.RingOfIntegers K) ((rayClassArtinMap 𝔪 h) ((GlobalNumberFields.idealClass 𝔪) I)) Q

The splitting law: the ray-class Artin symbol of the ray class of a prime ideal 𝔭 of K prime to 𝔪 is an arithmetic Frobenius at every prime of L above 𝔭.

theorem TauCeti.ClassFieldTheory.rayClassArtinMap_idealClass {K L : Type} [Field K] [NumberField K] [Field L] [NumberField L] [Algebra K L] [IsAbelianGalois K L] {𝔪 : GlobalNumberFields.Modulus K} (h : IsAdmissibleModulus K L 𝔪) (I : ↥(GlobalNumberFields.integralIdealsPrimeTo 𝔪)) [(↑I).IsMaximal] (hur : ∀ (Q : Ideal (NumberField.RingOfIntegers L)) [inst : Q.IsPrime] [Q.LiesOver ↑I], Algebra.IsUnramifiedAt (NumberField.RingOfIntegers K) Q) : ConjClasses.mk ((rayClassArtinMap 𝔪 h) ((GlobalNumberFields.idealClass 𝔪) I)) = NumberField.artinSymbol (↑I) hur

The splitting law, through the Artin symbol: the conjugacy class of the ray-class Artin symbol of the ray class of a prime ideal 𝔭 of K prime to 𝔪 is the Artin symbol of 𝔭.

The decomposition law

theorem TauCeti.ClassFieldTheory.orderOf_rayClassArtinMap_idealClass {K L : Type} [Field K] [NumberField K] [Field L] [NumberField L] [Algebra K L] [IsAbelianGalois K L] {𝔪 : GlobalNumberFields.Modulus K} (h : IsAdmissibleModulus K L 𝔪) (I : ↥(GlobalNumberFields.integralIdealsPrimeTo 𝔪)) [(↑I).IsMaximal] (Q : Ideal (NumberField.RingOfIntegers L)) [Q.IsPrime] [Q.LiesOver ↑I] : orderOf ((rayClassArtinMap 𝔪 h) ((GlobalNumberFields.idealClass 𝔪) I)) = Q.inertiaDeg (NumberField.RingOfIntegers K)

The order of the ray-class Artin symbol is the residue degree: for a prime ideal 𝔭 of K prime to 𝔪 and a prime Q of L above it, the ray-class Artin symbol of the ray class of 𝔭 has order the inertia degree f(Q / 𝔭).

theorem TauCeti.ClassFieldTheory.ncard_primesOver_mul_orderOf_rayClassArtinMap_idealClass {K L : Type} [Field K] [NumberField K] [Field L] [NumberField L] [Algebra K L] [IsAbelianGalois K L] {𝔪 : GlobalNumberFields.Modulus K} (h : IsAdmissibleModulus K L 𝔪) (I : ↥(GlobalNumberFields.integralIdealsPrimeTo 𝔪)) [(↑I).IsMaximal] : ((↑I).primesOver (NumberField.RingOfIntegers L)).ncard * orderOf ((rayClassArtinMap 𝔪 h) ((GlobalNumberFields.idealClass 𝔪) I)) = Module.finrank K L

The decomposition law for an admissible modulus: a prime ideal 𝔭 of K prime to 𝔪 has [L : K] / f primes above it in L, where f is the order of the ray-class Artin symbol of its ray class.

theorem TauCeti.ClassFieldTheory.ncard_primesOver_eq_finrank_iff_rayClassArtinMap_idealClass_eq_one {K L : Type} [Field K] [NumberField K] [Field L] [NumberField L] [Algebra K L] [IsAbelianGalois K L] {𝔪 : GlobalNumberFields.Modulus K} (h : IsAdmissibleModulus K L 𝔪) (I : ↥(GlobalNumberFields.integralIdealsPrimeTo 𝔪)) [(↑I).IsMaximal] : ((↑I).primesOver (NumberField.RingOfIntegers L)).ncard = Module.finrank K L ↔ (rayClassArtinMap 𝔪 h) ((GlobalNumberFields.idealClass 𝔪) I) = 1

The splitting criterion for an admissible modulus: a prime ideal 𝔭 of K prime to 𝔪 splits completely in L, that is, has [L : K] primes above it, exactly when the ray-class Artin symbol of its ray class is trivial.