Ab-faithfulness of absolute Galois groups

Formalization of Naganori Yamaguchi's Ab-faithfulness of absolute Galois groups in number theory, using the numbering of arXiv v1. Covers solvable extensions, cohomological criteria, slimness and field examples. Example…

This aggregate collects principal-unit logarithms and exponentials, cyclotomic eigenunits, and logarithmic character methods used in the abelian-faithfulness results.

Openness, closedness, torsion-freeness, and separation of the actual logarithm image in Section 3 of Yamaguchi, arXiv:2610.05634v1.

An eigenvector in a finite Galois extension remains in that field after multiplication by a power of the residue prime. In a complete mixed-characteristic overfield, a suitable such multiple is a principal-unit logarithm…

The set of nonzero character eigenvectors in the intermediate field whose images are principal-unit logarithms is nonempty by a scaled normal basis. The uniform logarithmic bound and integer-valued valuation give a minim…

The range carries its inherited p-adic module structure. Twisting its actual representation and taking subgroup invariants constructs the character subspace. Normality supplies stability under the full group action; it i…

If the actual action is trivial modulo p, its averaging kernel is p-divisible. The valuation lower bound on actual principal-unit logarithms forces that kernel to vanish. Thus every vector is invariant. The mod-p input i…

The normal-basis minimum is taken for the full lower cyclotomic group. Restriction of automorphisms, compatibility of the actual p-adic scalar maps, and character averaging give an eigenunit in the upper field with this…

The actual logarithm intertwines the constructed p-adic representations. The group order is a unit because it is prime to the residue characteristic, so character averaging produces an eigenvector preimage.

An automorphism fixing the lower field fixes the logarithm of the given principal unit. A nontrivial bounded exponent therefore produces a scalar multiple in the same lower-field character part, still in the logarithm im…

A field-unit witness for the ratio of an automorphic principal unit and an ordinary power is itself a principal unit. Its logarithm is determined by the same field automorphism and power relation.

A subgroup-supported normal-basis vector is an eigenvector for the subgroup and fails the prescribed character relation at an automorphism outside it. Multiplying by a power of the residue prime puts the vector in the pr…

Lines 460–467 of Section 3. P is literally p²𝒪K and U is 1 + p²𝒪K. The canonical evaluated series give inverse additive and multiplicative homomorphisms on these sets. This statement makes no finiteness assumption on the…

This aggregate collects finitely generated and sub-p-adic field examples, valuation models, and finiteness of roots of unity.

A nonzero base-ring element that is a nonunit in a valuation ring remains a nonunit in a discrete valuation ring of an essentially finite-type extension of the base fraction field.

An essentially finite-type extension of a fraction field admits an integral finite-type model inside any valuation ring containing the base ring.

The mixed-characteristic valuation is constructed from finite generation.

Finite Galois automorphisms move discrete valuations, so local Artin--Schreier characters detect the action on abelianization modulo the characteristic.

Finite extensions of the p-adic field have finite torsion unit groups. The same finiteness holds in essentially finite-type extensions by passing to their finite extension of algebraic constants.

The separably-closed-residue corollary retained from the earlier manuscript. The residue field is required only to be separably closed.

The existence of a mixed-characteristic discrete valuation is preserved under essentially finite-type field extensions and restriction along field embeddings.

A finite separable extension of a subfield embeds in a finite extension of the ambient field. In characteristic zero this descends finiteness of primary roots of unity to finite extensions of the subfield.

An embedding into an essentially finite-type p-adic extension supplies abelian faithfulness and finiteness of primary roots of unity in every finite extension of the embedded field.

The general group-theoretic definitions and proofs are maintained in ProCGroups.FiniteStepSolvableQuotients.AbTorsionFree. This module preserves existing downstream imports without duplicate declarations.

Restriction to the separable closure supplies the orientation on the actual algebraic-closure Galois group, including imperfect base fields.

Basic formal Hilbert 90 definitions and unnumbered supporting results.

These are the cocycle lifting assertions used in the earlier manuscript. The hypothesis concerns this H alone; no lifting on its open subgroups is assumed. Compatible successive lifts give a continuous p-adic cocycle.

A cyclic extension of prime degree in positive characteristic supplies an orientation satisfying formal Hilbert 90 with infinite image.

Adjoining every primary root of unity gives the primary cyclotomic extension. Infinite degree of that extension forces the absolute cyclotomic orientation to have infinite image.

The orientation is the actual cyclotomic character on the field automorphisms. Hilbert 90 supplies the cohomology reduction on every open subgroup.

