The local Artin symbols of a number field in a finite Galois extension

Let L/K be a finite normal extension of number fields and v a finite place of K with completion K_v. The absolute local Artin map artinMap K_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

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

In global class field theory it is the local factor of the global Artin map: the global Artin symbol of an idele is the product of the local Artin symbols of its components. It is compatible with restriction to a normal subextension (localArtinAt_comp).

For L/K Galois and a finite place w of L above v, the decomposition group of w is the Galois group of L_w/K_v (IsDedekindDomain.HeightOneSpectrum.decompositionEquiv), and the local Artin symbol at v is finite local reciprocity for L_w/K_v, read in Gal(L/K)^ab through that identification (localArtinAt_eq_map_normResidue). Consequently:

• the local norms N_{L_w/K_v}(L_wˣ) lie in its kernel (normGroup_le_ker_localArtinAt), with equality when L/K is abelian (localArtinAt_eq_one_iff_mem_normGroup), and its image is the image of the decomposition group of w (range_localArtinAt);
• at a place unramified in L, it is an arithmetic Frobenius at w raised to the normalized valuation (localArtinAt_eq_of_isArithFrobAt): a uniformizer goes to Frobenius (localArtinAt_uniformizer_eq_of_isArithFrobAt) and a unit to 1 (localArtinAt_eq_one_of_normalizedValuation_eq_one). For abelian L/K this Frobenius is the Artin automorphism TauCeti.NumberFieldArithmetic.artinElement of the ideal-theoretic Artin map (localArtinAt_eq_artinElement_zpow).

The last statement is the arithmetic content of the comparison between the global Artin map and the ideal-theoretic one at the unramified primes.

Main definitions

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

Main results

• TauCeti.ClassFieldTheory.localArtinAt_eq_of_mk_eq_artinMap: the local Artin symbol of x is the class of the automorphism of L induced, along any embedding of L into K_vᵃˡᵍ, by a representative of the absolute Artin symbol of x.
• TauCeti.ClassFieldTheory.localArtinAt_comp: compatibility with restriction to a normal subextension.
• TauCeti.ClassFieldTheory.localArtinAt_norm: compatibility with the local norm from a finite place of an intermediate field.
• TauCeti.ClassFieldTheory.localArtinAt_eq_map_normResidue: the local Artin symbol at v is finite local reciprocity for L_w/K_v, read through the decomposition group of w.
• TauCeti.ClassFieldTheory.normGroup_le_ker_localArtinAt: local norms have trivial local Artin symbol; TauCeti.ClassFieldTheory.localArtinAt_eq_one_iff_mem_normGroup: for L/K abelian, exactly the local norms do.
• TauCeti.ClassFieldTheory.range_localArtinAt: the image of the local Artin symbol is the image of the decomposition group.
• TauCeti.ClassFieldTheory.localArtinAt_eq_of_isArithFrobAt: at an unramified place, the local Artin symbol of x is an arithmetic Frobenius raised to the normalized valuation of x.
• TauCeti.ClassFieldTheory.localArtinAt_eq_artinElement_zpow: for L/K abelian, that Frobenius is the Artin automorphism of the ideal-theoretic Artin map.

References

• J. Neukirch, Algebraic Number Theory, Chapter II, §9 (decomposition groups and completions) and Chapter VI, §5 (the global reciprocity law and its local factors).

The local Artin symbol

noncomputable def TauCeti.ClassFieldTheory.localArtinAt (K : Type) [Field K] [NumberField K] (L : Type) [Field L] [Algebra K L] [FiniteDimensional K L] [Normal K L] (v : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)) : (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v)ˣ →* Abelianization Gal(L/K)

The local Artin symbol at a finite place v of a number field K, with values in the abelianized Galois group of a finite normal extension L/K: the absolute local 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.localArtinAt_apply {K : Type} [Field K] [NumberField K] {L : Type} [Field L] [Algebra K L] [FiniteDimensional K L] [Normal K L] (v : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)) (x : (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v)ˣ) : (localArtinAt K L v) x = (decompositionRestrict K (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v) L) ((artinMap (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v)) x)

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

