The local Artin symbols at the infinite places in a finite Galois extension

Let L/K be a finite normal extension of fields and v an infinite place of K, with completion K_v, which is ℝ or ℂ. The archimedean Artin map infiniteArtinAt v : K_vˣ → G_{K_v}^ab, read in Gal(L/K)^ab by restricting along a place of L above v (TauCeti.decompositionRestrict), is the local Artin symbol at v

infiniteLocalArtinAt K L v : K_vˣ →* Gal(L/K)^ab.

In global class field theory it is the local factor at v of the global Artin map. It is a reading of infiniteArtinAt, not a second archimedean Artin map, and it is compatible with restriction to a normal subextension (infiniteLocalArtinAt_comp).

For a place w of L above v the symbol is explicit, through the decomposition group of w, which acts on L_w (NumberField.InfinitePlace.decompositionHom).

• If w is unramified over K, then L_w = K_v and the symbol is trivial (infiniteLocalArtinAt_eq_one_of_isUnramified); in particular at a complex place of K (infiniteLocalArtinAt_eq_one_of_isComplex).
• At a real place v the symbol of a positive element is trivial (infiniteLocalArtinAt_eq_one_of_pos). If L/K is Galois and w is ramified over K, so that w is complex and its decomposition group has order two, the symbol of a negative element is the class of the nontrivial element of that group, the complex conjugation at w (TauCeti.NumberField.complexConjugationAt, infiniteLocalArtinAt_eq_complexConjugationAt).

Consequently, for L/K Galois, the image of the symbol is the image of the decomposition group of w (range_infiniteLocalArtinAt), the local norms N_{L_w/K_v}(L_wˣ) lie in its kernel (normGroup_le_ker_infiniteLocalArtinAt), and for L/K abelian they are exactly its kernel (infiniteLocalArtinAt_eq_one_iff_mem_normGroup): the archimedean form of local reciprocity K_vˣ / N_{L_w/K_v}(L_wˣ) ≃ Gal(L_w/K_v).

Main definitions

• TauCeti.ClassFieldTheory.infiniteLocalArtinAt K L v: the local Artin symbol at the infinite place v, with values in Gal(L/K)^ab.

Main results

• TauCeti.ClassFieldTheory.infiniteLocalArtinAt_eq_of_decompositionHom: the symbol of x is the class of the element of the decomposition group of w acting on L_w as a representative of the archimedean Artin symbol of x.
• TauCeti.ClassFieldTheory.infiniteLocalArtinAt_eq_one_of_isUnramified: the symbol is trivial at a place unramified in L.
• TauCeti.ClassFieldTheory.infiniteLocalArtinAt_eq_complexConjugationAt: at a complex place w over a real place, a negative element has as symbol the class of complex conjugation at w.
• TauCeti.ClassFieldTheory.range_infiniteLocalArtinAt: the image of the symbol is the image of the decomposition group.
• TauCeti.ClassFieldTheory.normGroup_le_ker_infiniteLocalArtinAt, TauCeti.ClassFieldTheory.infiniteLocalArtinAt_eq_one_iff_mem_normGroup: local norms have trivial symbol, and for L/K abelian exactly the local norms do.

References

• J. Neukirch, Algebraic Number Theory, Chapter II, §8 (infinite places and their decomposition groups) and Chapter VI, §5 (the global reciprocity law and its local factors).
• J. S. Milne, Class Field Theory, Chapter VII, §8 (the local Artin symbol at an archimedean place).

The local Artin symbol

noncomputable def TauCeti.ClassFieldTheory.infiniteLocalArtinAt (K : Type) [Field K] (L : Type) [Field L] [Algebra K L] [FiniteDimensional K L] [Normal K L] (v : NumberField.InfinitePlace K) : v.Completionˣ →* Abelianization Gal(L/K)

The local Artin symbol at an infinite place v of K, with values in the abelianized Galois group of a finite normal extension L/K: the archimedean Artin map of the completion K_v, read in Gal(L/K)^ab by restriction along a place of L above v (TauCeti.decompositionRestrict). It does not depend on the choice of that place.

