Keyboard shortcuts

Press ← or → to navigate between chapters

Press ? to show this help

Press Esc to hide this help

Actual minimal-normal factor orbits

Abstract

The action of a prescribed automorphism tuple partitions actual minimal normal factors into invariant dependent product blocks.

Definition 1.1 (The image action).

Lean statement: D5/S3/FiniteGroups/NikolovSegal/FactorOrbits.minimalFactorAction

Formalization. D5/S3/FiniteGroups/NikolovSegal/FactorOrbits.minimalFactorAction (✓ std3).

Source. Repository-derived.

Commentary.

For any group A, an automorphism acts on each actual minimal nontrivial normal subgroup M by its subgroup image. The instance proves the identity and composition action laws.

Definition 1.2 (The factor permutation homomorphism).

Lean statement: D5/S3/FiniteGroups/NikolovSegal/FactorOrbits.minimalFactorPermutation

Formalization. D5/S3/FiniteGroups/NikolovSegal/FactorOrbits.minimalFactorPermutation (✓ std3).

Source. Repository-derived.

Commentary.

The image action gives a homomorphism from MulAut(A) to permutations of MinimalNormalFactor(A). Its identity and multiplication laws are those of the actual group action.

Definition 1.3 (The prescribed generated group).

Lean statement: D5/S3/FiniteGroups/NikolovSegal/FactorOrbits.prescribedActionGroup

Formalization. D5/S3/FiniteGroups/NikolovSegal/FactorOrbits.prescribedActionGroup (✓ std3).

Source. Repository-derived.

Commentary.

For k indexed by Fin m, prescribedActionGroup(k) is the subgroup of MulAut(A) generated by the range of k.

Definition 1.4 (The orbit quotient).

Lean statement: D5/S3/FiniteGroups/NikolovSegal/FactorOrbits.FactorOrbit

Formalization. D5/S3/FiniteGroups/NikolovSegal/FactorOrbits.FactorOrbit (✓ std3).

Source. Repository-derived.

Commentary.

FactorOrbit(k) is the quotient of actual minimal normal factors by the action of prescribedActionGroup(k), rather than the full automorphism group.

Definition 1.5 (The factors in one orbit).

Lean statement: D5/S3/FiniteGroups/NikolovSegal/FactorOrbits.OrbitFactor

Formalization. D5/S3/FiniteGroups/NikolovSegal/FactorOrbits.OrbitFactor (✓ std3).

Source. Repository-derived.

Commentary.

For an orbit o, OrbitFactor(k,o) is the subtype of actual factors belonging to o.

Definition 1.6 (The dependent block product).

Lean statement: D5/S3/FiniteGroups/NikolovSegal/FactorOrbits.OrbitBlock

Formalization. D5/S3/FiniteGroups/NikolovSegal/FactorOrbits.OrbitBlock (✓ std3).

Source. Repository-derived.

Commentary.

OrbitBlock(k,o) is the dependent product of the underlying subgroup groups M over all M in OrbitFactor(k,o).

Definition 1.7 (The restricted block automorphism).

Lean statement: D5/S3/FiniteGroups/NikolovSegal/FactorOrbits.orbitBlockAut

Formalization. D5/S3/FiniteGroups/NikolovSegal/FactorOrbits.orbitBlockAut (✓ std3).

Source. Repository-derived.

Commentary.

Every element of prescribedActionGroup(k) defines an automorphism of OrbitBlock(k,o): the output at M applies the ambient automorphism to the input at its inverse image. Subgroup membership, both inverse laws and multiplication preservation are proved.

Definition 1.8 (Restriction preserves multiplication).

Lean statement: D5/S3/FiniteGroups/NikolovSegal/FactorOrbits.orbitBlockAutHom

Formalization. D5/S3/FiniteGroups/NikolovSegal/FactorOrbits.orbitBlockAutHom (✓ std3).

Source. Repository-derived.

Commentary.

Restriction to each orbit block is a homomorphism from prescribedActionGroup(k) to its block automorphisms. It satisfies the identity and composition laws.

Definition 1.9 (The restricted tuple).

Lean statement: D5/S3/FiniteGroups/NikolovSegal/FactorOrbits.prescribedOrbitAut

Formalization. D5/S3/FiniteGroups/NikolovSegal/FactorOrbits.prescribedOrbitAut (✓ std3).

Source. Repository-derived.

Commentary.

Each k(i), with its membership in the generated group, restricts to an automorphism of every orbit block.

Definition 1.10 (Permutations within an orbit).

Lean statement: D5/S3/FiniteGroups/NikolovSegal/FactorOrbits.orbitFactorPermutation

Formalization. D5/S3/FiniteGroups/NikolovSegal/FactorOrbits.orbitFactorPermutation (✓ std3).

Source. Repository-derived.

Commentary.