theorem TauCeti.ClassFieldTheory.localArtinAt_eq_of_mk_eq_artinMap {K : Type} [Field K] [NumberField K] {L : Type} [Field L] [Algebra K L] [FiniteDimensional K L] [Normal K L] (v : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)) {x : (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v)ˣ} (τ : Field.absoluteGaloisGroup (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v)) (hτ : ↑τ = (artinMap (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v)) x) (j : L →ₐ[K] AlgebraicClosure (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v)) (σ : Gal(L/K)) (hσ : ∀ (y : L), j (σ y) = τ.toRingEquiv (j y)) : (localArtinAt K L v) x = Abelianization.of σ

The local Artin symbol through a representative. If τ ∈ G_{K_v} represents the absolute local 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.localArtinAt_comp {K : Type} [Field K] [NumberField K] {L : Type} [Field L] [Algebra K L] [FiniteDimensional K L] [Normal K L] (v : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)) {M : Type} [Field M] [Algebra K M] [FiniteDimensional K M] [Normal K M] (f : M →ₐ[K] L) : (Abelianization.map f.restrictNormalHom).comp (localArtinAt K L v) = localArtinAt 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.

theorem TauCeti.ClassFieldTheory.localArtinAt_norm {K : Type} [Field K] [NumberField K] {L : Type} [Field L] [Algebra K L] [FiniteDimensional K L] [Normal K L] {E : Type} [Field E] [NumberField E] [Algebra K E] [Algebra E L] [IsScalarTower K E L] [FiniteDimensional E L] [Normal E L] (v : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)) (w : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers E)) [w.asIdeal.LiesOver v.asIdeal] (y : (IsDedekindDomain.HeightOneSpectrum.adicCompletion E w)ˣ) : (localArtinAt K L v) ((Algebra.normUnits (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v)) y) = (Abelianization.map (AlgEquiv.restrictScalarsHom K)) ((localArtinAt E L w) y)

Norm functoriality in the ground field. Let K ⊆ E ⊆ L with L/K finite normal, and let w be a finite place of E above the finite place v of K. The local Artin symbol at v of the local norm N_{E_w/K_v}(y) is the local Artin symbol at w of y, read in Gal(L/K)^ab through the inclusion Gal(L/E) ≤ Gal(L/K):

Art_v (N_{E_w/K_v} y) = Art_w y.

It is the norm functoriality artinMap_norm of the absolute local Artin maps, read through the decomposition groups. The instances on L/E follow from those on L/K.

Comparison with finite local reciprocity

theorem TauCeti.ClassFieldTheory.localArtinAt_eq_map_normResidue {K : Type} [Field K] [NumberField K] {L : Type} [Field L] [Algebra K L] [NumberField L] [IsGalois K L] (v : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)) (w : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers L)) [w.asIdeal.LiesOver v.asIdeal] (x : (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v)ˣ) : (localArtinAt K L v) x = (Abelianization.map ((MulAction.stabilizer Gal(L/K) w.asIdeal).subtype.comp (v.decompositionEquiv w).symm.toMonoidHom)) ((normResidue (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v) (IsDedekindDomain.HeightOneSpectrum.adicCompletion L w)) ↑x)

The local Artin symbol is finite local reciprocity at a place above v. For L/K Galois and a finite place w of L above v, the local Artin symbol at v of x ∈ K_vˣ is the image of its norm residue symbol in Gal(L_w/K_v)^ab under the identification of Gal(L_w/K_v) with the decomposition group of w (IsDedekindDomain.HeightOneSpectrum.decompositionEquiv).

theorem TauCeti.ClassFieldTheory.normGroup_le_ker_localArtinAt {K : Type} [Field K] [NumberField K] {L : Type} [Field L] [Algebra K L] [NumberField L] [IsGalois K L] (v : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)) (w : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers L)) [w.asIdeal.LiesOver v.asIdeal] : normGroup (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v) (IsDedekindDomain.HeightOneSpectrum.adicCompletion L w) ≤ (localArtinAt K L v).ker

Local norms have trivial local Artin symbol. For L/K Galois and w a finite place of L above v, the norms from L_w lie in the kernel of the local Artin symbol at v.

theorem TauCeti.ClassFieldTheory.range_localArtinAt {K : Type} [Field K] [NumberField K] {L : Type} [Field L] [Algebra K L] [NumberField L] [IsGalois K L] (v : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)) (w : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers L)) [w.asIdeal.LiesOver v.asIdeal] : (localArtinAt K L v).range = Subgroup.map Abelianization.of (MulAction.stabilizer Gal(L/K) w.asIdeal)

