Injectivity of the absolute local Artin map and the profinite completion of Kˣ

Let K be a nonarchimedean local field of characteristic zero, for instance a finite extension of ℚ_p. Local existence (localExistence) makes every subgroup of finite index of Kˣ a norm subgroup, and this file draws its two consequences for the absolute local Artin map artinMap K : Kˣ →* G_K^ab.

• The profinite completion. Since G_K^ab is profinite, artinMap K extends uniquely to a continuous homomorphism profiniteCompletionArtinMap K on the profinite completion (Kˣ)^. It is surjective for every local field, as artinMap K has dense image. In characteristic zero it is injective: a subgroup H of finite index is a norm subgroup, hence the preimage of an open subgroup U of G_K^ab (exists_openSubgroup_artinMap_mem_iff), and the H-coordinate of an element of (Kˣ)^ is read off its image in G_K^ab ⧸ U. So it is an isomorphism of topological groups profiniteCompletionArtinEquiv K : (Kˣ)^ ≃ₜ* G_K^ab.
• Injectivity (injective_artinMap). Since Kˣ is residually finite (TauCeti.residuallyFinite_units), it embeds in (Kˣ)^, so artinMap K is injective as the restriction of the injective profiniteCompletionArtinMap K; so is its geometric normalization (injective_geometricArtinMap).

Neither statement is claimed in characteristic p: existence is only proved there for subgroups of index prime to p, all of which contain the pro-p group of principal units.

Main definitions

• TauCeti.ClassFieldTheory.profiniteCompletionArtinMap: the continuous extension of the absolute local Artin map to the profinite completion of Kˣ.
• TauCeti.ClassFieldTheory.profiniteCompletionArtinEquiv: in characteristic zero, the resulting isomorphism of topological groups (Kˣ)^ ≃ₜ* G_K^ab.

Main results

• TauCeti.ClassFieldTheory.injective_artinMap: in characteristic zero the absolute local Artin map is injective.
• TauCeti.ClassFieldTheory.injective_geometricArtinMap: in characteristic zero the geometric local Artin map is injective.
• TauCeti.ClassFieldTheory.surjective_profiniteCompletionArtinMap and TauCeti.ClassFieldTheory.injective_profiniteCompletionArtinMap: the extension to the profinite completion is surjective, and in characteristic zero injective.

References

• J.-P. Serre, Local class field theory, in J. W. S. Cassels and A. Fröhlich (eds.), Algebraic Number Theory, Chapter VI, §2.
• J. Neukirch, Algebraic Number Theory, Chapter V, §1.

The profinite completion of Kˣ

noncomputable def TauCeti.ClassFieldTheory.profiniteCompletionArtinMap (K : Type) [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] : ↑(ProfiniteGrp.ProfiniteCompletion.completion ↧Kˣ).toProfinite.toTop →ₜ* Field.absoluteGaloisGroupAbelianization K

The absolute local Artin map on the profinite completion of Kˣ: the unique continuous extension of artinMap K to (Kˣ)^, which exists because G_K^ab is profinite. In characteristic zero it is an isomorphism (profiniteCompletionArtinEquiv).

@[simp]

theorem TauCeti.ClassFieldTheory.profiniteCompletionArtinMap_etaFn (K : Type) [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] (x : Kˣ) : (profiniteCompletionArtinMap K) (ProfiniteGrp.ProfiniteCompletion.etaFn (↧Kˣ) x) = (artinMap K) x

On the image of Kˣ in its profinite completion, profiniteCompletionArtinMap K is the absolute local Artin map.

theorem TauCeti.ClassFieldTheory.surjective_profiniteCompletionArtinMap (K : Type) [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] : Function.Surjective ⇑(profiniteCompletionArtinMap K)

The extension of the absolute local Artin map to the profinite completion of Kˣ is surjective: its image is compact, hence closed, and contains the dense image of artinMap K.

theorem TauCeti.ClassFieldTheory.injective_profiniteCompletionArtinMap (K : Type) [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] [CharZero K] : Function.Injective ⇑(profiniteCompletionArtinMap K)

In characteristic zero the extension of the absolute local Artin map to the profinite completion of Kˣ is injective: every subgroup of finite index of Kˣ is a norm subgroup (localExistence), hence the preimage of an open subgroup of G_K^ab (exists_openSubgroup_artinMap_mem_iff).

theorem TauCeti.ClassFieldTheory.injective_artinMap (K : Type) [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] [CharZero K] : Function.Injective ⇑(artinMap K)

The absolute local Artin map is injective in characteristic zero, in particular for a finite extension of ℚ_p: it is the composite of the injective extension profiniteCompletionArtinMap K with the map of Kˣ into its profinite completion, which is injective because Kˣ is residually finite.

theorem TauCeti.ClassFieldTheory.injective_geometricArtinMap (K : Type) [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] [CharZero K] : Function.Injective ⇑(geometricArtinMap K)

The geometric local Artin map is injective in characteristic zero, in particular for a finite extension of ℚ_p.

noncomputable def TauCeti.ClassFieldTheory.profiniteCompletionArtinEquiv (K : Type) [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] [CharZero K] : ↑(ProfiniteGrp.ProfiniteCompletion.completion ↧Kˣ).toProfinite.toTop ≃ₜ* Field.absoluteGaloisGroupAbelianization K

The profinite completion of Kˣ is G_K^ab. In characteristic zero, in particular for a finite extension of ℚ_p, the absolute local Artin map extends to an isomorphism of topological groups from the profinite completion of Kˣ onto G_K^ab (profiniteCompletionArtinEquiv_apply).

@[simp]

theorem TauCeti.ClassFieldTheory.profiniteCompletionArtinEquiv_apply (K : Type) [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] [CharZero K] (c : ↑(ProfiniteGrp.ProfiniteCompletion.completion ↧Kˣ).toProfinite.toTop) : (profiniteCompletionArtinEquiv K) c = (profiniteCompletionArtinMap K) c

The isomorphism (Kˣ)^ ≃ G_K^ab is the extension of the absolute local Artin map.