The generated group acts on the actual factors in each orbit, giving a permutation homomorphism on OrbitFactor(k,o).

Definition 1.11 (The prescribed permutations).

Lean statement: D5/S3/FiniteGroups/NikolovSegal/FactorOrbits.prescribedOrbitPermutation

Formalization. D5/S3/FiniteGroups/NikolovSegal/FactorOrbits.prescribedOrbitPermutation (✓ std3).

Source. Repository-derived.

Commentary.

The permutations induced by the original k(i) form a tuple indexed by the same Fin m.

Theorem 1.12 (The exact permutation image).

Lean statement: D5/S3/FiniteGroups/NikolovSegal/FactorOrbits.prescribedOrbitPermutation_generated

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

Source. Repository-derived.

Commentary.

For every k and orbit o, the subgroup generated by the prescribed orbit permutations equals the range of orbitFactorPermutation(k,o). The proof maps the generating tuple through the permutation homomorphism.

Theorem 1.13 (Transitivity inside each orbit).

Lean statement: D5/S3/FiniteGroups/NikolovSegal/FactorOrbits.prescribedOrbitPermutation_transitive

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

Source. Repository-derived.

Commentary.

For every k, orbit o and factors M,L in that orbit, some permutation in the subgroup generated by the prescribed orbit permutations sends M to L. Transitivity is obtained for this exact generated tuple; no transitivity of the tuple on the whole factor family is assumed.

Definition 1.14 (Regrouping the actual factors).

Lean statement: D5/S3/FiniteGroups/NikolovSegal/FactorOrbits.factorOrbitProductEquiv

Formalization. D5/S3/FiniteGroups/NikolovSegal/FactorOrbits.factorOrbitProductEquiv (✓ std3).

Source. Repository-derived.

Commentary.

For every k, the full dependent product over MinimalNormalFactor(A) is isomorphic to the dependent product of OrbitBlock(k,o) over FactorOrbit(k). Restriction and reconstruction are mutually inverse and preserve multiplication.

Definition 1.15 (Finite orbit quotient).

Lean statement: D5/S3/FiniteGroups/NikolovSegal/FactorOrbits.factorOrbitFinite

Formalization. D5/S3/FiniteGroups/NikolovSegal/FactorOrbits.factorOrbitFinite (✓ std3).

Source. Repository-derived.

Commentary.

If A is finite, FactorOrbit(k) is finite for every k.

Definition 1.16 (Each orbit contains a factor).

Lean statement: D5/S3/FiniteGroups/NikolovSegal/FactorOrbits.orbitFactorNonempty

Formalization. D5/S3/FiniteGroups/NikolovSegal/FactorOrbits.orbitFactorNonempty (✓ std3).

Source. Repository-derived.

Commentary.

For every k and every orbit o, OrbitFactor(k,o) is nonempty.

Definition 1.17 (The actual group-to-block isomorphism).

Lean statement: D5/S3/FiniteGroups/NikolovSegal/FactorOrbits.orbitProductEquiv

Formalization. D5/S3/FiniteGroups/NikolovSegal/FactorOrbits.orbitProductEquiv (✓ std3).

Source. Repository-derived.

Commentary.

For finite A with minimalNormalSocle(A) equal to top and center(A) equal to bottom, and every k, orbitProductEquiv is an isomorphism from A to the dependent product of its actual orbit blocks. It combines the internal-product isomorphism with orbit regrouping.

Theorem 1.18 (Equivariance for the generated group).

Lean statement: D5/S3/FiniteGroups/NikolovSegal/FactorOrbits.orbitProductEquiv_equivariant

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

Source. Repository-derived.

Commentary.

Under those same finite, full-socle and centerless hypotheses, for every k, generated automorphism alpha, x in A and orbit o, the o-coordinate of orbitProductEquiv(alpha(x)) equals orbitBlockAut(k,o,alpha) applied to the o-coordinate of orbitProductEquiv(x). Naturality is proved on the single-factor inclusions and hence on the full product.

Theorem 1.19 (Exact equivariance for the tuple).

Lean statement: D5/S3/FiniteGroups/NikolovSegal/FactorOrbits.orbitProductEquiv_prescribed

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

Source. Repository-derived.

Commentary.

Under the same hypotheses, for every k, i in Fin m, x in A and orbit o, the o-coordinate of orbitProductEquiv(k(i)(x)) equals prescribedOrbitAut(k,o,i) applied to the o-coordinate of orbitProductEquiv(x). This is the equivariance needed to combine the block value sets.

This is the invariant-orbit construction used on printed pages 227–228 of Nikolov and Segal, On finitely generated profinite groups, I, Annals of Mathematics 165 (2007), DOI 10.4007/annals.2007.165.171. The factor action, orbit splitting and equivariance are constructed. Coverage on these blocks remains a separate input.

References