The earlier roots-of-unity / Artin–Schreier form of the field criterion. The current extension-based statement is in Theorem6Dot6AbsoluteCenter.lean. The roots-of-unity condition concerns every finite extension inside th…

Under relative formal Hilbert 90, globally fixed primary classes inject into the primary abelianization of the ambient group.

The stronger oriented-invariants theorem retained from the earlier manuscript. It implies current Lemma 6.2 and additionally proves torsion-freeness and injectivity of the fixed-inclusion map. The fixed-point assertions…

Transfer of a p-adic character evaluates on a globally fixed primary class as multiplication by the index of the open normal subgroup.

The earlier all-primes relative criterion, retained in the foundation layer. The current Σ-quotient theorem is Theorem6Dot4RelativeCriterion.lean. The quotient is the actual G/[D,D], with closed commutator subgroup. The…

Centralizing classes in relative derived quotients yield fixed primary abelianization classes. Vanishing of these fixed classes forces the centralizing quotient class to be trivial.

Sigma-abelian faithfulness makes the action on an open normal subgroup injective. An element centralizing that subgroup in a sigma-residual quotient consequently belongs to the subgroup.

Centralizing classes in sigma-residual quotients project to fixed primary classes for primes in sigma. Vanishing of those fixed classes forces the centralizing quotient class to be trivial.

The criterion retained from the earlier manuscript identifies formal Hilbert 90 for the trivial orientation with the absence of ℓ-torsion in every open-subgroup abelianization. Ab-torsion-freeness then supplies formal Hi…

The general construction lives in ProCGroups.Abelian.AbelianModPower. These aliases preserve names exposed by the earlier paper-specific module.

This aggregate module exposes faithfulness properties of conjugation actions on topological abelianizations and their consequences for slimness and torsion.

For each actual finite quotient, apply the elementary-kernel solver to the regular wreath product with cyclic coefficient group of order q. Its right projection and canonical section give the split problem, while its act…

The elementary solver passes to each open subgroup by the induced-kernel construction. Applied to the actual regular wreath product, it produces a proper solution with faithful kernel action for each finite quotient. No…

Source: Yamaguchi, arXiv:2610.05634v1, Proposition 2.1. TopologicalEmbeddingProblem, ProperSolution, and IsSplit model the paper's embedding-problem terminology. The hypothesis below says that every finite split problem…

An invariant finite quotient of the abelianization of an open normal subgroup produces an open normal subgroup of the ambient group and a proper finite embedding problem.

The unnumbered equivariant-action observation in Section 1 of Yamaguchi, arXiv:2610.05634v1.

The general group-theoretic definitions and proofs are maintained in ProCGroups.FiniteStepSolvableQuotients.Faithful. This module preserves existing downstream imports without duplicate declarations.

Conjugation descends along an epimorphism with abelian kernel. Its faithfulness is characterized by the kernel being its own centralizer.

Ab-faithfulness of the absolute Galois group passes to finite field extensions, including inseparable extensions.

A nonfaithful finite quotient action has a prime-order subgroup in its kernel. Pulling that subgroup back gives an open layer with prime-order quotient and trivial action on the topological abelianization of its kernel.

For a compact totally disconnected abelian group, failure to be a prime-power power is detected by a continuous character of prime-power order.

The right projection of the regular wreath product has a commutative kernel when the coefficient group is commutative. A nontrivial coefficient group makes the quotient's conjugation action faithful, by evaluation on a f…

A faithful finite relative action on the actual residual abelianization admits a faithful finite invariant quotient in the original formation. Pulling its projection back to the normal subgroup produces an open normal su…

A homomorphism with finite image in a full formation factors through the actual residual quotient. If its image is commutative, equality after topological abelianization of that quotient forces equality in the image. Con…

A faithful finite invariant quotient of the residual abelianization gives an open normal ambient kernel. Its subgroup image is abelian and self-centralizing. The first isomorphism theorem identifies that actual image wit…

An abelian normal subgroup meeting a prime-order relative quotient nontrivially acts trivially on the residual abelianization when that prime is excluded. The commutator power identity and the required power injectivity…

The actual finite ambient quotient constructed from a faithful residual abelian quotient supplies the extension and its proper solution. Its kernel is exactly the image of the original normal subgroup, so it is a Sigma g…

For each finite quotient, the extension with finite abelian Sigma kernel may be chosen separately. A proper solution is surjective. Its image of the original kernel lies in the Sigma kernel, so the actual residual quotie…

A topological group equivalence identifies every open layer and its normal quotient action on the actual residual abelianization.

The quantifiers range over all open subgroups and all their open normal subgroups, without restricting the prime divisors of the relative index. The action is the existing conjugation action on the actual residual quotie…

