Bounded lifts of a fixed quotient tuple

Abstract

The alternating-section supplement of Lemma 2 supplies lifts of an arbitrary quotient tuple with the same bound on its generated subgroup.

Lemma 1.1 (Lift the tuple inside the bounded-section class).

Lean statement: D5/S3/FiniteGroups/NikolovSegal/BoundedTupleLift.exists_bounded_tuple_lift

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

Source. Repository-derived.

Commentary.

For finite groups G and Q, a surjective homomorphism q from G to Q, arbitrary naturals d and k with k at least four, and a tuple y from Fin d to Q whose generated subgroup has alpha at most k, there is a tuple z from Fin d to G with q(z(i)) equal to y(i) for every i and alpha of the subgroup generated by z at most k. No rank bound on the full preimage is assumed. Apply Lemma 2 to the kernel of the map from the preimage of the subgroup generated by y, then correct each lift into the same supplement and include its generated subgroup.

References

• Truth anchor: D5/S3/FiniteGroups/NikolovSegal/BoundedTupleLift.exists_bounded_tuple_lift
• Dependency: D5/S3/FiniteGroups/GaschutzFixed
• Dependency: D5/S3/FiniteGroups/NikolovSegal/SectionClosure