The geometric normalization of the absolute local Artin map

The absolute local Artin map artinMap K : Kˣ →* G_K^ab of a nonarchimedean local field K is normalized by arithmetic Frobenius: a uniformizer maps to the class of an arithmetic Frobenius lift (isArithFrobeniusLift_of_mk_eq_artinMap_uniformizer). Part of the literature, following Deligne, uses the opposite normalization, in which a uniformizer maps to a geometric Frobenius, the inverse of an arithmetic one. This file defines that map,

geometricArtinMap K : Kˣ →* G_K^ab,    geometricArtinMap K x = (artinMap K x)⁻¹,

as the arithmetic map followed by inversion in the commutative group G_K^ab, so that both normalizations are the same reciprocity map and no second one is constructed. Its properties are those of artinMap K read through inversion.

• It is continuous (continuous_geometricArtinMap), has the same image as artinMap K (range_geometricArtinMap), hence dense image (denseRange_geometricArtinMap), and the same kernel (ker_geometricArtinMap).
• Its unramified coordinate is the inverse, in the multiplicatively written ℤ̂, of the normalized valuation (unramifiedCoordinate_geometricArtinMap). So every lift of the geometric Artin symbol of a uniformizer is the inverse of an arithmetic Frobenius lift (isArithFrobeniusLift_inv_of_mk_eq_geometricArtinMap_uniformizer), and every lift of the geometric Artin symbol of a unit lies in inertia (mem_inertiaSubgroup_of_mk_eq_geometricArtinMap).
• Its finite restrictions are the inverses of the finite local Artin maps (geometricArtinMap_restrict), it is functorial for the norm of a finite extension (geometricArtinMap_norm), and it is natural in the local field (geometricArtinMap_congr).

Main definitions

• TauCeti.ClassFieldTheory.geometricArtinMap K: the absolute local Artin map normalized by geometric Frobenius.

References

• J. Tate, Number theoretic background, in Automorphic forms, representations and L-functions, Proc. Sympos. Pure Math. 33, Part 2 (1979), §1, for the two normalizations of the reciprocity map.
• P. Deligne, Les constantes des équations fonctionnelles des fonctions L, in Modular functions of one variable II, Lecture Notes in Math. 349 (1973), §2.

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

The geometric local Artin map Kˣ →* G_K^ab of a nonarchimedean local field K: the absolute local Artin map artinMap K followed by inversion in G_K^ab. It sends a uniformizer to the class of a geometric Frobenius, the inverse of an arithmetic Frobenius lift (isArithFrobeniusLift_inv_of_mk_eq_geometricArtinMap_uniformizer).

@[simp]

theorem TauCeti.ClassFieldTheory.geometricArtinMap_apply (K : Type) [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] (x : Kˣ) : (geometricArtinMap K) x = ((artinMap K) x)⁻¹

theorem TauCeti.ClassFieldTheory.continuous_geometricArtinMap (K : Type) [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] : Continuous ⇑(geometricArtinMap K)

The geometric local Artin map is continuous.

theorem TauCeti.ClassFieldTheory.range_geometricArtinMap (K : Type) [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] : (geometricArtinMap K).range = (artinMap K).range

The geometric and arithmetic local Artin maps have the same image.

theorem TauCeti.ClassFieldTheory.denseRange_geometricArtinMap (K : Type) [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] : DenseRange ⇑(geometricArtinMap K)

The geometric local Artin map has dense image.

theorem TauCeti.ClassFieldTheory.ker_geometricArtinMap (K : Type) [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] : (geometricArtinMap K).ker = (artinMap K).ker

The geometric and arithmetic local Artin maps have the same kernel, the intersection of the norm subgroups (ker_artinMap_eq_iInf).

The geometric Frobenius normalization

theorem TauCeti.ClassFieldTheory.unramifiedCoordinate_geometricArtinMap (K : Type) [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] (x : Kˣ) : (unramifiedCoordinate K) ((geometricArtinMap K) x) = (zHat.ofInt ((normalizedValuation K) x))⁻¹

The unramified coordinate of the geometric local Artin map is inverse normalized valuation: the coordinate of the geometric Artin symbol of x is the inverse of the image of v_K(x) in the multiplicatively written profinite integers.

theorem TauCeti.ClassFieldTheory.mem_inertiaSubgroup_of_mk_eq_geometricArtinMap (K : Type) [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] (u : Kˣ) (hu : (ValuativeRel.valuation K) ↑u = 1) (σ : Field.absoluteGaloisGroup K) (hσ : ↑σ = (geometricArtinMap K) u) : σ ∈ inertiaSubgroup K

Every lift of the geometric Artin symbol of a valuation-zero unit lies in inertia.

theorem TauCeti.ClassFieldTheory.isArithFrobeniusLift_inv_of_mk_eq_geometricArtinMap_uniformizer (K : Type) [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] {π : Kˣ} (hπ : IsUniformizer K π) (σ : Field.absoluteGaloisGroup K) (hσ : ↑σ = (geometricArtinMap K) π) : IsArithFrobeniusLift K σ⁻¹

Geometric Frobenius normalization. Every lift of the geometric Artin symbol of a uniformizer is a geometric Frobenius: its inverse is an arithmetic Frobenius lift.

Finite restrictions, norm functoriality and naturality

theorem TauCeti.ClassFieldTheory.geometricArtinMap_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σ : ↑σ = (geometricArtinMap K) x) : (localArtinMap K L ι) (Additive.ofMul x) = -Additive.ofMul (Abelianization.of (ι.restrictNormalHom ((absoluteGaloisGroupRestrictEquiv K) σ)))

The finite restrictions of the geometric local Artin map are the inverses of the finite local Artin maps. If σ ∈ Gal(AlgebraicClosure K/K) represents the geometric 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 inverse of the class of the restriction of σ to L.

theorem TauCeti.ClassFieldTheory.geometricArtinMap_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τ : ↑τ = (geometricArtinMap L) x) : ↑((absoluteGaloisGroupExtend K L iota) τ) = (geometricArtinMap K) ((Algebra.normUnits K) x)

Norm functoriality of the geometric 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 geometric Artin symbol of x ∈ Lˣ, then its image under absoluteGaloisGroupExtend K L iota : G_L → G_K represents the geometric Artin symbol of N_{L/K} x.

theorem TauCeti.ClassFieldTheory.geometricArtinMap_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σ : ↑σ = (geometricArtinMap K) x) : ↑σ' = (geometricArtinMap K') ((Units.map e.toMonoidHom) x)

The geometric 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 geometric Artin symbol of x ∈ Kˣ, then its conjugate σ' = e' ∘ σ ∘ e'⁻¹ ∈ G_{K'} represents the geometric Artin symbol of e x.