The Artin map of a class formation on the units of a field

Let F be a class formation on the formation unitsFormation K of (Kˢ)ˣ over the absolute Galois group G_K = Gal(Kˢ/K) of a field K. Its ground level is Kˣ, and its absolute Artin map ClassFormation.absoluteArtinMap lands in Gal(Kˢ/K)^ab. Reading it through these identifications gives the Artin map of F on Kˣ

F.fieldArtinMap : Kˣ →* G_K^ab,

into Field.absoluteGaloisGroupAbelianization K, the topological abelianization of Mathlib's absolute Galois group Gal(AlgebraicClosure K/K). The comparison between the two closures is TauCeti.absoluteGaloisGroupRestrictEquiv, restriction to the separable closure.

This is the common construction behind the nonarchimedean local Artin map TauCeti.ClassFieldTheory.artinMap and the archimedean Artin maps TauCeti.ClassFieldTheory.infiniteArtinAt; it uses no property of K or of F.

Main definitions

• TauCeti.ClassFieldTheory.ClassFormation.fieldArtinMap: the Artin map Kˣ →* G_K^ab of a class formation on unitsFormation K.

Main results

• TauCeti.ClassFieldTheory.ClassFormation.fieldArtinMap_apply: F.fieldArtinMap is the absolute Artin map of F, read on Kˣ and in Gal(AlgebraicClosure K/K)^ab.
• TauCeti.ClassFieldTheory.ClassFormation.absoluteArtinMap_eq_of_mk_eq_fieldArtinMap: a representative of F.fieldArtinMap x restricts to a representative of the absolute Artin symbol of x.

noncomputable def TauCeti.ClassFieldTheory.ClassFormation.fieldArtinMap {K : Type} [Field K] (F : ClassFormation (unitsFormation K)) : Kˣ →* Field.absoluteGaloisGroupAbelianization K

The Artin map Kˣ →* G_K^ab of a class formation F on unitsFormation K: the absolute Artin map of F (fieldArtinMap_apply), read on Kˣ through the identification of the ground level, and in the topological abelianization of Mathlib's absolute Galois group Gal(AlgebraicClosure K/K).

theorem TauCeti.ClassFieldTheory.ClassFormation.fieldArtinMap_apply {K : Type} [Field K] (F : ClassFormation (unitsFormation K)) (x : Kˣ) : F.fieldArtinMap x = (absoluteGaloisGroupRestrictEquiv K).symm.topologicalAbelianizationCongr (Additive.toMul (F.absoluteArtinMap ((unitsLevelEquiv (Algebra.ofId K (SeparableClosure K)) ⋯) (Additive.ofMul x))))

F.fieldArtinMap is the absolute Artin map of F: the absolute Artin symbol of x ∈ Kˣ, regarded as an element of the ground level ((Kˢ)ˣ)^{G_K}, carried from Gal(Kˢ/K)^ab to Gal(AlgebraicClosure K/K)^ab.

theorem TauCeti.ClassFieldTheory.ClassFormation.absoluteArtinMap_eq_of_mk_eq_fieldArtinMap {K : Type} [Field K] (F : ClassFormation (unitsFormation K)) (x : Kˣ) (σ : Field.absoluteGaloisGroup K) (hσ : ↑σ = F.fieldArtinMap x) : F.absoluteArtinMap ((unitsLevelEquiv (Algebra.ofId K (SeparableClosure K)) ⋯) (Additive.ofMul x)) = Additive.ofMul ↑((absoluteGaloisGroupRestrictEquiv K) σ)

If σ ∈ Gal(AlgebraicClosure K/K) represents F.fieldArtinMap x, then the absolute Artin symbol of x for F is the class of the restriction of σ to the separable closure.