The product formula for the cyclotomic characters of local Artin symbols

Let K be a number field, p a prime and x ∈ Kˣ. At every place v of K the local Artin symbol Art_v(x) of the image of x in the completion K_v acts on the roots of unity of p-power order through the p-adic cyclotomic character χ_p = TauCeti.abelianizedLocalCyclotomicCharacter p K_v. This file proves the product formula

∏_v χ_p(Art_v(x)) = 1,

the product running over the finite and the infinite places (finprod_mul_prod_abelianizedLocalCyclotomicCharacter_artinMap_eq_one). Reading each Art_v(x) through its action on the roots of unity of p-power order, which is what χ_p records, this is the reciprocity law ∏_v Art_v(x) = 1 for the cyclotomic extensions K(μ_{pⁿ})/K, and so, as p varies, for every K(μ_m)/K. That reciprocity law is the input from which the sum of the local invariants of a Brauer class of K split by a cyclic cyclotomic extension is shown to vanish.

The local factors are explicit over ℚ. At a prime ℓ ≠ p the Artin symbol of a ∈ ℚˣ has cyclotomic character ℓ ^ v_ℓ(a) (abelianizedLocalCyclotomicCharacter_artinMap, the residue field of ℚ_ℓ having ℓ elements), at p it is u⁻¹ for a = pᵏ u with u ∈ ℤ_pˣ (abelianizedLocalCyclotomicCharacter_artinMap_padic), and at the real place it is the sign of a (abelianizedLocalCyclotomicCharacter_infiniteArtinAt_eq_neg_one_of_neg). The finite places of ℚ are read in ℚ_ℓ through Padic.adicCompletionEquiv and the naturality of the cyclotomic character of Artin symbols (abelianizedLocalCyclotomicCharacter_artinMap_congr). Modulo pⁿ the local factors are exactly the explicit cyclotomic symbols cyclotomicSymbol (pⁿ) ℓ and realCyclotomicSymbol (pⁿ) of ℚ(μ_{pⁿ})/ℚ, so the product formula over ℚ is, level by level, the product formula for the explicit symbols (prod_cyclotomicSymbol_of_subset). The norm functoriality of the local Artin symbols (finprod_abelianizedLocalCyclotomicCharacter_artinMap_normUnits and prod_abelianizedLocalCyclotomicCharacter_infiniteArtinAt_normUnits) then carries the formula for N_{K/ℚ}(x) over ℚ to the formula for x over K.

Main results

• TauCeti.ClassFieldTheory.finprod_mul_prod_abelianizedLocalCyclotomicCharacter_artinMap_eq_one: the product over all places of K of the p-adic cyclotomic characters of the local Artin symbols of x ∈ Kˣ is 1.

References

• J. S. Milne, Class Field Theory, Chapter VII, Example 8.2 and Lemma 8.4.

Over ℚ

theorem TauCeti.ClassFieldTheory.instFactPrimeValNat_tauCeti (ℓ : Nat.Primes) : Fact (Nat.Prime ↑ℓ)

theorem TauCeti.ClassFieldTheory.finprod_mul_prod_abelianizedLocalCyclotomicCharacter_artinMap_eq_one (p : ℕ) [Fact (Nat.Prime p)] {K : Type} [Field K] [NumberField K] (x : Kˣ) : (∏ᶠ (v : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)), (abelianizedLocalCyclotomicCharacter p (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v)) ((artinMap (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v)) ((Units.map ↑(algebraMap K (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v))) x))) * ∏ w : NumberField.InfinitePlace K, (abelianizedLocalCyclotomicCharacter p w.Completion) ((infiniteArtinAt w) ((Units.map ↑(algebraMap K w.Completion)) x)) = 1

The product formula for the cyclotomic characters of local Artin symbols. For x ∈ Kˣ, the product over all places v of the number field K, finite and infinite, of the p-adic cyclotomic characters of the local Artin symbols Art_v(x) is 1:

∏_v χ_p(Art_v(x)) = 1.

The factors at the finite places are 1 for all but finitely many v (hasFiniteMulSupport_abelianizedLocalCyclotomicCharacter_artinMap).