Keyboard shortcuts

Press ← or → to navigate between chapters

Press ? to show this help

Press Esc to hide this help

Part II SL3UnipotentNormalizer

Abstract

Part II SL3UnipotentNormalizer.

Theorem 1.1 (below diagonal zero of normalizer).

Lean statement: D5/S3/FiniteGroups/NikolovSegal/PartIISL3UnipotentNormalizer.below_diagonal_zero_of_normalizer

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

Source. Repository-derived.

Commentary.

Every element of the normalizer of the actual upper-unitriangular subgroup has all entries below the diagonal equal to zero.

Theorem 1.2 (conjugate mem U3 of upper).

Lean statement: D5/S3/FiniteGroups/NikolovSegal/PartIISL3UnipotentNormalizer.conjugate_mem_U3_of_upper

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

Source. Repository-derived.

Commentary.

Conjugation by an actual upper-triangular SL3 matrix preserves every upper-unitriangular matrix.

Theorem 1.3 (mem normalizer iff upper).

Lean statement: D5/S3/FiniteGroups/NikolovSegal/PartIISL3UnipotentNormalizer.mem_normalizer_iff_upper

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

Source. Repository-derived.

Commentary.

An actual SL3 matrix normalizes the upper-unitriangular subgroup exactly when it is upper triangular. This holds over every field.

Theorem 1.4 (automorphism normalizer map).

Lean statement: D5/S3/FiniteGroups/NikolovSegal/PartIISL3UnipotentNormalizer.automorphism_normalizer_map

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

Source. Repository-derived.

Commentary.

A genuine automorphism preserving the actual upper-unitriangular subgroup also preserves its normalizer as a subgroup.

Theorem 1.5 (automorphism upper iff).

Lean statement: D5/S3/FiniteGroups/NikolovSegal/PartIISL3UnipotentNormalizer.automorphism_upper_iff

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

Source. Repository-derived.

Commentary.

For an automorphism preserving the actual upper-unitriangular subgroup, beta(g) is upper triangular exactly when g is upper triangular.

Nikolov and Segal, On finitely generated profinite groups, I: Strong completeness and uniform bounds, Annals of Mathematics 165 (2007), 171-238, DOI 10.4007/annals.2007.165.171, Section 10, Proposition 10.2 and equations (45)-(50) (pages 228-232). Part II: Products in quasisimple groups, Annals of Mathematics 165 (2007), 239-273, DOI 10.4007/annals.2007.165.239, Theorem 1.2, Lemma 4.1 (pages 247-248), Section 6, Proposition 6.2, and Lemma 7.1(a) with its A2 orbital application (pages 257-261). These are formal adaptations and consequences of published mathematics, using actual matrix geometry, finite-field arithmetic and Sylow arguments. No originality claim or redistribution of the papers is made. The scalar, twisted and transitive conclusions here concern the SL3 family. Other families, CFSG exhaustion, general central covers, the full all-simple scalar supplier, all-length Proposition 10.2, width and restricted Burnside bounds, and strong completeness remain open.

References