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.
PSL(2,7) is a nonabelian simple group of order 168
Statement
The explicitly constructed group is nonabelian, simple, and has order . This proof uses no classification theorem and no choice principle.
Facts & Assumptions
Arithmetic modulo is a commutative ring by For every natural , is an abelian group, multiplication is a commutative monoid operation, and both distributive laws hold. Its nonzero elements have respective inverses , so it is the field . Matrix multiplication is associative and unital by Matrix multiplication is associative, unital, distributive, and compatible with scalar multiplication.
Quotients by normal subgroups have the coset multiplication and group laws (The quotient group and coset product , For , the cosets form a group with identity and inverse ); simplicity means nontriviality and absence of nontrivial proper normal subgroups (Normal subgroup: invariance under conjugation, Simple groups).
Commutators are and generate the normal subgroup (Commutators and the commutator subgroup , The commutator subgroup is normal). An abelian quotient forces ( is abelian if and only if ).
A group action assigns compatible permutations to its elements (Left group actions, transitive actions, and faithful actions).
Given: The field and matrix arithmetic of F1. Define to be the two-by-two matrices over with .
Proof
Direct expansion of a product shows that the determinant of the product of two such matrices is the product of their determinants. Their inverses are ; together with F1 this makes a group. Its first column can be any of the nonzero vectors. For first column with , there are exactly seven second columns: is arbitrary and ; for one has , , and arbitrary. Thus . The central subgroup has two elements; its cosets pair each matrix with its negative, so has order .
Write , , , and for . Multiplication gives and . These upper and lower matrices generate : if the top left entry of is nonzero, then ; if it is zero, left multiplication by makes it nonzero, since . Every displayed factor is generated by the and , proving the assertion.
In , since in . As multiplication by permutes the field, every is a commutator. Also , so normality of the commutator subgroup puts every in it. Step 2.1 gives . The same calculations after quotienting, and the images of the same generators, give . Since , cannot be abelian: all commutators in an abelian group are the identity.
Let be the one-dimensional subspaces of , written and for . The matrices in permute these lines, and fixes them, giving an action of on these eight points. It is faithful: a matrix fixing all lines fixes and , hence is diagonal; fixing makes its two diagonal entries equal, and determinant one then makes the matrix or . The action is transitive because sends to and translates to . The stabilizer of contains all these translations and is transitive on the other seven points. Thus the action is two-transitive: first move one entry of an ordered pair to its target, then use the target stabilizer to move the other entry.
If , its orbits form a -invariant equivalence relation on , since . Under two-transitivity any equivalent pair of distinct points makes every pair of distinct points equivalent, by transporting that ordered pair. Thus either all -orbits are singletons, or is transitive. In the singleton case faithfulness forces . If , then is transitive and : for any take with and then .
Let be the image of in . It is abelian, since . Every matrix representing a member of is upper triangular, of the form ; it conjugates to , so . The conjugates of generate , since they include the images of all and by step 3.1 and these generate by step 2.1. For nontrivial normal , let be the quotient map. By step 4.1 any is with , , and therefore . Hence , generated by the images of these conjugates, equals the abelian subgroup . F3 and step 3.1 imply , so . With step 1.1 this proves simplicity, order , and nonabelianness. All sets and selections used are finite.
Depends on
- For every natural $n$, $(\mathbb{Z}/n,+)$ is an abelian group, multiplication is a commutative monoid operation, and both distributive laws hold
- Matrix multiplication is associative, unital, distributive, and compatible with scalar multiplication
- The quotient group $G/N$ and coset product $(gN)(hN)=ghN$
- For $N\mathrel{\trianglelefteq}G$, the cosets form a group with identity $N$ and inverse $(gN)^{-1}=g^{-1}N$
- Normal subgroup: invariance under conjugation
- Simple groups
- Left group actions, transitive actions, and faithful actions
- Commutators $[g,h]=ghg^{-1}h^{-1}$ and the commutator subgroup $[G,G]$
- The commutator subgroup is normal
- $G/N$ is abelian if and only if $[G,G]\subseteq N$
Used by
- All finite simple groups are alternating or cyclic False statement
Dependency tree · two levels
25 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.
Sources
- Stephen D. Smith, CFSG—A User’s Manual (family entry; elementary simplicity argument supplied locally) (standard reference, not scraped)