Local Artin symbols on roots of unity

Let K be a nonarchimedean local field whose residue field has q elements, and let π be a uniformizer of K. For every finite Galois extension L/K, the local Artin symbol of π acts on the roots of unity of L of order prime to q by ζ ↦ ζ ^ q. The extension need not be unramified: such roots of unity generate an unramified subextension, on which the Artin symbol of π is arithmetic Frobenius.

This is the local cyclotomic input of the cyclotomic normalization of the local Artin map: over ℚ_ℓ, the Artin symbol of ℓ acts on the pⁿ-th roots of unity, p ≠ ℓ, by ζ ↦ ζ ^ ℓ (localArtinMap_cyclotomic_padic). For ℚ₂(ζ₅)/ℚ₂, which is unramified of degree four, the Artin symbol of 2 is ζ₅ ↦ ζ₅ ^ 2 (localArtinMap_Q2_zeta5); with geometric Frobenius the exponent would be 3.

The same input computes the p-adic cyclotomic character of absolute Artin symbols when p is not the residue characteristic: the Artin symbol of a unit lies in inertia, which fixes the roots of unity of p-power order, and that of a uniformizer is a Frobenius lift, which raises them to the q-th power, so χ_p(Art_K(x)) = q ^ v_K(x). For every p, norm functoriality of the Artin map reduces the cyclotomic character of the Artin symbols of a finite extension L/K to those of K: χ_L(Art_L(x)) = χ_K(Art_K(N_{L/K} x)). When p is the residue characteristic, this passes the cyclotomic character of Artin symbols from ℚ_p to its finite extensions.

On the roots of unity of p-power order, the Artin symbol of p over ℚ_p acts trivially: p is the norm of ζ - 1 from ℚ_p(ζ) for every primitive pⁿ-th root of unity ζ with pⁿ ≠ 2. So the p-adic cyclotomic character takes the value 1 on every lift of Art_{ℚ_p}(p) to the absolute Galois group (localCyclotomicCharacter_artinMap_padic_uniformizer). Together with the value of the cyclotomic character on the Artin symbols of units, this determines the cyclotomic character on the whole image of the Artin map of ℚ_p.

Over ℚ_p, the cyclotomic character and the action on the roots of unity of order prime to p can be prescribed independently: for u ∈ ℤ_pˣ and f ≥ 1 some ρ ∈ G_{ℚ_p} has χ_cyc(ρ) = u and acts on the (p^f − 1)-st roots of unity as ζ ↦ ζ ^ p (exists_localCyclotomicCharacter_eq_and_apply_of_pow_eq_one). This is the finite-level linear disjointness of ℚ_p(μ_{p^∞}) and the unramified extension of degree f that the comparison of the Artin symbols of units with the explicit cyclotomic symbols needs.

Since the image of the absolute Artin map is dense in G_K^ab, the image of the p-adic cyclotomic character of G_K is the closure of its values on Artin symbols (range_localCyclotomicCharacter). This is how the image is computed from evaluations of the cyclotomic character at units and at a uniformizer.

Main results

• TauCeti.ClassFieldTheory.localArtinMap_cyclotomic_uniformizer: the Artin symbol of a uniformizer raises every root of unity of order prime to q to the q-th power.
• TauCeti.ClassFieldTheory.localArtinMap_cyclotomic_padic: over ℚ_[p], the Artin symbol of p raises every root of unity of order prime to p to the p-th power.
• TauCeti.ClassFieldTheory.localArtinMap_Q2_zeta5: over ℚ_[2], the Artin symbol of 2 sends a fifth root of unity ζ to ζ ^ 2.
• TauCeti.ClassFieldTheory.abelianizedLocalCyclotomicCharacter_artinMap: for p different from the residue characteristic, χ_p(Art_K(x)) = q ^ v_K(x).
• TauCeti.ClassFieldTheory.abelianizedLocalCyclotomicCharacter_artinMap_norm: the cyclotomic character of the Artin symbol of x ∈ Lˣ is that of the Artin symbol of N_{L/K} x.
• TauCeti.ClassFieldTheory.abelianizedLocalCyclotomicCharacter_artinMap_congr: the cyclotomic character of the Artin symbols is unchanged by a continuous isomorphism of local fields.
• TauCeti.ClassFieldTheory.localCyclotomicCharacter_artinMap_padic_uniformizer: the p-adic cyclotomic character of the Artin symbol of p over ℚ_[p] is 1.
• TauCeti.ClassFieldTheory.exists_localCyclotomicCharacter_eq_and_apply_of_pow_eq_one: an element of G_{ℚ_p} with prescribed cyclotomic character acting as Frobenius on the (p^f − 1)-st roots of unity.
• TauCeti.ClassFieldTheory.range_localCyclotomicCharacter: the image of the cyclotomic character of G_K is the closure of its values on the absolute Artin symbols.