theorem TauCeti.ClassFieldTheory.infiniteLocalArtinAt_apply {K : Type} [Field K] {L : Type} [Field L] [Algebra K L] [FiniteDimensional K L] [Normal K L] (v : NumberField.InfinitePlace K) (x : v.Completionˣ) : (infiniteLocalArtinAt K L v) x = (decompositionRestrict K v.Completion L) ((infiniteArtinAt v) x)

The local Artin symbol at v is the archimedean Artin map of K_v followed by restriction to L.

theorem TauCeti.ClassFieldTheory.infiniteLocalArtinAt_eq_of_mk_eq_infiniteArtinAt {K : Type} [Field K] {L : Type} [Field L] [Algebra K L] [FiniteDimensional K L] [Normal K L] (v : NumberField.InfinitePlace K) {x : v.Completionˣ} (τ : Field.absoluteGaloisGroup v.Completion) (hτ : ↑τ = (infiniteArtinAt v) x) (j : L →ₐ[K] AlgebraicClosure v.Completion) (σ : Gal(L/K)) (hσ : ∀ (y : L), j (σ y) = τ.toRingEquiv (j y)) : (infiniteLocalArtinAt K L v) x = Abelianization.of σ

The local Artin symbol through a representative. If τ ∈ G_{K_v} represents the archimedean Artin symbol of x, then for every K-embedding j : L → K_vᵃˡᵍ the local Artin symbol of x at v is the class of the automorphism σ of L with j ∘ σ = τ ∘ j.

theorem TauCeti.ClassFieldTheory.infiniteLocalArtinAt_comp {K : Type} [Field K] {L : Type} [Field L] [Algebra K L] [FiniteDimensional K L] [Normal K L] (v : NumberField.InfinitePlace K) {M : Type} [Field M] [Algebra K M] [FiniteDimensional K M] [Normal K M] (f : M →ₐ[K] L) : (Abelianization.map f.restrictNormalHom).comp (infiniteLocalArtinAt K L v) = infiniteLocalArtinAt K M v

Compatibility with restriction to a normal subextension. For a K-embedding f : M → L of a finite normal extension M/K, the local Artin symbol at v in Gal(L/K)^ab, restricted to M along f, is the local Artin symbol at v in Gal(M/K)^ab.

@[simp]

theorem TauCeti.ClassFieldTheory.infiniteLocalArtinAt_eq_one_of_isComplex {K : Type} [Field K] {L : Type} [Field L] [Algebra K L] [FiniteDimensional K L] [Normal K L] {v : NumberField.InfinitePlace K} (hv : v.IsComplex) (x : v.Completionˣ) : (infiniteLocalArtinAt K L v) x = 1

The local Artin symbol at a complex place is trivial: the absolute Galois group of K_v ≅ ℂ is trivial.

theorem TauCeti.ClassFieldTheory.infiniteLocalArtinAt_eq_one_of_pos {K : Type} [Field K] {L : Type} [Field L] [Algebra K L] [FiniteDimensional K L] [Normal K L] {v : NumberField.InfinitePlace K} (hv : v.IsReal) {x : v.Completionˣ} (hx : 0 < (NumberField.InfinitePlace.Completion.extensionEmbeddingOfIsReal hv) ↑x) : (infiniteLocalArtinAt K L v) x = 1

Positive elements have trivial local Artin symbol at a real place: they lie in the kernel of the real Artin map.

The local Artin symbol through the decomposition group

theorem TauCeti.ClassFieldTheory.infiniteLocalArtinAt_eq_of_decompositionHom {K : Type} [Field K] {L : Type} [Field L] [Algebra K L] [FiniteDimensional K L] [Normal K L] (v : NumberField.InfinitePlace K) (w : NumberField.InfinitePlace L) [w.LiesOver v] {x : v.Completionˣ} (τ : Field.absoluteGaloisGroup v.Completion) (hτ : ↑τ = (infiniteArtinAt v) x) (ι : w.Completion →ₐ[v.Completion] AlgebraicClosure v.Completion) (σ : ↥(MulAction.stabilizer Gal(L/K) w)) (hσ : ∀ (y : w.Completion), ι (((v.decompositionHom w) σ) y) = τ.toRingEquiv (ι y)) : (infiniteLocalArtinAt K L v) x = Abelianization.of ↑σ

