NYLL

theorem · Research papers

Mixed-characteristic discrete valuations

Conjugation on the mod-p abelianized absolute Galois group detects every element of a finite Galois group.

The field need only carry a discrete valuation of mixed characteristic $(0,p)$; completeness and Henselianity are unnecessary. Detection through a single prime thus applies beyond ordinary local fields. Yamaguchi's Theorem 3.6 proves this using Kummer theory and a reduction to prime-degree extensions, providing an input to the higher-local-field theorem and later applications to solvable Galois quotients.

YamaguchiPapersFormalization on GitHub ↗

Mathematical statement

Let $K$ have characteristic $0$ and a discrete valuation with residue characteristic $p>0$. For every finite Galois extension $L/K$,

$$\operatorname{Gal}(L/K)\longrightarrow\operatorname{Aut}(G_L^{\mathrm{ab}}/p)$$

is injective. In addition, $G_K$ is $p$-ab-faithful. Neither completeness nor Henselianity of the given valuation is assumed in this declaration.

Lean code

Yamaguchi26AbfaithfulGalois.mixed_characteristic_properties_3_6

Published library source ↗Same source in NYLL ↗

theorem mixed_characteristic_properties_3_6
    (K : Type u) [Field K] [CharZero K]
    (base : DVF.{u, v} K) (p : ℕ) [Fact p.Prime]
    [CharP base.residueField p] :
    (∀ (L : Type u) [Field L] [Algebra K L]
      [FiniteDimensional K L] [IsGalois K L],
      ∀ τ : Gal(L/K),
        (∀ z : abelianModPower Gal(AlgebraicClosure L/L) p,
          relativeGaloisAbelianModPowerTransform K L p τ z = z) → τ = 1) ∧
      IsSigmaAbFaithful {p} Gal(AlgebraicClosure K/K)
In-scope Lean context
namespace Yamaguchi26AbfaithfulGalois

open KummerTheory ValuationTheory.DiscreteValuationField ProCGroups.Abelian

open ProCGroups.FiniteStepSolvableQuotients

universe u v
Full declaration and proof
/-- For each finite Galois extension of a mixed-characteristic discretely
valued field, the conjugation action on the mod-`p` abelianization is
faithful. Consequently its absolute Galois group is `p`-ab-faithful. -/
theorem mixed_characteristic_properties_3_6
    (K : Type u) [Field K] [CharZero K]
    (base : DVF.{u, v} K) (p : ℕ) [Fact p.Prime]
    [CharP base.residueField p] :
    (∀ (L : Type u) [Field L] [Algebra K L]
      [FiniteDimensional K L] [IsGalois K L],
      ∀ τ : Gal(L/K),
        (∀ z : abelianModPower Gal(AlgebraicClosure L/L) p,
          relativeGaloisAbelianModPowerTransform K L p τ z = z) → τ = 1) ∧
      IsSigmaAbFaithful {p} Gal(AlgebraicClosure K/K) := by
  have hdetect : ∀ (F E : Type u) [Field F] [Field E] [Algebra F E]
      [IsGalois F E] [CharZero F]
      (source : DVF.{u,v} F) [CharP source.residueField p]
      (r : ℕ) [Fact r.Prime], Module.finrank F E = r →
        ∃ τ : Gal(E/F), τ ≠ 1 ∧
          ∃ z : abelianModPower Gal(AlgebraicClosure E/E) p,
            relativeGaloisAbelianModPowerTransform F E p τ z ≠ z := by
    intro F E _ _ _ _ _ source _ r _ hdegree
    exact prime_order_detection_of_mixedChar source p r hdegree
  constructor
  · intro L _ _ _ _
    exact relativeGaloisAbelianModPowerTransform_faithful_of_primeDegree_detection
      p hdetect base L
  · exact isSigmaAbFaithful_of_primeDegree_detection p hdetect base
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

  1. 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