Open subgroups and their open normal subgroups are pulled back along the actual residual projection. The maximal-quotient subgroup comparison identifies the residual quotient of each preimage with the original subgroup a…

The subgroup of an open subgroup is mapped into the ambient group by the actual subtype inclusion. Residual conjugation is transported by the resulting continuous group equivalence.

A prime-order subgroup of the kernel of a nonfaithful quotient action pulls back to an open layer in the original group. The two presentations of its normal subgroup have canonically equivalent residual quotients, and th…

Every closed subgroup of a pro-Sigma group is pro-Sigma. Its actual residual quotient therefore retains the ordinary abelianization action.

For an excluded prime, a normal pro-p subgroup acts trivially on the actual maximal pro-Sigma quotient of every open normal subgroup. Sigma-faithfulness puts it inside every open normal subgroup, whose intersection is tr…

Slimness is preserved by continuous group isomorphisms. A finite extension of a field with slim absolute Galois group has center-free absolute Galois group.

The general group-theoretic definitions and proofs are maintained in ProCGroups.FiniteStepSolvableQuotients.SlimnessAndTorsion. This module preserves existing downstream imports without duplicate declarations.

This aggregate collects the definition, positive-characteristic theory, and properties of higher local fields used in abelian-faithfulness results.

A zero-dimensional higher local field is a finite field. At each successor step we choose a complete discrete valuation whose actual residue field is one dimension lower. No Galois-theoretic or finite-extension permanenc…

Finite extensions inherit the higher local field structure. On every open Galois layer, prime-degree detection follows from Artin--Schreier classes over the complete discrete valuation at the first level. No embedding-pr…

The stronger joint root-finiteness and ab-faithfulness statement supporting Theorem 4.2 of Yamaguchi, arXiv:2610.05634v1.

This aggregate collects Kummer comparisons, valuation and cohomology detection, prime-degree reductions, and local methods for abelian faithfulness.

The stronger abelian-quotient form of current Proposition 3.5. The action is formed on the actual quotient GLᵃᵇ/p. The prime-to-p branch uses faithful mod-p H¹ and its character-dual action on the actual abelianization q…

The maximal pro-p quotient is the actual quotient by the pro-p residual core. The absolute Galois comparison carries this core onto the corresponding core of the completion, giving a continuous group isomorphism and pres…

This aggregate collects mixed-characteristic Kummer detection and faithfulness arguments, roots downstairs, and residue-characteristic zero inertia and unramified detection.

The residue prime controls the coefficients. The Galois extension degree can be any prime: residue-prime degree uses wild detection, while a different prime degree is already detected at the first p-power level.

Both cyclotomic fields are constructed in an actual algebraic closure. A complete integer-valued extension valuation and its residue characteristic are generated from the base. The two-branch detection then gives a nontr…

The positive branch descends the actual invariant Kummer trace. Triviality of the lower action would fix that same trace, contradicting its construction. The other branch uses the logarithmic minimum argument. The common…

The p-adic eigenunit relation supplies the power action on the field's Kummer quotient. The actual finite cyclotomic character supplies the same power action on all roots at the selected level. These two actions cancel i…

The character space uses the kernel of the actual normal restriction map. Its vectors lift to cyclotomic eigenunits. Kummer descent gives a logarithm for each character difference; multiplying by the inverse character an…

The actual Kummer power witness gives a principal-unit logarithm after subtracting the finite exponent. The exponent agrees modulo p with the specified primitive-root character, so a p-adic power corrects that logarithm…

The actual cyclotomic eigenunit gives an invariant character over the intermediate field. Descent across the cyclotomic degree and triviality of the lower H¹ action make that character invariant under a compatible lift.…

The minimal logarithmic eigenvector and its eigenunit are generated from the two cyclotomic extensions. A trivial lower H¹ action produces an actual power witness. If its bounded exponent differs from one, its logarithm…

Faithful H¹ supplies a changed finite p-power character. The actual closure comparison moves that character to the fixing subgroup, and its factorization through the pro-p residual quotient detects the same ambient conju…

Over a complete mixed-characteristic discretely valued base, the quotient by a prime-degree fixing subgroup acts faithfully on the topological abelianization of that subgroup's intrinsic pro-p residual quotient.

The actual completion Galois equivalence carries an open normal subgroup to an open normal subgroup of the same index. Completion preserves the residue characteristic, and transport of residual conjugation returns faithf…

The original prime degree and the two cyclotomic extensions supply the upper prime-degree Galois extension. A nonidentity automorphism, an eigenunit with primitive eigenvalue, and the last positive root level are chosen…

