Keyboard shortcuts

Press ← or → to navigate between chapters

Press ? to show this help

Press Esc to hide this help

Part IIUnitary Projective Prescribed Product

Abstract

The projective carrier is the actual quotient of SU by its center. Genuine automorphisms descend through characteristicity of the center. Quotient maps preserve corrected powers and the actual ordered value product. No arbitrary projective automorphism is assumed to lift.

Definition 1.1 (projectiveSpecialUnitary).

Lean statement: D5/S3/FiniteGroups/NikolovSegal/Unitary/PartIIUnitaryProjectivePrescribedProduct.projectiveSpecialUnitary

Formalization. D5/S3/FiniteGroups/NikolovSegal/Unitary/PartIIUnitaryProjectivePrescribedProduct.projectiveSpecialUnitary (✓ std3).

Source. Repository-derived.

Commentary.

The parameterized projectiveSpecialUnitary statement describes the actual unitary geometry or prescribed ordered-product construction. Its Lean telescope retains every field, rank, involution, input and equality hypothesis shown.

Definition 1.2 (pi).

Lean statement: D5/S3/FiniteGroups/NikolovSegal/Unitary/PartIIUnitaryProjectivePrescribedProduct.pi

Formalization. D5/S3/FiniteGroups/NikolovSegal/Unitary/PartIIUnitaryProjectivePrescribedProduct.pi (✓ std3).

Source. Repository-derived.

Commentary.

The parameterized pi statement describes the actual unitary geometry or prescribed ordered-product construction. Its Lean telescope retains every field, rank, involution, input and equality hypothesis shown.

Definition 1.3 (projectiveAction).

Lean statement: D5/S3/FiniteGroups/NikolovSegal/Unitary/PartIIUnitaryProjectivePrescribedProduct.projectiveAction

Formalization. D5/S3/FiniteGroups/NikolovSegal/Unitary/PartIIUnitaryProjectivePrescribedProduct.projectiveAction (✓ std3).

Source. Repository-derived.

Commentary.

The parameterized projectiveAction statement describes the actual unitary geometry or prescribed ordered-product construction. Its Lean telescope retains every field, rank, involution, input and equality hypothesis shown.

Theorem 1.4 (action pi).

Lean statement: D5/S3/FiniteGroups/NikolovSegal/Unitary/PartIIUnitaryProjectivePrescribedProduct.action_pi

Proof. Machine-checked in Lean as D5/S3/FiniteGroups/NikolovSegal/Unitary/PartIIUnitaryProjectivePrescribedProduct.action_pi (✓ std3). ∎

Source. Repository-derived.

Commentary.

The parameterized action pi statement describes the actual unitary geometry or prescribed ordered-product construction. Its Lean telescope retains every field, rank, involution, input and equality hypothesis shown.

Theorem 1.5 (corrected power pi).

Lean statement: D5/S3/FiniteGroups/NikolovSegal/Unitary/PartIIUnitaryProjectivePrescribedProduct.corrected_power_pi

Proof. Machine-checked in Lean as D5/S3/FiniteGroups/NikolovSegal/Unitary/PartIIUnitaryProjectivePrescribedProduct.corrected_power_pi (✓ std3). ∎

Source. Repository-derived.

Commentary.

The parameterized corrected power pi statement describes the actual unitary geometry or prescribed ordered-product construction. Its Lean telescope retains every field, rank, involution, input and equality hypothesis shown.

Theorem 1.6 (ordered corrected values pi).

Lean statement: D5/S3/FiniteGroups/NikolovSegal/Unitary/PartIIUnitaryProjectivePrescribedProduct.ordered_corrected_values_pi

Proof. Machine-checked in Lean as D5/S3/FiniteGroups/NikolovSegal/Unitary/PartIIUnitaryProjectivePrescribedProduct.ordered_corrected_values_pi (✓ std3). ∎

Source. Repository-derived.

Commentary.

The parameterized ordered corrected values pi statement describes the actual unitary geometry or prescribed ordered-product construction. Its Lean telescope retains every field, rank, involution, input and equality hypothesis shown.

Theorem 1.7 (actual uniform projective positive q over e product).

Lean statement: D5/S3/FiniteGroups/NikolovSegal/Unitary/PartIIUnitaryProjectivePrescribedProduct.actual_uniform_projective_positive_q_over_e_product

Proof. Machine-checked in Lean as D5/S3/FiniteGroups/NikolovSegal/Unitary/PartIIUnitaryProjectivePrescribedProduct.actual_uniform_projective_positive_q_over_e_product (✓ std3). ∎

Source. Repository-derived.

Commentary.

The parameterized actual uniform projective positive q over e product statement describes the actual unitary geometry or prescribed ordered-product construction. Its Lean telescope retains every field, rank, involution, input and equality hypothesis shown.

Theorem 1.8 (actual uniform projective negative q over e product).

Lean statement: D5/S3/FiniteGroups/NikolovSegal/Unitary/PartIIUnitaryProjectivePrescribedProduct.actual_uniform_projective_negative_q_over_e_product

Proof. Machine-checked in Lean as D5/S3/FiniteGroups/NikolovSegal/Unitary/PartIIUnitaryProjectivePrescribedProduct.actual_uniform_projective_negative_q_over_e_product (✓ std3). ∎

Source. Repository-derived.

Commentary.

The parameterized actual uniform projective negative q over e product statement describes the actual unitary geometry or prescribed ordered-product construction. Its Lean telescope retains every field, rank, involution, input and equality hypothesis shown.

The results concern special-unitary matrix groups over finite fields. Their geometric setting is Nikolov and Segal, On finitely generated profinite groups, II: Products in quasisimple groups, Annals of Mathematics 165 (2007), 239-273, DOI 10.4007/annals.2007.165.239. Prescribed-product statements retain their field-size, rank and automorphism hypotheses.

References