The Galois group of the maximal unramified extension

For a nonarchimedean local field K and a separably closed extension Ω, this file identifies the Galois group of the maximal unramified extension with the profinite integers:

Gal(Kᵘʳ/K) ≃ₜ* ℤ̂.

The isomorphism sends arithmetic Frobenius to the canonical generator zHat.gen, and hence each integral power of zHat.gen to the same power of Frobenius; in particular arithmetic Frobenius has infinite order (TauCeti.not_isOfFinOrder_maximalUnramifiedFrobenius), and Gal(Kᵘʳ/K) is commutative.

Main definition

• TauCeti.maximalUnramifiedGaloisGroupEquivZHat: the continuous multiplicative equivalence Gal(Kᵘʳ/K) ≃ₜ* ℤ̂, carrying arithmetic Frobenius to zHat.gen.

References

• J.-P. Serre, Corps Locaux, Chapter III, §5.
• J. Neukirch, Algebraic Number Theory, Chapter II, §7.

noncomputable def TauCeti.maximalUnramifiedGaloisGroupEquivZHat (K : Type u) [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] (Ω : Type v) [Field Ω] [Algebra K Ω] [IsSepClosed Ω] : Gal(↥(maximalUnramifiedExtension K Ω)/K) ≃ₜ* ↑zHat.toProfinite.toTop

The Galois group of the maximal unramified extension is the profinite integers. This continuous multiplicative equivalence sends arithmetic Frobenius to zHat.gen.

Equations

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

@[simp]

theorem TauCeti.maximalUnramifiedGaloisGroupEquivZHat_symm_apply_gen (K : Type u) [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] (Ω : Type v) [Field Ω] [Algebra K Ω] [IsSepClosed Ω] : (maximalUnramifiedGaloisGroupEquivZHat K Ω).symm zHat.gen = maximalUnramifiedFrobenius K Ω

The inverse isomorphism sends the canonical generator of ℤ̂ to arithmetic Frobenius.

@[simp]

theorem TauCeti.maximalUnramifiedGaloisGroupEquivZHat_apply_frobenius (K : Type u) [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] (Ω : Type v) [Field Ω] [Algebra K Ω] [IsSepClosed Ω] : (maximalUnramifiedGaloisGroupEquivZHat K Ω) (maximalUnramifiedFrobenius K Ω) = zHat.gen

The isomorphism sends arithmetic Frobenius to the canonical generator of ℤ̂.

theorem TauCeti.maximalUnramifiedGaloisGroupEquivZHat_symm_apply_ofInt (K : Type u) [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] (Ω : Type v) [Field Ω] [Algebra K Ω] [IsSepClosed Ω] (n : ℤ) : (maximalUnramifiedGaloisGroupEquivZHat K Ω).symm (zHat.ofInt (Multiplicative.ofAdd n)) = maximalUnramifiedFrobenius K Ω ^ n

Integral powers of the canonical generator correspond to the same powers of arithmetic Frobenius.

instance TauCeti.instIsMulCommutativeAlgEquivSubtypeMemIntermediateFieldMaximalUnramifiedExtension (K : Type u) [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] (Ω : Type v) [Field Ω] [Algebra K Ω] [IsSepClosed Ω] : IsMulCommutative Gal(↥(maximalUnramifiedExtension K Ω)/K)

The Galois group of the maximal unramified extension is commutative, being isomorphic to ℤ̂.

theorem TauCeti.not_isOfFinOrder_maximalUnramifiedFrobenius (K : Type u) [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] (Ω : Type v) [Field Ω] [Algebra K Ω] [IsSepClosed Ω] : ¬IsOfFinOrder (maximalUnramifiedFrobenius K Ω)

Arithmetic Frobenius has infinite order in Gal(Kᵘʳ/K), since ℤ embeds into ℤ̂.