definition · Research papers

Ab-faithfulness

Finite relative quotients must be detectable by their action on abelianized open normal subgroups.

For absolute Galois groups, the condition tests relative automorphisms through the abelian Galois theory of finite extensions. Information from many extensions can therefore retain structure lost by abelianizing the original group alone. Yamaguchi's 2026 paper introduces the prime-restricted form in Definition 1.1 and uses valuation theory and embedding problems to establish the property and connect it with center-freeness and slimness.

YamaguchiPapersFormalization on GitHub ↗

Mathematical statement

A profinite group $G$ is ab-faithful if, for every open subgroup $H\le G$ and every open normal subgroup $N\triangleleft H$, the conjugation action gives an injection

$$H/N\hookrightarrow\operatorname{Aut}(N^{\mathrm{ab}}),\qquad N^{\mathrm{ab}}=N/\overline{[N,N]}.$$

For a set of primes $\Sigma$, the $\Sigma$-version replaces $N^{\mathrm{ab}}$ by $(N^\Sigma)^{\mathrm{ab}}$, where $N^\Sigma$ is the maximal pro-$\Sigma$ quotient.

Lean code

`ProCGroups.FiniteStepSolvableQuotients.IsAbFaithful`

Published library source ↗Same source in NYLL ↗

def IsAbFaithful
    (G : Type u) [TopologicalSpace G] [Group G] [IsTopologicalGroup G] : Prop

In-scope Lean context

open scoped Topology

namespace ProCGroups.FiniteStepSolvableQuotients

open ProCGroups.ProC ProCGroups.Abelian

universe u

Full declaration and proof

/-- Every open subgroup acts faithfully on the topological abelianization
of each open normal subgroup. -/
def IsAbFaithful
    (G : Type u) [TopologicalSpace G] [Group G] [IsTopologicalGroup G] : Prop :=
  ∀ H : OpenSubgroup G,
    ∀ N : OpenNormalSubgroup ↥(H : Subgroup G),
      Function.Injective
        (quotientConjugationTopologicalAbelianizationMap
          (G := ↥(H : Subgroup G)) (N := (N : Subgroup ↥(H : Subgroup G))))

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