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.
Orthogonal and unitary operators form groups, and their determinants have modulus one
Statement
The orthogonal operators on a finite-dimensional real inner product space form a group under composition, as do the unitary operators on a finite-dimensional complex inner product space. Every such operator satisfies
Over , this says . In dimension zero, the unique determinant is .
Facts & Assumptions
Given: Orthogonal or unitary operators on a fixed finite-dimensional inner product space.
Adjoints reverse products and fix the identity (Adjoints satisfy , , , and ).
In an orthonormal basis, the matrix of is the conjugate transpose of the matrix of (In orthonormal bases, the matrix of the adjoint is the conjugate transpose of the matrix).
For the operator determinant is independent of the ordered basis, in dimension zero it is the separately defined value , and (The determinant of a linear operator is independent of the chosen ordered basis, For endomorphisms and of one finite-dimensional vector space, ).
For and over a commutative ring, ; complex conjugation is a field automorphism, and (For every square matrix over a commutative ring, , Conjugation is an involutive real-field automorphism, , and modulus is definite, multiplicative, and subadditive).
Every finite-dimensional real or complex inner product space has an orthonormal basis, the empty one in dimension zero (Every finite-dimensional real or complex inner product space has an orthonormal basis).
Proof
The identity satisfies [L1]. If satisfy it, then [L2] gives ; and the inverse also satisfies the same identities. Hence the operators are closed under identity, composition, and inverses, so form a group.
Suppose and choose an orthonormal basis by [L6]; write for the matrix of in it. By [L3] the matrix of is , and since conjugation is a field automorphism it conjugates the determinant, so [L5] gives . Hence [L4] makes . Taking determinants in , where has matrix and so determinant , [L4] gives , so [L5] yields .
Over , the only real scalars of modulus one are and . If , then [L4] gives the operator determinant , so holds there as well, and the group has its single identity element.
Depends on
- For an endomorphism in finite dimension, preserving lengths, preserving inner products, carrying orthonormal bases to orthonormal bases, and $T^*T=I$ are equivalent
- Adjoints satisfy $(S+T)^*=S^*+T^*$, $(\lambda T)^*=\overline\lambda T^*$, $(ST)^*=T^*S^*$, and $T^{**}=T$
- In orthonormal bases, the matrix of the adjoint is the conjugate transpose of the matrix
- The determinant of a linear operator is independent of the chosen ordered basis
- For endomorphisms $S$ and $T$ of one finite-dimensional vector space, $\det(ST)=\det(S)\det(T)$
- For every square matrix over a commutative ring, $\det(A^{\mathsf T})=\det(A)$
- Conjugation is an involutive real-field automorphism, $z\overline z=|z|^2$, and modulus is definite, multiplicative, and subadditive
- Every finite-dimensional real or complex inner product space has an orthonormal basis
Used by
- Lebesgue measure on ℝⁿ is invariant under every orthogonal linear map Corollary
- Polar integration may discard the cut locus Corollary
- The oriented unit volume form Definition
- Newtonian potential of radial compact data Example
- Spectral and Frobenius norms are unitarily invariant, are given by singular values, and satisfy the sharp rank comparison Theorem
Dependency tree · two levels
33 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
- Sheldon Axler, Linear Algebra Done Right, 4th ed., §7D (standard reference, not scraped)