Documentation

TauCeti.NumberTheory.ClassFieldTheory.Local.ArtinMap

The absolute local Artin map #

Let K be a nonarchimedean local field. The local class formation TauCeti.ClassFieldTheory.localClassFormation K lives on the formation of (Kˢ)ˣ over the absolute Galois group G_K = Gal(Kˢ/K). Its ground level is Kˣ. Its absolute Artin map ClassFormation.absoluteArtinMap is the inverse limit of the finite Artin maps. Reading it through these identifications gives the absolute local Artin map

artinMap K : Kˣ →* G_K^ab,

normalized, like the finite local Artin maps, by arithmetic Frobenius. Its target is Field.absoluteGaloisGroupAbelianization K, the topological abelianization of Mathlib's absolute Galois group Gal(AlgebraicClosure K/K), taken at the algebraic closure. The comparison between the two closures is TauCeti.absoluteGaloisGroupRestrictEquiv, restriction to the separable closure.

The finite restrictions of artinMap K are the finite local Artin maps (artinMap_restrict): if σ ∈ Gal(AlgebraicClosure K/K) represents the absolute Artin symbol of x ∈ Kˣ, then for every finite Galois extension L/K embedded in Kˢ by ι, the Artin symbol of x in Gal(L/K)^ab is the class of the restriction of σ to L. The image of artinMap K is dense (denseRange_artinMap), but it is not all of G_K^ab, so no statement about G_K^ab follows from one about the image alone.

The norm subgroups of Kˣ are the preimages of the open subgroups of G_K^ab: every open subgroup of G_K^ab is cut out by some finite Galois extension L/K, and its preimage under artinMap K is the norm group N_{L/K}(Lˣ) (exists_artinMap_mem_iff), the kernel of the finite local Artin map. Conversely every norm subgroup is such a preimage (exists_openSubgroup_artinMap_mem_iff). Since norm groups of finite separable extensions are open, artinMap K is continuous (continuous_artinMap), and its kernel is the intersection of all norm subgroups (ker_artinMap_eq_iInf).

The absolute Artin map is functorial for the norm (artinMap_norm). For a finite extension L/K embedded in Kˢ by iota, TauCeti.absoluteGaloisGroupExtend K L iota embeds G_L in G_K as Gal(Kˢ/iota(L)), and it carries the Artin symbol of x ∈ Lˣ to that of N_{L/K} x. The proof compares the two local class formations on corresponding layers (TauCeti.ClassFieldTheory.artinMap_localFormationLayerEquiv) and then uses the Artin–Tate diagram for the norm inside the formation of K (TauCeti.ClassFieldTheory.ClassFormation.artinMap_groundNorm). On ground levels, that norm is the field norm N_{L/K} (TauCeti.ClassFieldTheory.groundNorm_layerRestriction_localFormationMap).