The upper extension is Galois by its actual splitting-field construction. A root outside the lower cyclotomic field is moved by a Galois automorphism. Its restriction cannot act trivially on H¹, since the logarithmic min…

Infinite Galois correspondence constructs the finite Galois fixed field of an open normal subgroup. Its degree is the given index, so the established field detection applies to the subgroup's actual pro-p residual quotie…

The cyclotomic field and its complete discrete valuation are constructed from the base field. The logarithmic detection theorem then applies with no auxiliary field or representation data in the public statement.

The normal-basis character vector and its principal-unit logarithm are noninvariant under an automorphism outside the cyclotomic restriction kernel. Trivial lower mod-p cohomology would make all action differences p-divi…

For a prime-degree Galois extension M/K of a mixed-characteristic Henselian DVF, the relative Galois group acts faithfully on the abelianization of the actual maximal pro-p quotient of the absolute Galois group of M. The…

A nonidentity inertia element in a prime-degree Galois extension supplies a primitive root. Every primary root descends to the base, and finite residual primary roots make the existing roots-downstairs Kummer detection a…

For a residue-zero Henselian discrete valuation, ab-faithfulness of the residue Galois group and finite primary root groups imply faithfulness of the conjugation action associated with a prime-index open normal subgroup.

Residue ab-faithfulness detects quotient conjugation on every open normal subgroup that contains the actual inertia kernel.

For a prime-degree Galois extension with finite prime-power roots all in the base, each nonidentity automorphism moves a continuous degree-one class. The eigenunit, coefficient exponent, character, and point detecting mo…

The moved classes constructed from eigenunits detect the genuine relative Galois action on H¹ and the canonical action on topological abelianization.

Inside any algebraic closure, the quotient by the fixing subgroup of a prime-degree Galois intermediate field acts faithfully on that subgroup's topological abelianization under the roots-downstairs hypotheses.

Infinite Galois correspondence supplies the finite Galois fixed field of an open normal subgroup. Prime quotient order supplies its prime field degree, so roots-downstairs detection applies to the original quotient actio…

The separable Kummer equivalence and its actual absolute conjugation formula produce the last-root-level detecting character. Prime-degree Galois theory then gives faithful H¹ action, without a characteristic-zero assump…

The dyadic detection result retained from the earlier manuscript. A quadratic norm outside the two square classes gives a nonsquare norm in the extension. Trivial conjugation on the actual mod-two abelianization would ma…

Prime-degree detection yields faithful mod-prime abelianization actions for finite Galois extensions by passing to fixed fields of prime-order subgroups in a hypothetical kernel.

Nontrivial finite-order automorphisms move discrete valuations. A local Artin--Schreier character and weak approximation detect their action modulo the characteristic, including over imperfect fields.

When a prolongation is invariant under the Galois group, its completion has the same Galois degree. The complete-field detection theorem detects an automorphism there, and the injective weak-approximation map transports…

Each open absolute Galois subgroup is the absolute group of its actual finite fixed field. Its Henselian discrete valuation and residue prime are constructed from the base. Prime-index detection, including primes distinc…

A nonzero residue-prime character of one completion and the zero character of its inequivalent conjugate extend simultaneously by weak approximation. Their different values detect the relative action on abelianization mo…

A prolongation is either invariant under every automorphism or is moved by one. Completion detects the first case, and simultaneous character approximation detects the second case. No completeness or Henselian hypothesis…

An unnumbered auxiliary reduction for Section 3 of Yamaguchi, arXiv:2610.05634v1. The hypothesis is made on the actual quotient GLᵃᵇ/p for every mixed-characteristic discretely valued field and every prime-degree Galois…

A moved mod-prime abelianization class yields a nontrivial relative Galois cohomology action. The inverse automorphism reflects contravariant pullback.

Artin--Schreier classes are infinite over a discretely valued field. In degree p, finite restriction kernels and additive Hilbert 90 detect the action. In every other prime degree, a norm valuation and a base-field multi…

Fixed fields in a separable closure give finite extensions even over imperfect fields. The actual comparison with the algebraic-closure absolute action transports prime-degree detection to every open Galois layer.

This is stronger than Lemma 3.2 of Yamaguchi, arXiv:2610.05634v1: it requires neither μp ⊆ K nor completeness.

Fixed-field comparison transports the actual mod-prime action to conjugation on the residual abelianization. Discrete prolongations supply the hypothesis on each open layer without completeness or Henselianity assumption…

