Nikolov-Segal Lemma 2: Supplements and Alternating Sections
Abstract
Every normal subgroup of a finite group has a supplement controlling all alternating sections of degree at least five and the largest alternating section degree.
Theorem 1.1 (Sections descend through the quotient).
Proof. Machine-checked in Lean as D5/S3/FiniteGroups/NikolovSegal/NikolovSegalLemma2.sylow_normalizer_section_transfer (✓ std3). ∎
Source. Repository-derived.
Commentary.
For a Sylow p-subgroup P of N, take the normalizer in G of its image under the inclusion of N in G. The kernel of the restricted quotient map embeds in the normalizer of P inside N. The simple-section dichotomy and the Sylow-normalizer obstruction therefore force every indicated section into G/N. The image and normalizer refer to the subgroup inclusion, not a change of section definition.
Theorem 1.2 (One supplement transfers every large alternating section).
Proof. Machine-checked in Lean as D5/S3/FiniteGroups/NikolovSegal/NikolovSegalLemma2.exists_supplement_preserving_alternating_sections (✓ 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.
Choose a Sylow 2-subgroup P of N and let L be the normalizer in G of its image. Frattini gives N join L equal to G. For every k at least five, Alt(k) is simple, has even order, and is not a 2-group, so its sections in L descend to G/N. The existential quantifier for L precedes the universal quantifier for k: the same supplement works for all such degrees.
Theorem 1.3 (The exact largest-degree inequality).
Proof. Machine-checked in Lean as D5/S3/FiniteGroups/NikolovSegal/NikolovSegalLemma2.exists_supplement_alpha_le (✓ 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.
This is Powers in finite groups, printed page 504, Lemma 2. Use the same Sylow-normalizer supplement as in the section-transfer theorem and apply the attained maximum characterization of alpha. All finite groups and all normal subgroups are allowed, including the bottom and top normal subgroups. This structural lemma does not by itself establish the power-width, restricted Burnside, or profinite strong-completeness targets.
References
- Truth anchor:
D5/S3/FiniteGroups/NikolovSegal/NikolovSegalLemma2.exists_supplement_alpha_le - Truth anchor:
D5/S3/FiniteGroups/NikolovSegal/NikolovSegalLemma2.exists_supplement_preserving_alternating_sections - Truth anchor:
D5/S3/FiniteGroups/NikolovSegal/NikolovSegalLemma2.sylow_normalizer_section_transfer - Dependency: D5/S3/FiniteGroups/NikolovSegal/Alpha
- Dependency: D5/S3/FiniteGroups/NikolovSegal/AlternatingBounds
- Dependency: D5/S3/FiniteGroups/NikolovSegal/SylowKernel