Implementation notes

The roots of unity in question lie in the unramified extension unramifiedExtension K Kˢ f of some degree f, where the finite local Artin map sends π to arithmetic Frobenius (localArtinMap_uniformizer). The absolute local Artin map compares the Artin symbol on this extension with the Artin symbol on L (artinMap_restrict), and the action on a root of unity factors through the abelian group (ℤ/nℤ)ˣ (IsPrimitiveRoot.autToPow), so it only depends on the class of an automorphism in Gal(L/K)ᵃᵇ.

For the roots of unity of p-power order over ℚ_[p], the norm computation is Mathlib's IsPrimitiveRoot.sub_one_norm_isPrimePow, which needs Φ_{pⁿ} to be irreducible over ℚ_[p] (TauCeti.irreducible_cyclotomic_prime_pow_ratPadic). A norm has trivial finite Artin symbol (localArtinMap_eq_zero_iff), so the restriction of a lift of Art_{ℚ_p}(p) to ℚ_p(ζ) is trivial by artinMap_restrict and the injectivity of IsPrimitiveRoot.autToPow.

For the independent prescription, the cyclotomic character of G_{ℚ_p} is surjective (surjective_localCyclotomicCharacter_ratPadic), so some ρ₀ has χ_cyc(ρ₀) = u. A lift τ of the Artin symbol of p has trivial cyclotomic character and is an arithmetic Frobenius lift; its restriction to the unramified extension of degree f is that extension's Frobenius, which generates its Galois group (IsArithFrobeniusLift.zpowers_restrictNormalHom_unramifiedExtension). So ρ₀ restricts there to a power τ ^ j, and ρ = ρ₀ τ⁻ʲ τ has character u and acts on the unramified extension as τ does.

References

• J.-P. Serre, Local Fields, Chapter XIII, §4.
• J. Neukirch, Algebraic Number Theory, Chapter V, §1, and §2 for the norm residue symbol over ℚ_p.

theorem TauCeti.ClassFieldTheory.localArtinMap_cyclotomic_uniformizer (K : Type) [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] (L : Type u_1) [Field L] [Algebra K L] [FiniteDimensional K L] [IsGalois K L] (ι : L →ₐ[K] SeparableClosure K) {π : Kˣ} (hπ : IsUniformizer K π) {σ : Gal(L/K)} (hσ : (localArtinMap K L ι) (Additive.ofMul π) = Additive.ofMul (Abelianization.of σ)) {m : ℕ} (hm : (Nat.card (IsLocalRing.ResidueField ↥(ValuativeRel.valuation K).integer)).Coprime m) {ζ : L} (hζ : ζ ^ m = 1) : σ ζ = ζ ^ Nat.card (IsLocalRing.ResidueField ↥(ValuativeRel.valuation K).integer)

The local Artin symbol of a uniformizer on roots of unity. Let L/K be a finite Galois extension of a nonarchimedean local field whose residue field has q elements, and let σ represent the local Artin symbol of a uniformizer π in Gal(L/K)ᵃᵇ. Then σ ζ = ζ ^ q for every ζ ∈ L with ζ ^ m = 1 and m prime to q.

