Keyboard shortcuts

Press ← or → to navigate between chapters

Press ? to show this help

Press Esc to hide this help

Minimal normal subgroups and smaller quotients

Abstract

Finite-order induction uses actual minimal nontrivial normal subgroups and coordinatewise quotient lifts.

Lemma 1.1 (A minimal nontrivial normal subgroup exists).

Lean statement: D5/S3/FiniteGroups/NikolovSegal/FiniteNormalInduction.exists_minimal_normal

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

Source. Repository-derived.

Commentary.

Every finite nontrivial group G has a subgroup N minimal for the predicate that N is normal and nontrivial. Minimality is among normal subgroups, not among all subgroups. The finite set of such subgroups is nonempty because it contains G.

Lemma 1.2 (The quotient has strictly smaller order).

Lean statement: D5/S3/FiniteGroups/NikolovSegal/FiniteNormalInduction.card_quotient_lt

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

Source. Repository-derived.

Commentary.

For every finite group G and nontrivial normal subgroup N, Nat.card(G/N) is strictly less than Nat.card(G). The subgroup has order greater than one; quotient order is positive; their product equals the order of G.

Lemma 1.3 (Coordinate lifts generate modulo the kernel).

Lean statement: D5/S3/FiniteGroups/NikolovSegal/FiniteNormalInduction.lift_tuple_generation

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

Source. Repository-derived.

Commentary.

For any group G, normal subgroup N and natural d, let x and y be tuples from Fin d to G and xq and yq tuples from Fin d to G/N. If the quotient map sends x(i) to xq(i) and y(i) to yq(i) for every i, and the two quotient tuple ranges generate G/N, then N joined with the subgroup generated by both lifted ranges is G. Finiteness and rank hypotheses are unnecessary for this statement.

References