The absolute Artin map is natural in the local field (artinMap_congr). A continuous isomorphism e : K ≃+* K', extended to the algebraic closures by e', carries Art_K(x) to Art_{K'}(e x). Conjugation by e' is determined only up to an inner automorphism of G_{K'}, which is invisible in G_{K'}^ab. This transports Artin symbols across identifications of local fields, for instance from a completion of a number field to a concrete model such as ℚ_[p].

Main definitions #

Main results #

References #

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

The absolute local Artin map Kˣ →* G_K^ab of a nonarchimedean local field K, into the topological abelianization of the absolute Galois group Gal(AlgebraicClosure K/K). It is the map ClassFormation.fieldArtinMap of the local class formation, that is, its absolute Artin map (artinMap_apply), the inverse limit of the finite local Artin maps (artinMap_restrict). It has dense image (denseRange_artinMap).

Instances For
    source
    theorem TauCeti.ClassFieldTheory.artinMap_apply (K : Type) [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] (x : Kˣ) :
    (artinMap K) x = (absoluteGaloisGroupRestrictEquiv K).symm.topologicalAbelianizationCongr (Additive.toMul ((localClassFormation K).absoluteArtinMap ((unitsLevelEquiv (Algebra.ofId K (SeparableClosure K)) ⋯) (Additive.ofMul x))))

    The absolute local Artin map is the absolute Artin map of the local class formation: 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.

    source
    theorem TauCeti.ClassFieldTheory.artinMap_restrict (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) (x : Kˣ) (σ : Field.absoluteGaloisGroup K) (hσ : ↑σ = (artinMap K) x) :
    (localArtinMap K L ι) (Additive.ofMul x) = Additive.ofMul (Abelianization.of (ι.restrictNormalHom ((absoluteGaloisGroupRestrictEquiv K) σ)))

    The finite restrictions of the absolute local Artin map are the finite local Artin maps. If σ ∈ Gal(AlgebraicClosure K/K) represents the absolute Artin symbol of x ∈ Kˣ, then for every finite Galois extension L/K embedded in the separable closure by ι, the Artin symbol of x in Gal(L/K)^ab is the class of the restriction of σ to L.

    source
    theorem TauCeti.ClassFieldTheory.mem_normGroup_of_mk_eq_artinMap_of_fixes (K : Type) [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] {x : Kˣ} (σ : Field.absoluteGaloisGroup K) (hσ : ↑σ = (artinMap K) x) (M : IntermediateField K (AlgebraicClosure K)) [FiniteDimensional K ↥M] [IsGalois K ↥M] (hσM : ∀ (z : ↥M), σ ↑z = ↑z) :
    x ∈ normGroup K ↥M

    An Artin symbol that fixes a finite Galois extension comes from a norm. If σ ∈ Gal(AlgebraicClosure K/K) represents the absolute Artin symbol of x ∈ Kˣ and fixes pointwise a finite Galois extension M of K inside the algebraic closure, then x is a norm from M. This is artinMap_restrict combined with the kernel of the finite local Artin map (localArtinMap_eq_zero_iff).

    source
    theorem TauCeti.ClassFieldTheory.mem_normGroup_fixedField_iff {K : Type} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] {M : Type u_1} [Field M] [Algebra K M] [FiniteDimensional K M] [IsAbelianGalois K M] (H : Subgroup Gal(M/K)) {u : Kˣ} {σ : Gal(M/K)} (hσ : Abelianization.of σ = (normResidue K M) ↑u) :
    u ∈ normGroup K ↥(IntermediateField.fixedField H) ↔ σ ∈ H

    Norms from a subextension of an abelian extension. Let M/K be a finite abelian extension and H a subgroup of Gal(M/K). If σ ∈ Gal(M/K) is the norm residue symbol of u ∈ Kˣ, then u is a norm from the fixed field of H exactly when σ ∈ H.

    source
    theorem TauCeti.ClassFieldTheory.denseRange_artinMap (K : Type) [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] :
    DenseRange ⇑(artinMap K)

    The absolute local Artin map has dense image: it reaches every finite quotient of G_K^ab, because every finite local Artin map is surjective.

    source
    theorem TauCeti.ClassFieldTheory.exists_artinMap_mem_iff (K : Type) [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] (U : OpenSubgroup (Field.absoluteGaloisGroupAbelianization K)) :
    ∃ (V : OpenNormalSubgroup (AbsoluteGaloisGroup K)), ∀ (x : Kˣ), (artinMap K) x ∈ U ↔ x ∈ localNormSubgroup K V

    The preimage of an open subgroup under the absolute local Artin map is a norm subgroup. For every open subgroup U of G_K^ab there is an open normal subgroup V of G_K, cutting out the finite Galois extension classField K V, such that the Artin symbol of x ∈ Kˣ lies in U exactly when x is a norm from classField K V.

    source
    theorem TauCeti.ClassFieldTheory.exists_openSubgroup_artinMap_mem_iff (K : Type) [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] (V : OpenNormalSubgroup (AbsoluteGaloisGroup K)) :
    ∃ (U : OpenSubgroup (Field.absoluteGaloisGroupAbelianization K)), ∀ (x : Kˣ), (artinMap K) x ∈ U ↔ x ∈ localNormSubgroup K V

    Every local norm subgroup is the preimage of an open subgroup under the absolute local Artin map. For every open normal subgroup V of G_K there is an open subgroup U of G_K^ab, the kernel of the projection G_K^ab → Gal(classField K V/K)^ab, such that the Artin symbol of x ∈ Kˣ lies in U exactly when x is a norm from classField K V. This is the converse of exists_artinMap_mem_iff.

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

    The absolute local Artin map is continuous. The preimage of an open subgroup of G_K^ab is a norm subgroup (exists_artinMap_mem_iff), and norm subgroups of finite separable extensions are open in Kˣ.

    source
    theorem TauCeti.ClassFieldTheory.ker_artinMap_eq_iInf (K : Type) [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] :
    (artinMap K).ker = ⨅ (V : OpenNormalSubgroup (AbsoluteGaloisGroup K)), localNormSubgroup K V

    The kernel of the absolute local Artin map is the intersection of all norm subgroups: the Artin symbol of x ∈ Kˣ is trivial exactly when x is a norm from every finite Galois extension of K. This says nothing about whether that intersection is trivial.

    Norm functoriality #

    source
    theorem TauCeti.ClassFieldTheory.artinMap_norm {K : Type} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] (L : Type) [Field L] [Algebra K L] [FiniteDimensional K L] (iota : L →ₐ[K] SeparableClosure K) [ValuativeRel L] [TopologicalSpace L] [IsNonarchimedeanLocalField L] [ValuativeExtension K L] (x : Lˣ) (τ : Field.absoluteGaloisGroup L) (hτ : ↑τ = (artinMap L) x) :
    ↑((absoluteGaloisGroupExtend K L iota) τ) = (artinMap K) ((Algebra.normUnits K) x)

    Norm functoriality of the absolute local Artin map. Let L/K be a finite extension of nonarchimedean local fields, embedded in Kˢ by iota. If τ ∈ Gal(AlgebraicClosure L/L) represents the absolute Artin symbol of x ∈ Lˣ, then its image under the embedding absoluteGaloisGroupExtend K L iota : G_L → G_K represents the absolute Artin symbol of the norm N_{L/K} x: in G_K^ab,

    Art_K (N_{L/K} x) = absoluteGaloisGroupExtend K L iota (Art_L x).

    Naturality in the local field #

    source
    theorem TauCeti.ClassFieldTheory.artinMap_congr {K : Type} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] {K' : Type} [Field K'] [ValuativeRel K'] [TopologicalSpace K'] [IsNonarchimedeanLocalField K'] (e : K ≃+* K') (he : Continuous ⇑e) (e' : AlgebraicClosure K ≃+* AlgebraicClosure K') (he' : ∀ (c : K), e' ((algebraMap K (AlgebraicClosure K)) c) = (algebraMap K' (AlgebraicClosure K')) (e c)) (x : Kˣ) (σ : Field.absoluteGaloisGroup K) (σ' : Field.absoluteGaloisGroup K') (hσσ' : ∀ (y : AlgebraicClosure K), e' (σ.toRingEquiv y) = σ'.toRingEquiv (e' y)) (hσ : ↑σ = (artinMap K) x) :
    ↑σ' = (artinMap K') ((Units.map e.toMonoidHom) x)

    The absolute local Artin map is natural in the local field. Let e : K ≃+* K' be a continuous isomorphism of nonarchimedean local fields and e' an extension of e to the algebraic closures. If σ ∈ G_K represents the absolute Artin symbol of x ∈ Kˣ, then its conjugate σ' = e' ∘ σ ∘ e'⁻¹ ∈ G_{K'} represents the absolute Artin symbol of e x:

    Art_{K'} (e x) = e' ∘ Art_K (x) ∘ e'⁻¹.

    Two extensions of e differ by an element of G_{K'}, and conjugation by it is invisible in G_{K'}^ab, so every extension e' is allowed. Continuity of e is what makes it compatible with the valuations of K and K'.