The archimedean Artin maps

Let w be an infinite place of a field K, with completion K_w, which is ℝ or ℂ. The units formation of K_w carries the class formation infiniteClassFormation w, whose invariant is the archimedean Brauer invariant infiniteInvMap w after inflation. Its absolute Artin map, read through the identification of the ground level with K_wˣ and the comparison of the separable and algebraic closures, is the archimedean Artin map

infiniteArtinAt w : K_wˣ →* G_{K_w}^ab,

into the topological abelianization of Mathlib's absolute Galois group, the target of the nonarchimedean artinMap. It is built from the formation machinery and the archimedean Brauer computation alone, with no reciprocity law.

On every layer V ◁ G_{K_w} it is the abstract Artin map of infiniteClassFormation w (infiniteArtinAt_layer), so the character formula of a class formation gives the archimedean character formula χ(Art_w x) = inv_w(x ∪ δχ) (character_infiniteArtinAt). This is the form in which an archimedean Artin symbol enters a sum of local invariants.

The map is explicit. At a complex place G_{K_w} is trivial, so Art_w is trivial (infiniteArtinAt_eq_one_of_isComplex). At a real place G_{K_w} has order two, so Art_w kills the squares, which are the positive elements, while the Artin map of the quadratic layer is surjective onto a group of order two; hence the kernel of Art_w is exactly ℝ_{>0}, the norm group of ℂ/ℝ (infiniteArtinAt_eq_one_iff_of_isReal). On roots of unity a lift of Art_w(x) therefore acts trivially for x > 0 and by ζ ↦ ζ⁻¹ for x < 0, that is, through the explicit real cyclotomic symbol realCyclotomicSymbol (infiniteArtinAt_rootsOfUnity_of_isReal): the nontrivial automorphism of K_w(i)/K_w sends a + b i to a - b i, so ζ σ(ζ) = a² + b² is a nonnegative root of unity in K_w ≅ ℝ. In particular the p-adic cyclotomic character of the Artin symbol of a negative element is -1 (abelianizedLocalCyclotomicCharacter_infiniteArtinAt_eq_neg_one_of_neg). Finally, the archimedean Artin maps are functorial for the norm of a finite extension (infiniteArtinAt_norm), the archimedean analogue of artinMap_norm.

Main definitions

• TauCeti.ClassFieldTheory.infiniteArtinAt: the archimedean Artin map K_wˣ →* G_{K_w}^ab.

Main results

• TauCeti.ClassFieldTheory.infiniteArtinAt_apply: the archimedean Artin map is the absolute Artin map of infiniteClassFormation w.
• TauCeti.ClassFieldTheory.infiniteArtinAt_layer: on every layer V ◁ G_{K_w}, the archimedean Artin map is the Artin map of infiniteClassFormation w.
• TauCeti.ClassFieldTheory.character_infiniteArtinAt: the archimedean character formula.
• TauCeti.ClassFieldTheory.infiniteArtinAt_eq_one_of_isComplex: at a complex place the Artin map is trivial.
• TauCeti.ClassFieldTheory.infiniteArtinAt_eq_one_iff_of_isReal: at a real place the kernel of the Artin map is the group of positive elements.
• TauCeti.ClassFieldTheory.infiniteArtinAt_rootsOfUnity_of_isReal: at a real place the Artin symbol acts on the m-th roots of unity through realCyclotomicSymbol m.
• TauCeti.ClassFieldTheory.abelianizedLocalCyclotomicCharacter_infiniteArtinAt_eq_neg_one_of_neg: at a real place the cyclotomic character of the Artin symbol of a negative element is -1.
• TauCeti.ClassFieldTheory.infiniteArtinAt_norm: norm functoriality of the archimedean Artin maps.

References

• E. Artin and J. Tate, Class Field Theory, Chapter XIV, §§1–4.
• J. S. Milne, Class Field Theory, Chapter VII, §8 (the local Artin symbol at an archimedean place), and Chapter VIII, §4.

