LemmaStatement: AI-generatedProof: AI-generatedPipeline-generatedverified 2026-09-24 (gpt-6-sol)

How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

Quasisimple normal intersections and perfect central actions

Statement

If $Q$ is quasisimple and $M ⊴ Q$ is proper, then $M \leq Z (Q)$ . If $P$ is perfect, $T$ normalizes $P$ , and every commutator $t p t^{- 1} p^{- 1}$ with $t \in T$ and $p \in P$ lies in $Z (P)$ , then $T$ centralizes $P$ .

Facts & Assumptions

Given: Groups $Q, P$ , subgroups $M ⊴ Q$ and $T$ as in the statement. A group is perfect when it equals its commutator subgroup.

[F1]

Quasisimple means $Q = [Q, Q]$ and $Q / Z (Q)$ is simple. (Quasisimple groups, components, and the layer)

[F2]

A simple group has only the trivial and whole normal subgroups. (Simple groups)

[F3]

The center $Z (Q)$ commutes with every element of $Q$ , and $[x, y] = x y x^{- 1} y^{- 1}$ . (The center $Z (G)$ of a group, Commutators $[g, h] = g h g^{- 1} h^{- 1}$ and the commutator subgroup $[G, G]$ )

Proof

1.1

The image $M Z (Q) / Z (Q)$ is normal in the simple group $Q / Z (Q)$ , so it is trivial or the whole quotient. In the trivial case $M \leq Z (Q)$ . In the whole case $Q = M Z (Q)$ , and the quotient $Q / M$ is generated by the image of the abelian group $Z (Q)$ ; hence $Q / M$ is abelian. But a quotient of the perfect group $Q = [Q, Q]$ is perfect, and an abelian perfect group is trivial. Thus $M = Q$ , contrary to properness. Only the first case remains.

F1F2F3algebra

2.1

Fix $t \in T$ . Since $t$ normalizes $P$ , the formula $c_{t} (p) = t p t^{- 1} p^{- 1}$ defines a function $P \to Z (P)$ by hypothesis. Its values are central, so $t (p q) t^{- 1} = c_{t} (p) p c_{t} (q) q = c_{t} (p) c_{t} (q) p q$ and therefore $c_{t} (p q) = c_{t} (p) c_{t} (q)$ . Thus $c_{t}$ is a homomorphism to the abelian group $Z (P)$ . It kills every commutator of $P$ , and $P = [P, P]$ , so $c_{t}$ is trivial. Every $t$ consequently commutes with every $p$ , as claimed. The argument also covers a trivial center or a trivial $T$ .

F3givenalgebra∎

Depends on

Used by

Dependency tree · two levels

11 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.