theorem TauCeti.ClassFieldTheory.localArtinMap_cyclotomic_padic (p : ℕ) [Fact (Nat.Prime p)] (L : Type u_1) [Field L] [Algebra ℚ_[p] L] [FiniteDimensional ℚ_[p] L] [IsGalois ℚ_[p] L] (ι : L →ₐ[ℚ_[p]] SeparableClosure ℚ_[p]) {σ : Gal(L/ℚ_[p])} (hσ : (localArtinMap ℚ_[p] L ι) (Additive.ofMul (Units.mk0 ↑p ⋯)) = Additive.ofMul (Abelianization.of σ)) {m : ℕ} (hm : p.Coprime m) {ζ : L} (hζ : ζ ^ m = 1) : σ ζ = ζ ^ p

The local Artin symbol of p on roots of unity over ℚ_[p]. If σ represents the Artin symbol of p for a finite Galois extension L/ℚ_[p], then σ ζ = ζ ^ p for every ζ ∈ L with ζ ^ m = 1 and m prime to p.

theorem TauCeti.ClassFieldTheory.localArtinMap_Q2_zeta5 (E : Type u_1) [Field E] [Algebra ℚ_[2] E] [FiniteDimensional ℚ_[2] E] [IsGalois ℚ_[2] E] (ι : E →ₐ[ℚ_[2]] SeparableClosure ℚ_[2]) {σ : Gal(E/ℚ_[2])} (hσ : (localArtinMap ℚ_[2] E ι) (Additive.ofMul (Units.mk0 2 ⋯)) = Additive.ofMul (Abelianization.of σ)) {ζ : E} (hζ : ζ ^ 5 = 1) : σ ζ = ζ ^ 2

The ℚ₂(ζ₅) test of local reciprocity. Over ℚ_[2], the Artin symbol of 2 sends a fifth root of unity ζ to ζ ^ 2. The fifth roots of unity generate the unramified extension of degree four of ℚ_[2], and geometric Frobenius would send ζ to ζ ^ 3.

The cyclotomic character of absolute Artin symbols

theorem TauCeti.ClassFieldTheory.abelianizedLocalCyclotomicCharacter_artinMap (K : Type) [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] {p : ℕ} [Fact (Nat.Prime p)] {u : ℤ_[p]ˣ} (hu : ↑u = ↑(Nat.card (IsLocalRing.ResidueField ↥(ValuativeRel.valuation K).integer))) (x : Kˣ) : (abelianizedLocalCyclotomicCharacter p K) ((artinMap K) x) = u ^ Multiplicative.toAdd ((normalizedValuation K) x)

The p-adic cyclotomic character of an Artin symbol, p away from the residue characteristic. Let q be the cardinality of the residue field of K, let u ∈ ℤ_pˣ be the unit q, and let x ∈ Kˣ. Then the p-adic cyclotomic character of the absolute Artin symbol of x is q ^ v_K(x):

χ_p (Art_K x) = q ^ v_K(x).

That q is a unit of ℤ_[p] forces p to differ from the residue characteristic.

theorem TauCeti.ClassFieldTheory.abelianizedLocalCyclotomicCharacter_artinMap_norm (K : Type) [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] (p : ℕ) [Fact (Nat.Prime p)] {L : Type} [Field L] [Algebra K L] [FiniteDimensional K L] [Algebra.IsSeparable K L] [ValuativeRel L] [TopologicalSpace L] [IsNonarchimedeanLocalField L] [ValuativeExtension K L] (x : Lˣ) : (abelianizedLocalCyclotomicCharacter p L) ((artinMap L) x) = (abelianizedLocalCyclotomicCharacter p K) ((artinMap K) ((Algebra.normUnits K) x))

The cyclotomic character of the Artin symbol of a norm. Let L/K be a finite separable extension of nonarchimedean local fields. The absolute Artin symbol of x ∈ Lˣ and that of its norm N_{L/K} x have the same p-adic cyclotomic character:

χ_L (Art_L x) = χ_K (Art_K (N_{L/K} x)).

This reduces the cyclotomic character of the Artin symbols of a finite extension of ℚ_p to those of ℚ_p itself.