noncomputable def TauCeti.ClassFieldTheory.infiniteArtinAt {K : Type} [Field K] (w : NumberField.InfinitePlace K) : w.Completionˣ →* Field.absoluteGaloisGroupAbelianization w.Completion

The archimedean Artin map Art_w : K_wˣ →* G_{K_w}^ab at an infinite place w: the map ClassFormation.fieldArtinMap of infiniteClassFormation w, that is, its absolute Artin map read on K_wˣ and in the topological abelianization of Mathlib's absolute Galois group of K_w, as for the nonarchimedean artinMap. On every layer it is the Artin map of that class formation (infiniteArtinAt_layer); it is trivial at a complex place (infiniteArtinAt_eq_one_of_isComplex) and has kernel the positive elements at a real place (infiniteArtinAt_eq_one_iff_of_isReal).

theorem TauCeti.ClassFieldTheory.infiniteArtinAt_apply {K : Type} [Field K] (w : NumberField.InfinitePlace K) (x : w.Completionˣ) : (infiniteArtinAt w) x = (absoluteGaloisGroupRestrictEquiv w.Completion).symm.topologicalAbelianizationCongr (Additive.toMul ((infiniteClassFormation w).absoluteArtinMap ((unitsLevelEquiv (Algebra.ofId w.Completion (SeparableClosure w.Completion)) ⋯) (Additive.ofMul x))))

The archimedean Artin map is the absolute Artin map of infiniteClassFormation w: the absolute Artin symbol of x ∈ K_wˣ, regarded as an element of the ground level ((K_wˢ)ˣ)^{G_{K_w}}, carried from Gal(K_wˢ/K_w)^ab to Gal(AlgebraicClosure K_w/K_w)^ab.

theorem TauCeti.ClassFieldTheory.infiniteArtinAt_layer {K : Type} [Field K] (w : NumberField.InfinitePlace K) (V : OpenNormalSubgroup (AbsoluteGaloisGroup w.Completion)) (x : w.Completionˣ) (σ : Field.absoluteGaloisGroup w.Completion) (hσ : ↑σ = (infiniteArtinAt w) x) : ((infiniteClassFormation w).artinMap (NormalLayer.ofOpenNormal V)) ((localGroundEquiv w.Completion V) (Additive.ofMul x)) = Additive.ofMul (Abelianization.of ((NormalLayer.galOfOpenNormalEquiv V).symm ↑((absoluteGaloisGroupRestrictEquiv w.Completion) σ)))

The archimedean Artin map on a layer. If σ ∈ Gal(AlgebraicClosure K_w/K_w) represents Art_w(x), then for every open normal subgroup V of G_{K_w} the Artin map of infiniteClassFormation w on the layer V ◁ G_{K_w} sends x to the class of the restriction of σ.

theorem TauCeti.ClassFieldTheory.character_infiniteArtinAt {K : Type} [Field K] (w : NumberField.InfinitePlace K) (V : OpenNormalSubgroup (AbsoluteGaloisGroup w.Completion)) (x : w.Completionˣ) (σ : Field.absoluteGaloisGroup w.Completion) (hσ : ↑σ = (infiniteArtinAt w) x) (χ : Additive (Abelianization (NormalLayer.ofOpenNormal V).Gal) →+ AddCircle 1) : χ (Additive.ofMul (Abelianization.of ((NormalLayer.galOfOpenNormalEquiv V).symm ↑((absoluteGaloisGroupRestrictEquiv w.Completion) σ)))) = (infiniteInvMap w) ((brInfl V) ((((NormalLayer.ofOpenNormal V).artinCharacterCup (unitsFormation w.Completion)) ((localGroundEquiv w.Completion V) (Additive.ofMul x))) χ))

The archimedean character formula χ(Art_w x) = inv_w(x ∪ δχ). If σ represents Art_w(x), then for every character χ of the abelianized Galois group of a layer V ◁ G_{K_w}, the value of χ at the class of σ is the archimedean Brauer invariant of the inflation of the cup product of x with the connecting class of χ.

