The unramified coordinate of the abelianized absolute Galois group

Let K be a nonarchimedean local field, G_K = Field.absoluteGaloisGroup K its absolute Galois group and G_K^{ab} = Field.absoluteGaloisGroupAbelianization K the topological abelianization. This file defines the unramified coordinate

TauCeti.unramifiedCoordinate K : G_K^{ab} →ₜ* ℤ̂,

the continuous homomorphism induced by restriction to the maximal unramified extension K^{ur} followed by the identification Gal(K^{ur}/K) ≃ₜ* ℤ̂ carrying arithmetic Frobenius to the canonical generator zHat.gen. Since ℤ̂ is commutative, restriction factors through the topological abelianization.

The coordinate is normalized arithmetically: the class of σ has coordinate zHat.gen exactly when σ is an arithmetic Frobenius lift, and more generally coordinate zHat.gen ^ n exactly when σ acts on K^{ur} as the n-th power of Frobenius, hence on every unramified extension K_f of finite degree as the n-th power of its arithmetic Frobenius. It is surjective, and its kernel is the image of the inertia subgroup. It is the coordinate in which the arithmetic normalization of local class field theory is expressed: the local Artin map sends x ∈ Kˣ to an element of unramified coordinate zHat.gen ^ v_K(x), for v_K the normalized valuation.

Main definition

• TauCeti.unramifiedCoordinate K: the continuous homomorphism G_K^{ab} →ₜ* ℤ̂.

Main results

• TauCeti.unramifiedCoordinate_mk: the coordinate of the class of σ is the image in ℤ̂ of the restriction of σ to K^{ur}.
• TauCeti.unramifiedCoordinate_mk_eq_gen_zpow_iff, TauCeti.unramifiedCoordinate_mk_eq_gen_iff: the class of σ has coordinate zHat.gen ^ n exactly when σ restricts to the n-th power of Frobenius on K^{ur}, and coordinate zHat.gen exactly when σ is an arithmetic Frobenius lift.
• TauCeti.unramifiedCoordinate_mk_eq_unramifiedCoordinate_mk_iff: two elements of G_K have the same coordinate exactly when they agree on every unramified extension K_f.
• TauCeti.apply_of_unramifiedCoordinate_mk_eq_gen_zpow: an element of coordinate zHat.gen ^ n acts on K_f as the n-th power of the arithmetic Frobenius of K_f / K.
• TauCeti.unramifiedCoordinate_mk_eq_one_iff, TauCeti.ker_unramifiedCoordinate: the kernel is the image of the inertia subgroup.
• TauCeti.unramifiedCoordinate_surjective: the coordinate is surjective.

References

• J.-P. Serre, Corps Locaux, Chapter XIII, §4.
• J. Neukirch, Algebraic Number Theory, Chapter V, §1.

noncomputable def TauCeti.unramifiedCoordinate (K : Type u) [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] : Field.absoluteGaloisGroupAbelianization K →ₜ* ↑zHat.toProfinite.toTop

The unramified coordinate G_K^{ab} →ₜ* ℤ̂ of a nonarchimedean local field K: restriction to the maximal unramified extension K^{ur}, followed by the identification Gal(K^{ur}/K) ≃ₜ* ℤ̂ sending arithmetic Frobenius to zHat.gen, factored through the topological abelianization of the absolute Galois group.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem TauCeti.unramifiedCoordinate_mk {K : Type u} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] (σ : Field.absoluteGaloisGroup K) : (unramifiedCoordinate K) ↑σ = (maximalUnramifiedGaloisGroupEquivZHat K (AlgebraicClosure K)) ((restrictMaximalUnramifiedHom K) σ)

The unramified coordinate of the class of σ is the image in ℤ̂ of the restriction of σ to the maximal unramified extension.

theorem TauCeti.unramifiedCoordinate_mk_eq_gen_zpow_iff {K : Type u} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] (σ : Field.absoluteGaloisGroup K) (n : ℤ) : (unramifiedCoordinate K) ↑σ = zHat.gen ^ n ↔ (restrictMaximalUnramifiedHom K) σ = maximalUnramifiedFrobenius K (AlgebraicClosure K) ^ n

Integral coordinates. The class of σ has unramified coordinate zHat.gen ^ n exactly when σ acts on the maximal unramified extension as the n-th power of its arithmetic Frobenius.

theorem TauCeti.unramifiedCoordinate_mk_eq_gen_iff {K : Type u} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] (σ : Field.absoluteGaloisGroup K) : (unramifiedCoordinate K) ↑σ = zHat.gen ↔ IsArithFrobeniusLift K σ

Arithmetic normalization. The class of σ has unramified coordinate zHat.gen exactly when σ is an arithmetic Frobenius lift.

theorem TauCeti.unramifiedCoordinate_mk_eq_unramifiedCoordinate_mk_iff {K : Type u} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] (σ τ : Field.absoluteGaloisGroup K) : (unramifiedCoordinate K) ↑σ = (unramifiedCoordinate K) ↑τ ↔ ∀ (f : ℕ), ∀ x ∈ unramifiedExtension K (AlgebraicClosure K) f, σ x = τ x

Two elements of the absolute Galois group have the same unramified coordinate exactly when they agree on the unramified extension K_f of every degree f.

theorem TauCeti.apply_of_unramifiedCoordinate_mk_eq_gen_zpow {K : Type u} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] {f : ℕ} [ValuativeRel ↥(unramifiedExtension K (AlgebraicClosure K) f)] [TopologicalSpace ↥(unramifiedExtension K (AlgebraicClosure K) f)] [IsNonarchimedeanLocalField ↥(unramifiedExtension K (AlgebraicClosure K) f)] [ValuativeExtension K ↥(unramifiedExtension K (AlgebraicClosure K) f)] [IsUnramified K ↥(unramifiedExtension K (AlgebraicClosure K) f)] {σ : Field.absoluteGaloisGroup K} {n : ℤ} (hσ : (unramifiedCoordinate K) ↑σ = zHat.gen ^ n) {x : AlgebraicClosure K} (hx : x ∈ unramifiedExtension K (AlgebraicClosure K) f) : σ x = ↑((frobeniusAlgEquiv ^ n) ⟨x, hx⟩)

The unramified coordinate at finite level. An element of the absolute Galois group whose class has unramified coordinate zHat.gen ^ n acts on the unramified extension K_f of any degree f as the n-th power of the arithmetic Frobenius of K_f / K.

theorem TauCeti.unramifiedCoordinate_mk_eq_one_iff {K : Type u} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] (σ : Field.absoluteGaloisGroup K) : (unramifiedCoordinate K) ↑σ = 1 ↔ σ ∈ inertiaSubgroup K

The class of σ has trivial unramified coordinate exactly when σ lies in the inertia subgroup.

theorem TauCeti.ker_unramifiedCoordinate (K : Type u) [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] : (unramifiedCoordinate K).ker = Subgroup.map (QuotientGroup.mk' (commutator (Field.absoluteGaloisGroup K)).topologicalClosure) (inertiaSubgroup K)

The kernel of the unramified coordinate is the image of the inertia subgroup in the topological abelianization.

theorem TauCeti.unramifiedCoordinate_surjective (K : Type u) [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] : Function.Surjective ⇑(unramifiedCoordinate K)

The unramified coordinate is surjective: every element of ℤ̂ is the coordinate of some element of the absolute Galois group.