theorem TauCeti.ClassFieldTheory.abelianizedLocalCyclotomicCharacter_artinMap_congr (K : Type) [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] (p : ℕ) [Fact (Nat.Prime p)] {K' : Type} [Field K'] [ValuativeRel K'] [TopologicalSpace K'] [IsNonarchimedeanLocalField K'] (e : K ≃+* K') (he : Continuous ⇑e) (x : Kˣ) : (abelianizedLocalCyclotomicCharacter p K) ((artinMap K) x) = (abelianizedLocalCyclotomicCharacter p K') ((artinMap K') ((Units.map e.toMonoidHom) x))

The cyclotomic character of Artin symbols is natural in the local field. For a continuous isomorphism e : K ≃+* K' of nonarchimedean local fields, the absolute Artin symbols of x ∈ Kˣ and of e x ∈ K'ˣ have the same p-adic cyclotomic character:

χ_K (Art_K x) = χ_{K'} (Art_{K'} (e x)).

This is how the cyclotomic character of Artin symbols is computed in a model of a local field, such as ℚ_[p] for a completion of ℚ.

The Artin symbol of p on roots of unity of p-power order

theorem TauCeti.ClassFieldTheory.localCyclotomicCharacter_artinMap_padic_uniformizer (p : ℕ) [Fact (Nat.Prime p)] (σ : Field.absoluteGaloisGroup ℚ_[p]) (hσ : ↑σ = (artinMap ℚ_[p]) (Units.mk0 ↑p ⋯)) : (localCyclotomicCharacter p ℚ_[p]) σ = 1

The cyclotomic character of the Artin symbol of p over ℚ_[p]. If σ in the absolute Galois group of ℚ_[p] represents the absolute local Artin symbol of p, then χ_cyc(σ) = 1 for the p-adic cyclotomic character: σ fixes every root of unity of p-power order, because p is a norm from every ℚ_p(μ_{pⁿ}).

Prescribing the cyclotomic character and the unramified action

theorem TauCeti.ClassFieldTheory.exists_localCyclotomicCharacter_eq_and_apply_of_pow_eq_one (p : ℕ) [Fact (Nat.Prime p)] (u : ℤ_[p]ˣ) {f : ℕ} (hf : f ≠ 0) : ∃ (ρ : Field.absoluteGaloisGroup ℚ_[p]), (localCyclotomicCharacter p ℚ_[p]) ρ = u ∧ ∀ (z : AlgebraicClosure ℚ_[p]), z ^ (p ^ f - 1) = 1 → ρ z = z ^ p

Independent prescription of the cyclotomic character and the unramified action. For u ∈ ℤ_pˣ and f ≠ 0 there is ρ ∈ G_{ℚ_p} whose p-adic cyclotomic character is u and which raises every (p ^ f − 1)-st root of unity to the p-th power.

The image of the cyclotomic character

theorem TauCeti.ClassFieldTheory.range_localCyclotomicCharacter (K : Type) [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] (p : ℕ) [Fact (Nat.Prime p)] : (localCyclotomicCharacter p K).range = ((abelianizedLocalCyclotomicCharacter p K).comp (artinMap K)).range.topologicalClosure

The image of the cyclotomic character is generated by the Artin symbols. For a nonarchimedean local field K, the image of the p-adic cyclotomic character of G_K is the closure of its values on the image of the absolute local Artin map:

χ_cyc(G_K) = closure (χ_cyc(Art_K(Kˣ))).

No relation between p and the residue characteristic of K is assumed.

The unit values of χ_cyc ∘ Art_K do not determine the image on their own: for p = 3 and K = ℚ_3(√3), the extension K(μ_3) = K(√-1) is unramified over K, so the image is all of ℤ_3ˣ, while the norms of units of K fill only the index-two subgroup 1 + 3ℤ_3.

theorem TauCeti.ClassFieldTheory.range_localCyclotomicCharacter_le_iff (K : Type) [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] (p : ℕ) [Fact (Nat.Prime p)] {H : Subgroup ℤ_[p]ˣ} (hH : IsClosed ↑H) : (localCyclotomicCharacter p K).range ≤ H ↔ ∀ (x : Kˣ), (abelianizedLocalCyclotomicCharacter p K) ((artinMap K) x) ∈ H

The image of the p-adic cyclotomic character of a nonarchimedean local field K lies in a closed subgroup H of ℤ_pˣ exactly when the cyclotomic character of every absolute Artin symbol does.