The image of the local Artin symbol is the decomposition group. For L/K Galois and w a finite 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.localArtinAt_eq_one_iff_mem_normGroup {K : Type} [Field K] [NumberField K] {L : Type} [Field L] [Algebra K L] [NumberField L] [IsGalois K L] (v : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)) (w : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers L)) [w.asIdeal.LiesOver v.asIdeal] [IsMulCommutative Gal(L/K)] (x : (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v)ˣ) : (localArtinAt K L v) x = 1 ↔ x ∈ normGroup (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v) (IsDedekindDomain.HeightOneSpectrum.adicCompletion L w)

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 finite 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.

Unramified places

theorem TauCeti.ClassFieldTheory.localArtinAt_eq_of_isArithFrobAt {K : Type} [Field K] [NumberField K] {L : Type} [Field L] [Algebra K L] [NumberField L] [IsGalois K L] (v : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)) (w : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers L)) [w.asIdeal.LiesOver v.asIdeal] [Algebra.IsUnramifiedAt (NumberField.RingOfIntegers K) w.asIdeal] {σ : Gal(L/K)} (hσ : IsArithFrobAt (NumberField.RingOfIntegers K) σ w.asIdeal) (x : (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v)ˣ) : (localArtinAt K L v) x = Abelianization.of σ ^ Multiplicative.toAdd ((normalizedValuation (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v)) x)

The local Artin symbol at an unramified place is a power of Frobenius. If w is unramified over v and σ ∈ Gal(L/K) is an arithmetic Frobenius at w, then the local Artin symbol at v of x ∈ K_vˣ is the class of σ raised to the normalized valuation of x.

theorem TauCeti.ClassFieldTheory.localArtinAt_uniformizer_eq_of_isArithFrobAt {K : Type} [Field K] [NumberField K] {L : Type} [Field L] [Algebra K L] [NumberField L] [IsGalois K L] (v : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)) (w : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers L)) [w.asIdeal.LiesOver v.asIdeal] [Algebra.IsUnramifiedAt (NumberField.RingOfIntegers K) w.asIdeal] {σ : Gal(L/K)} (hσ : IsArithFrobAt (NumberField.RingOfIntegers K) σ w.asIdeal) {π : (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v)ˣ} (hπ : IsUniformizer (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v) π) : (localArtinAt K L v) π = Abelianization.of σ

A uniformizer has Frobenius as local Artin symbol at a place unramified in L.

theorem TauCeti.ClassFieldTheory.localArtinAt_eq_one_of_normalizedValuation_eq_one {K : Type} [Field K] [NumberField K] {L : Type} [Field L] [Algebra K L] [NumberField L] [IsGalois K L] (v : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)) (w : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers L)) [w.asIdeal.LiesOver v.asIdeal] [Algebra.IsUnramifiedAt (NumberField.RingOfIntegers K) w.asIdeal] {u : (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v)ˣ} (hu : (normalizedValuation (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v)) u = 1) : (localArtinAt K L v) u = 1

Units have trivial local Artin symbol at a place v below a place w of L unramified over it.

Abelian extensions

theorem TauCeti.ClassFieldTheory.localArtinAt_eq_artinElement_zpow {K : Type} [Field K] [NumberField K] {L : Type} [Field L] [Algebra K L] [NumberField L] [IsGalois K L] (hab : ∀ (σ τ : Gal(L/K)), Commute σ τ) (v : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)) (hur : ∀ (Q : Ideal (NumberField.RingOfIntegers L)) [inst : Q.IsPrime] [Q.LiesOver v.asIdeal], Algebra.IsUnramifiedAt (NumberField.RingOfIntegers K) Q) (x : (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v)ˣ) : (localArtinAt K L v) x = Abelianization.of (NumberFieldArithmetic.artinElement hab v.asIdeal hur) ^ Multiplicative.toAdd ((normalizedValuation (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v)) x)

At an unramified place of an abelian extension, the local Artin symbol is the Artin automorphism of the ideal-theoretic Artin map raised to the normalized valuation: the local Artin symbol at v of x ∈ K_vˣ is artinElement hab v hur ^ v(x).