Documentation

TauCeti.NumberTheory.ClassFieldTheory.WeilGroup.ArtinMap

The image of the local Artin map and the Artin map into the Weil group #

Let K be a nonarchimedean local field. The absolute local Artin map artinMap K : Kˣ →* G_K^ab has dense image, but it is not surjective. This file identifies its image: it is the subgroup integralUnramifiedSubgroup K of classes whose unramified coordinate in ℤ̂ is an integer (range_artinMap), which is also the image of the abelianized Weil group W_K^ab → G_K^ab (range_weilToAbsoluteAbelianization). So a class in G_K^ab is an Artin symbol exactly when it is the class of an element of the Weil group (mem_range_artinMap_iff).

Since W_K^ab → G_K^ab is injective, the Artin map therefore factors uniquely through W_K^ab, as weilArtinMap K : Kˣ →* W_K^ab. Unlike artinMap K, it is surjective, and it is a quotient map of topological groups: it is continuous, because the topology of W_K^ab is the one induced by x ↦ (x, deg x) into G_K^ab × ℤ and the degree of weilArtinMap K x is the normalized valuation of x, and it is open by the open mapping theorem, since Kˣ is σ-compact and W_K^ab is locally compact. Its kernel is that of artinMap K.

The inclusion of the image in integralUnramifiedSubgroup K is the computation of the unramified coordinate of an Artin symbol as the normalized valuation (unramifiedCoordinate_artinMap). For the reverse inclusion, a class with unramified coordinate n ∈ ℤ differs from the Artin symbol of an element of valuation n by a class with trivial coordinate, that is, by the image of an element of inertia, and these are the Artin symbols of the units of 𝒪[K] (map_artinMap_unitFiltration_zero).

None of this needs local existence, so it holds for every nonarchimedean local field, in every characteristic.

Main results #

References #

source
theorem TauCeti.ClassFieldTheory.range_artinMap (K : Type) [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] :
(artinMap K).range = integralUnramifiedSubgroup K

The image of the absolute local Artin map consists exactly of the classes in G_K^ab whose unramified coordinate is an integer.

source
theorem TauCeti.ClassFieldTheory.mem_range_artinMap_iff (K : Type) [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] (y : Field.absoluteGaloisGroupAbelianization K) :
y ∈ (artinMap K).range ↔ ∃ (w : WeilGroup K), ↑((weilToAbsolute K) w) = y

The Artin symbols are the classes of the Weil group. A class in G_K^ab is the Artin symbol of an element of Kˣ exactly when it is the class of an element of the local Weil group W_K.

source
theorem TauCeti.ClassFieldTheory.not_surjective_artinMap (K : Type) [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] :
¬Function.Surjective ⇑(artinMap K)

The absolute local Artin map is not surjective: the unramified coordinate of an Artin symbol is an integer, while the unramified coordinate takes every value in ℤ̂ ≠ ℤ.

The Artin map into the abelianized Weil group #

source
noncomputable def TauCeti.ClassFieldTheory.weilArtinMap (K : Type) [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] :
Kˣ →* TopologicalAbelianization (WeilGroup K)

The local Artin map into the abelianized Weil group, Kˣ →* W_K^ab: the lift of the absolute local Artin map artinMap K along the injection W_K^ab → G_K^ab (weilToAbsoluteAbelianization_weilArtinMap), which exists because both maps have the same image (range_artinMap, range_weilToAbsoluteAbelianization). It is surjective (surjective_weilArtinMap), and in characteristic zero it is an isomorphism of topological groups (localWeilArtinEquiv).

Instances For
    source
    @[simp]
    theorem TauCeti.ClassFieldTheory.weilToAbsoluteAbelianization_weilArtinMap (K : Type) [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] (x : Kˣ) :
    (weilToAbsoluteAbelianization K) ((weilArtinMap K) x) = (artinMap K) x

    The image of weilArtinMap K x in G_K^ab is the Artin symbol of x. Since W_K^ab → G_K^ab is injective, this determines weilArtinMap K.

    source
    @[simp]
    theorem TauCeti.ClassFieldTheory.weilDegreeAbelianization_weilArtinMap (K : Type) [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] (x : Kˣ) :
    (weilDegreeAbelianization K) ((weilArtinMap K) x) = (normalizedValuation K) x

    The degree of weilArtinMap K x is the normalized valuation of x.

    source
    theorem TauCeti.ClassFieldTheory.continuous_weilArtinMap (K : Type) [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] :
    Continuous ⇑(weilArtinMap K)

    The local Artin map into the abelianized Weil group is continuous.

    source
    theorem TauCeti.ClassFieldTheory.surjective_weilArtinMap (K : Type) [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] :
    Function.Surjective ⇑(weilArtinMap K)

    Every class of the abelianized Weil group is an Artin symbol: the local Artin map Kˣ → W_K^ab is surjective.

    source
    theorem TauCeti.ClassFieldTheory.isOpenMap_weilArtinMap (K : Type) [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] :
    IsOpenMap ⇑(weilArtinMap K)

    The local Artin map into the abelianized Weil group is open. This is the open mapping theorem for the continuous surjection weilArtinMap K from the σ-compact group Kˣ onto the locally compact group W_K^ab.

    source
    theorem TauCeti.ClassFieldTheory.ker_weilArtinMap (K : Type) [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] :
    (weilArtinMap K).ker = (artinMap K).ker

    The local Artin map into the abelianized Weil group has the same kernel as the absolute local Artin map, namely the intersection of the norm subgroups (ker_artinMap_eq_iInf).