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.
Path-connectedness of SL(2,C)
Statement
For a complex matrix , write . On use and , and set . Give its Euclidean topology as , and define with matrix multiplication. Then is path-connected.
Statement references
Facts & Assumptions
Given: A matrix .
The determinant is multiplicative for square matrices over (For same-sized finite square matrices over a commutative ring, ).
The determinant is defined by a finite alternating sum of products of matrix entries; for a conjugate-transpose matrix, the Leibniz formula gives (For , the determinant over a commutative ring by the Leibniz formula, and for a real matrix).
Proof
Write the columns of as . Since , and are linearly independent. Put , , , , and . Then and makes unitary; with we have . By [F1]–[F2], , and then gives . Therefore and for and .
If the first column of is , its unit orthogonal vectors are with . The determinant of the matrix with these columns is ; therefore forces . Thus and . This identifies with the unit sphere . Under this identification use the standard Euclidean inner product and norm on . The sphere is path-connected: non-antipodal points are joined by normalizing their straight segment. For antipodal points , at least one of the first two standard basis vectors is not parallel to ; choose such an and set The denominator is nonzero because is not parallel to ; hence and . The normalized straight segments from to and from to give a path. Hence there is a continuous path in from to .
For , the path has continuous entries because for the fixed , and the real exponential is continuous. It has determinant one for every , with and . Thus is a continuous path in from to . Since was arbitrary, is path-connected.