theorem · Research papers

Higher local fields

Every positive-dimensional higher local field has an ab-faithful absolute Galois group.

Higher local fields are built through successive complete discrete valuations ending in a finite residue field. The uniform conclusion over finite extensions is useful for studying solvable quotients, where conjugation must remain controlled after passing to open subgroups. Yamaguchi's Theorem 4.2 follows the residue-field towers, combining mixed-characteristic detection with lifting from characteristic-zero residue fields.

YamaguchiPapersFormalization on GitHub ↗

Mathematical statement

An $n$-dimensional higher local field is defined recursively: dimension $0$ means a finite field, and dimension $n+1$ means a field with a complete discrete valuation whose residue field is $n$-dimensional. The theorem states

$$n>0,\quad K\text{ an }n\text{-dimensional higher local field}\quad\Longrightarrow\quad G_K\text{ is ab-faithful}.$$

Lean code

`Yamaguchi26AbfaithfulGalois.higher_local_field_abFaithful_4_2`

Published library source ↗Same source in NYLL ↗

theorem higher_local_field_abFaithful_4_2
    (n : ℕ) (K : Type u) [Field K]
    (hK : ValuationTheory.IsHigherLocalField.{u, v} n K) (hn : 0 < n) :
    IsAbFaithful Gal(AlgebraicClosure K/K)

In-scope Lean context

namespace Yamaguchi26AbfaithfulGalois

open ProCGroups.FiniteStepSolvableQuotients

universe u v

Full declaration and proof

theorem higher_local_field_abFaithful_4_2
    (n : ℕ) (K : Type u) [Field K]
    (hK : ValuationTheory.IsHigherLocalField.{u, v} n K) (hn : 0 < n) :
    IsAbFaithful Gal(AlgebraicClosure K/K) :=
  (higher_local_field_roots_and_abFaithful n K hK).2 hn

Source credits and license

Copyright (c) 2026 Naganori Yamaguchi (https://github.com/n-yamaguchi-0729). All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Naganori Yamaguchi (assisted by OpenAI Codex)

References

Naganori Yamaguchi. Ab-faithfulness of absolute Galois groups in number theory. 2026. arXiv:2610.05634v1, submitted October 4, 2026.

Published source: a1a5a03f.

← All selected results in Research papers