The conjugation map on the absolute Galois group is a continuous automorphism. Passing to its topological abelianization and then modulo q-th powers gives the actual map used in Section 3.

An embedding intertwining two relative automorphisms intertwines their actions on the actual absolute Galois abelianizations, independently of closure lifts.

Ab-faithfulness of the residue Galois group and finite primary root groups in its finite field extensions imply ab-faithfulness of the absolute Galois group of the Henselian discretely valued field.

Slimness over a residue-zero Henselian discrete valuation forces finite primary root groups in every finite residue extension. Ab-faithfulness provides the corresponding specialization.

Equation eq:kummer-trivial in Section 3. The left side says that conjugation is trivial on GKᵃᵇ/n, using its exact character-dual description: every continuous ZMod n-valued character is fixed. The right side says τ(x)/x…

Weak approximation prescribes a nonzero character on one completion and the zero character on its inequivalent conjugate. These characters detect the relative Galois action on abelianization modulo a prime.

The stronger simultaneous character-approximation theorem retained from the earlier manuscript. The restriction of a character uses mathlib's actual continuous absolute Galois-group map attached to the canonical embeddin…

In Definition 1.1 of Yamaguchi, arXiv:2610.05634v1, Σ-ab-faithfulness means that, for every open H ≤ G and open normal N ⊴ H, the quotient H/N acts faithfully on the topological abelianization of the maximal pro-Σ quotie…

Source: Yamaguchi, arXiv:2610.05634v1, Lemma 1.2. Condition (iii) is expressed directly in the abelianization: two classes agree modulo ℓ ^ s precisely when they differ by an ℓ ^ s-th power. The prime order of H/N is not…

Source: Yamaguchi, arXiv:2610.05634v1, Remark 1.3. The first conjunct also records the all-primes identification stated with the definition.

Source: Yamaguchi, arXiv:2610.05634v1, Proposition 2.1. The stronger regular-module quotient construction is retained in GroupTheory/ElementarySplitRegularQuotient.lean.

The proof is the existing shared valuation theorem; this paper leaf records its exact mixed-characteristic statement under the paper's numbering.

Source: Yamaguchi, arXiv:2610.05634v1, Lemma 3.3. The separation hypothesis is stated elementwise; no finite generation is assumed.

Source: Yamaguchi, arXiv:2610.05634v1, Lemma 3.4. The logarithm below is the existing convergent logarithm series homomorphism. Closure under the canonical p-adic scalars expresses the submodule assertion without install…

Source: Yamaguchi, arXiv:2610.05634v1, Proposition 3.5.

Theorem 3.6 of Yamaguchi, arXiv:2610.05634v1. Its first assertion is stated on the actual quotient GLᵃᵇ/p.

Source: Yamaguchi, arXiv:2610.05634v1, Lemma 4.1.

Source: Yamaguchi, arXiv:2610.05634v1, Theorem 4.2. The stronger result including finiteness of roots is in HigherLocalField/Properties.lean.

Source: Yamaguchi, arXiv:2610.05634v1, Lemma 5.1. We use the finite group of functions with constant right differences along the last derived subgroup. It contains the manuscript's W and transversal function. Its differe…

Source: Yamaguchi, arXiv:2610.05634v1, Proposition 5.2. For an open subgroup of G^m, choose a smaller open normal subgroup avoiding a nonidentity centralizing element. Lemma 5.1 supplies the finite split problem. Its pro…

This module constructs the twisted coefficient representations from a continuous p-adic orientation and states formal Hilbert 90 using mathlib's continuous first cohomology and its functorial reduction map. Explicit cont…

Source: Yamaguchi, arXiv:2610.05634v1, Lemma 6.2. The stronger torsion-freeness and fixed-inclusion theorem is retained in FormalHilbert90/OrientedInvariants.lean.

Source: Yamaguchi, arXiv:2610.05634v1, Lemma 6.3.

Source: Yamaguchi, arXiv:2610.05634v1, Theorem 6.4. The previous criterion for G/[D,D], requiring only relative Hilbert 90, is retained in FormalHilbert90/RelativeDerivedCriterion.lean.

Yamaguchi, arXiv:2610.05634v1, Corollary 6.5. Each orientation satisfies formal Hilbert 90 on every open subgroup.

Yamaguchi, arXiv:2610.05634v1, Corollary 6.6. Cyclotomic and trivial orientations supply formal Hilbert 90; no orientation or cohomology hypothesis is added to the field statement.

Example 6.7 of Yamaguchi, arXiv:2610.05634v1. The toral Kummer condition is imposed on actual units of every finite extension. The higher-local-field Artin--Schreier condition follows directly from the first discrete val…