Local–global compatibility of the global Artin map

Let L/K be a finite Galois extension of number fields. The global Artin map globalArtinMap K L ι : C_K → Gal(L/K)^ab is the abstract Artin map of the global class formation, whose invariant is the sum of the local invariants. Its local factors are the local Artin symbols localArtinAt K L v : K_vˣ → Gal(L/K)^ab at the finite places and infiniteLocalArtinAt K L w : K_wˣ → Gal(L/K)^ab at the infinite places, the local Artin maps read in Gal(L/K)^ab through the decomposition group of a place of L above.

The global Artin symbol of the class of an idele a is determined by these local factors: every character χ : Gal(L/K)^ab → ℚ/ℤ satisfies

χ (Art [a]) = ∑ᶠ v, χ (Art_v a_v) + ∑_w χ (Art_w a_w)

(apply_globalArtinMap_eq_finsum). It is the character formula of the global class formation on idele classes, ClassFormation.apply_artinMap_eq_finsum_of_inv_eq_ideleSumLocalInv, for the idele a regarded as an invariant idele of Kˢ, whose coordinates are its components (exists_ideleCoeffComponent_ideleExtension_eq, exists_ideleCoeffInfiniteComponent_ideleExtension_eq), and with the local symbols read in Gal(L/K)^ab by decompositionRestrict_mk_eq_restrictNormalHom_absoluteGaloisGroupMap.

Since characters separate the points of Gal(L/K)^ab, the restriction of the global Artin map to the units of one completion, embedded in C_K as ideles concentrated at one place, is the local Artin symbol there: globalArtinMap_local at a finite place, globalArtinMap_infiniteLocal at an infinite place. No hypothesis of abelianity or unramifiedness is needed.

Main results

• TauCeti.ClassFieldTheory.apply_globalArtinMap_eq_finsum: the value of a character on the global Artin symbol of an idele class is the sum of its values on the local Artin symbols of the components.
• TauCeti.ClassFieldTheory.globalArtinMap_eq_zero_of_forall_eq_one: an idele whose local Artin symbols are all trivial has trivial global Artin symbol.
• TauCeti.ClassFieldTheory.globalArtinMap_local: on K_vˣ at a finite place v, the global Artin map is the local Artin symbol localArtinAt K L v.
• TauCeti.ClassFieldTheory.globalArtinMap_infiniteLocal: on K_wˣ at an infinite place w, the global Artin map is the local Artin symbol infiniteLocalArtinAt K L w.

References

• J. Neukirch, Algebraic Number Theory, Chapter VI, §5 (the global reciprocity law and its local factors).
• J. S. Milne, Class Field Theory, v4.03, Chapter VIII.
• J. Tate, Global class field theory, in J. W. S. Cassels and A. Fröhlich (eds.), Algebraic Number Theory, Chapter VII, §11.

theorem TauCeti.ClassFieldTheory.apply_globalArtinMap_eq_finsum (K : Type) [Field K] [NumberField K] (L : Type) [Field L] [NumberField L] [Algebra K L] [IsGalois K L] (ι : L →ₐ[K] SeparableClosure K) (χ : Additive (Abelianization Gal(L/K)) →+ AddCircle 1) (a : NumberField.IdeleGroup (NumberField.RingOfIntegers K) K) : χ ((globalArtinMap K L ι) (Additive.ofMul ↑a)) = ∑ᶠ (v : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)), χ (Additive.ofMul ((localArtinAt K L v) (v.ideleFiniteCoord a))) + ∑ w : NumberField.InfinitePlace K, χ (Additive.ofMul ((infiniteLocalArtinAt K L w) (w.ideleInfiniteCoord a)))

The local–global character formula for the global Artin map. For a finite Galois extension L/K of number fields, embedded in Kˢ by ι, every character χ : Gal(L/K)^ab → ℚ/ℤ takes on the global Artin symbol of the class of an idele a the sum of its values on the local Artin symbols of the components of a, at the finite places and at the infinite places:

χ (Art [a]) = ∑ᶠ v, χ (Art_v a_v) + ∑_w χ (Art_w a_w).

theorem TauCeti.ClassFieldTheory.globalArtinMap_eq_zero_of_forall_eq_one (K : Type) [Field K] [NumberField K] (L : Type) [Field L] [NumberField L] [Algebra K L] [IsGalois K L] (ι : L →ₐ[K] SeparableClosure K) {a : NumberField.IdeleGroup (NumberField.RingOfIntegers K) K} (hfin : ∀ (v : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)), (localArtinAt K L v) (v.ideleFiniteCoord a) = 1) (hinf : ∀ (w : NumberField.InfinitePlace K), (infiniteLocalArtinAt K L w) (w.ideleInfiniteCoord a) = 1) : (globalArtinMap K L ι) (Additive.ofMul ↑a) = 0

Trivial local Artin symbols give a trivial global Artin symbol. For a finite Galois extension L/K of number fields, embedded in Kˢ by ι, if every local Artin symbol of the components of an idele a, at the finite and at the infinite places, is trivial, then so is the global Artin symbol of the class of a.

@[simp]

theorem TauCeti.ClassFieldTheory.globalArtinMap_local (K : Type) [Field K] [NumberField K] (L : Type) [Field L] [NumberField L] [Algebra K L] [IsGalois K L] (ι : L →ₐ[K] SeparableClosure K) (v : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)) (x : (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v)ˣ) : (globalArtinMap K L ι) (Additive.ofMul ↑((NumberField.IdeleGroup.ofAdicCompletion (NumberField.RingOfIntegers K) K v) x)) = Additive.ofMul ((localArtinAt K L v) x)

Local–global compatibility at a finite place. For a finite Galois extension L/K of number fields and a finite place v of K, the global Artin symbol of the class of the idele concentrated at v with component x ∈ K_vˣ is the local Artin symbol of x at v, read in Gal(L/K)^ab through the decomposition group of a place of L above v.

@[simp]

theorem TauCeti.ClassFieldTheory.globalArtinMap_infiniteLocal (K : Type) [Field K] [NumberField K] (L : Type) [Field L] [NumberField L] [Algebra K L] [IsGalois K L] (ι : L →ₐ[K] SeparableClosure K) (w : NumberField.InfinitePlace K) (x : w.Completionˣ) : (globalArtinMap K L ι) (Additive.ofMul ↑((NumberField.IdeleGroup.ofCompletion (NumberField.RingOfIntegers K) K w) x)) = Additive.ofMul ((infiniteLocalArtinAt K L w) x)

Local–global compatibility at an infinite place. For a finite Galois extension L/K of number fields and an infinite place w of K, the global Artin symbol of the class of the idele concentrated at w with component x ∈ K_wˣ is the archimedean local Artin symbol of x at w, read in Gal(L/K)^ab through the decomposition group of a place of L above w.