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.
The sign is a homomorphism , surjective exactly when
Statement
For every natural , the function is a group homomorphism. It is surjective exactly when ; for and its image is .
Facts & Assumptions
Given: A natural and permutations .
Every finite permutation has a transposition factorisation, the sign is , and every such factorisation has that parity (Every finite permutation is a product of transpositions, so the transpositions generate , Inversions, inversion number, the sign , and even and odd permutations, Every transposition factorisation of has parity ).
Proof
Choose transposition factorisations and . Their concatenation is a transposition factorisation in the library's composition order.
By [L1], , and the identity has sign ; hence sign is a group homomorphism.
If , the transposition belongs to and has sign , while the identity has sign , so sign is surjective. If or , contains only the identity and the image is .
Depends on
- Inversions, inversion number, the sign $\operatorname{sgn}(\sigma)=(-1)^{\operatorname{inv}(\sigma)}$, and even and odd permutations
- Every transposition factorisation of $\sigma$ has parity $(-1)^{\operatorname{inv}(\sigma)}$
- Every finite permutation is a product of transpositions, so the transpositions generate $S_n$
- Monoid homomorphism and group homomorphism
- The integers form a commutative ring
Used by
- A k-cycle has sign (-1)ᵏ⁻¹, and sgn(σ)=(-1)^n-c(σ) when fixed points are counted as cycles Corollary
- Aₙ is normal in Sₙ; for n≥2, 2 |Aₙ|=n!, while Aₙ=Sₙ for n=0,1 Corollary
- For n≥2, sign is the unique nontrivial homomorphism Sₙ→{+1,-1} Corollary
- The alternating group Aₙ=ker(sgn) of even permutations Definition
- Every alternating multilinear F satisfies F(A)=F(I)∑_σ∈ Sₙsgn(σ)∏ᵢ a_σ(i),i Lemma
- For every square matrix over a commutative ring, det(A^mathsf T)=det(A) Theorem
- The Leibniz determinant is column-multilinear, alternating and normalized over every commutative ring Theorem
Dependency tree · next 3 levels
Direct dependencies and their dependencies through the next three levels: 56 results over 18 levels. An arrow runs from a result to what uses it, and this result sits at the bottom with a heavier outline. Click the chart to enlarge it.
Sources
- J. S. Milne, Group Theory, §4, the sign homomorphism (standard reference, not scraped)
- Stanford Math 51H, Permutations (standard reference, not scraped)