@[simp]

theorem TauCeti.ClassFieldTheory.infiniteArtinAt_eq_one_of_isComplex {K : Type} [Field K] (w : NumberField.InfinitePlace K) (hw : w.IsComplex) (x : w.Completionˣ) : (infiniteArtinAt w) x = 1

The archimedean Artin map is trivial at a complex place: the absolute Galois group of K_w ≅ ℂ is trivial.

theorem TauCeti.ClassFieldTheory.infiniteArtinAt_eq_one_iff_of_isReal {K : Type} [Field K] (w : NumberField.InfinitePlace K) (hw : w.IsReal) (x : w.Completionˣ) : (infiniteArtinAt w) x = 1 ↔ 0 < (NumberField.InfinitePlace.Completion.extensionEmbeddingOfIsReal hw) ↑x

The kernel of the real Artin map is ℝ_{>0}: at a real place, Art_w(x) is trivial exactly when the image of x in ℝ is positive, so that the kernel is the norm group of ℂ/ℝ.

theorem TauCeti.ClassFieldTheory.infiniteArtinAt_rootsOfUnity_of_isReal {K : Type} [Field K] (w : NumberField.InfinitePlace K) (hw : w.IsReal) (m : ℕ) [NeZero m] (x : w.Completionˣ) (σ : Field.absoluteGaloisGroup w.Completion) (hσ : ↑σ = (infiniteArtinAt w) x) {z : AlgebraicClosure w.Completion} (hz : z ^ m = 1) : σ.toRingEquiv z = z ^ (↑((realCyclotomicSymbol m) ((Units.map ↑(NumberField.InfinitePlace.Completion.extensionEmbeddingOfIsReal hw)) x))).val

The real Artin map on roots of unity. At a real place, a lift σ of Art_w(x) acts on the m-th roots of unity through realCyclotomicSymbol m at the image of x in ℝ: trivially for x > 0, and by ζ ↦ ζ⁻¹, complex conjugation, for x < 0.

theorem TauCeti.ClassFieldTheory.abelianizedLocalCyclotomicCharacter_infiniteArtinAt_eq_neg_one_of_neg {K : Type} [Field K] (w : NumberField.InfinitePlace K) (hw : w.IsReal) (p : ℕ) [Fact (Nat.Prime p)] {x : w.Completionˣ} (hx : (NumberField.InfinitePlace.Completion.extensionEmbeddingOfIsReal hw) ↑x < 0) : (abelianizedLocalCyclotomicCharacter p w.Completion) ((infiniteArtinAt w) x) = -1

The cyclotomic character of the real Artin symbol of a negative element. At a real place, the p-adic cyclotomic character of Art_w(x) is -1 for x < 0: a lift of the symbol inverts every root of unity.

theorem TauCeti.ClassFieldTheory.infiniteArtinAt_norm {K : Type} [Field K] {L : Type} [Field L] [Algebra K L] (w : NumberField.InfinitePlace L) (v : NumberField.InfinitePlace K) [w.LiesOver v] [Module.Finite v.Completion w.Completion] (iota : w.Completion →ₐ[v.Completion] SeparableClosure v.Completion) (x : w.Completionˣ) (τ : Field.absoluteGaloisGroup w.Completion) (hτ : ↑τ = (infiniteArtinAt w) x) : ↑((absoluteGaloisGroupExtend v.Completion w.Completion iota) τ) = (infiniteArtinAt v) ((Units.map (Algebra.norm v.Completion)) x)

Norm functoriality at the archimedean places, the analogue of artinMap_norm: for a place w of L over v, embedded by iota, the image in G_{K_v}^ab of a lift of Art_w(x) is Art_v(N_{L_w/K_v} x). For ℝ/ℝ the norm is the identity, and for ℂ/ℝ and ℂ/ℂ both sides are trivial, N(x) = |x|² being positive in the first case.