The local Artin symbol through the decomposition group. Let w be a place of L above v, ι : L_w → K_vᵃˡᵍ a K_v-embedding and τ ∈ G_{K_v} a representative of the archimedean Artin symbol of x. If σ is in the decomposition group of w and acts on L_w as τ does through ι, then the local Artin symbol of x at v is the class of σ.

theorem TauCeti.ClassFieldTheory.infiniteLocalArtinAt_eq_one_of_isUnramified {K : Type} [Field K] {L : Type} [Field L] [Algebra K L] [FiniteDimensional K L] [Normal K L] (v : NumberField.InfinitePlace K) (w : NumberField.InfinitePlace L) [w.LiesOver v] (hw : NumberField.InfinitePlace.IsUnramified K w) (x : v.Completionˣ) : (infiniteLocalArtinAt K L v) x = 1

The local Artin symbol at an unramified place is trivial. If a place w of L above v is unramified over K, then L_w = K_v, and every element of G_{K_v} acts trivially on it.

theorem TauCeti.ClassFieldTheory.normGroup_le_ker_infiniteLocalArtinAt {K : Type} [Field K] {L : Type} [Field L] [Algebra K L] [FiniteDimensional K L] [Normal K L] (v : NumberField.InfinitePlace K) (w : NumberField.InfinitePlace L) [w.LiesOver v] : normGroup v.Completion w.Completion ≤ (infiniteLocalArtinAt K L v).ker

Local norms have trivial local Artin symbol. For a place w of L above v, the norms from L_w lie in the kernel of the local Artin symbol at v: at an unramified place it is trivial, and at a complex place over a real place the norms are the positive elements.

theorem TauCeti.ClassFieldTheory.infiniteLocalArtinAt_eq_complexConjugationAt {K : Type} [Field K] {L : Type} [Field L] [Algebra K L] [FiniteDimensional K L] [Normal K L] (v : NumberField.InfinitePlace K) (w : NumberField.InfinitePlace L) [w.LiesOver v] [IsGalois K L] (hw : NumberField.InfinitePlace.IsRamified K w) {x : v.Completionˣ} (hx : (NumberField.InfinitePlace.Completion.extensionEmbeddingOfIsReal ⋯) ↑x < 0) : (infiniteLocalArtinAt K L v) x = Abelianization.of (NumberField.complexConjugationAt K w hw)

The local Artin symbol of a negative element is complex conjugation. Let L/K be Galois and w a place of L ramified over K, so that w is complex and the place v below it is real. Every x ∈ K_vˣ that is negative in K_v ≅ ℝ has as local Artin symbol the class of the complex conjugation at w, the nontrivial element of its decomposition group.

theorem TauCeti.ClassFieldTheory.range_infiniteLocalArtinAt {K : Type} [Field K] {L : Type} [Field L] [Algebra K L] [FiniteDimensional K L] [Normal K L] (v : NumberField.InfinitePlace K) (w : NumberField.InfinitePlace L) [w.LiesOver v] [IsGalois K L] : (infiniteLocalArtinAt K L v).range = Subgroup.map Abelianization.of (MulAction.stabilizer Gal(L/K) w)

The image of the local Artin symbol is the decomposition group. For L/K Galois and w a place of L above v, the local Artin symbols at v are exactly the classes in Gal(L/K)^ab of the elements of the decomposition group of w.

theorem TauCeti.ClassFieldTheory.infiniteLocalArtinAt_eq_one_iff_mem_normGroup {K : Type} [Field K] {L : Type} [Field L] [Algebra K L] [FiniteDimensional K L] [Normal K L] (v : NumberField.InfinitePlace K) (w : NumberField.InfinitePlace L) [w.LiesOver v] [IsGalois K L] [IsMulCommutative Gal(L/K)] (x : v.Completionˣ) : (infiniteLocalArtinAt K L v) x = 1 ↔ x ∈ normGroup v.Completion w.Completion

For an abelian extension, the kernel of the local Artin symbol is the local norm group. If Gal(L/K) is commutative and w is a place of L above v, then x ∈ K_vˣ has trivial local Artin symbol at v exactly when it is a norm from L_w.