Keyboard shortcuts

Press ← or → to navigate between chapters

Press ? to show this help

Press Esc to hide this help

Generator decomposition under explicit absorption

Abstract

Finite-order induction gives the generator decomposition with a fixed exact power-product length under a uniform minimal-normal absorption premise.

Definition 1.1 (The unproved large minimal-normal input).

Lean statement: D5/S3/FiniteGroups/NikolovSegal/GeneratorDecomposition.LargeMinimalNormalAbsorption

Formalization. D5/S3/FiniteGroups/NikolovSegal/GeneratorDecomposition.LargeMinimalNormalAbsorption (✓ std3).

Source. Repository-derived.

Commentary.

Fix natural q, m and k before quantifying over all finite groups G in an arbitrary universe. For every subgroup N minimal among nontrivial normal subgroups, if alpha(N) is greater than k, then every a in N and every x in orderedPowerProducts(G,q,m) satisfy a*x in that same set. Absorption acts on the left and preserves the same exact m ordered qth-power factors. This proposition is an explicit input, with no supplied proof. In the paper the corresponding input follows from Proposition 2 and the classification of minimal normal subgroups.

Theorem 1.2 (Complete induction for every finite group).

Lean statement: D5/S3/FiniteGroups/NikolovSegal/GeneratorDecomposition.generator_decomposition_of_absorption

Proof. Machine-checked in Lean as D5/S3/FiniteGroups/NikolovSegal/GeneratorDecomposition.generator_decomposition_of_absorption (✓ std3). ∎

Citation. Nikolay Nikolov and Dan Segal (2011). Powers in finite groups. DOI: 10.4171/GGD/136. URL: https://doi.org/10.4171/GGD/136.

Commentary.

For all natural q, m and k with k at least four, assuming LargeMinimalNormalAbsorption(q,m,k) uniformly over finite groups with m already fixed, every finite group G and natural d with Group.rank(G) at most d admit tuples x and y from Fin d to G. The closure of the union of their ranges is G; every x(i) is a product of the same exact m ordered qth powers; and alpha of the subgroup generated by y is at most k. This includes d equal to zero and arbitrary finite groups, with no solvability or commutativity assumption.

Induct on the finite order of G. For a minimal nontrivial normal subgroup N, the quotient has strictly smaller order and rank at most d. Lift the x factors in order, and lift y using the same Lemma 2 supplement. If alpha(N) is at most k, apply Gaschutz with x fixed and correct y; the corrected subgroup lies in the bounded preimage. Otherwise apply Gaschutz with y fixed and correct x; left absorption preserves every exact power-product constraint.

Taking the finite images of the two tuples gives sets X and Y of cardinality at most d with the same generation, power-product and alpha conclusions. The paper proves an unconditional Proposition 3 by supplying the absorption input. Here that input remains unproved. Uniform power width, Proposition 4, the restricted Burnside bound and strong completeness remain outside this conditional induction.

References