Tensor Symmetry
Exercise PLAN-313
primary source nl only. Current content-bound mathematical second pass accepted. No new Lean verification is claimed for this NL view.
Assumptions and conventions
- Permutations act on a fixed finite set; every permutation has a disjoint cycle decomposition.
- Cycle type is the multiset of cycle lengths in non-increasing order.
Question
Two permutations in the symmetric group are conjugate if and only if they have the same cycle type. Prove the key computational identity that conjugating a single cycle by an arbitrary permutation sigma relabels its entries by sigma, and use it to establish both directions of the conjugacy criterion.
Hint: mathematical route
Permutations are conjugate exactly when they share a cycle type, proved via the identity that conjugation relabels cycle entries by the conjugating permutation.
- Conjugating a cycle by sigma produces the cycle on the sigma-images of its entries.
- Conjugating a disjoint-cycle product preserves all cycle lengths, so cycle type is a conjugacy invariant.
- Matching equal-length cycles entrywise defines a permutation sigma relating two same-type permutations.
- This sigma conjugates one permutation to the other, giving the converse.
Reference solution
Key identity: let a cycle send each listed entry to the next and the last back to the first, and let sigma be any permutation. The conjugate sigma times cycle times sigma inverse acts on sigma applied to a listed entry by first undoing sigma, then applying the cycle to move to the next listed entry, then applying sigma; the net effect sends sigma of an entry to sigma of the next entry, and fixes everything outside the sigma-image of the listed entries. Thus the conjugate is again a cycle of the same length whose entries are the sigma-images of the original entries. Forward direction: write any permutation as a product of disjoint cycles. Conjugating the whole product by sigma conjugates each cycle, replacing its entries by their sigma-images while preserving all cycle lengths and keeping the cycles disjoint (sigma is a bijection). Hence the conjugate has the same multiset of cycle lengths, i.e. the same cycle type. Converse: given two permutations with the same cycle type, align their disjoint-cycle decompositions so that cycles of equal length are paired, and define sigma to map the entries of each cycle of the first permutation, in order, to the entries of the paired cycle of the second. This sigma is a well-defined permutation because the cycle decompositions partition the ground set, and by the key identity it conjugates the first permutation to the second. Therefore same cycle type is equivalent to conjugacy.
Assessment rubric
- Proves the identity that conjugating a cycle by sigma yields the cycle with entries replaced by their sigma-images (1 weight)
- Uses disjoint cycle decomposition to show conjugation preserves the multiset of cycle lengths (forward direction) (1 weight)
- Constructs an explicit sigma matching cycle decompositions entrywise for two permutations of equal cycle type (converse) (1 weight)
- Verifies this sigma is a well-defined permutation and conjugates one to the other, completing the equivalence (1 weight)
Graph-grounded prerequisites
These are support/source anchors, not an automatically extracted theorem-dependency proof.
- Operator and semigroup theory (frozen curriculum anchor; see graph registry)
- Probability and sampling (frozen curriculum anchor; see graph registry)
Lean view and evidence boundary
No aligned Lean view has been admitted for this native core in this textbook checkpoint. This is not a claim that the underlying mathematics lacks a formal proof. Contributions must preserve this exact target contract and split.
Sources and provenance
- website/research/sources.json
leditzky-2025-repth-qit
Source SHA-256:9f85f45f20ed5a46931ad0dec3b94ee09748bc56e39fae29b0aefe910440b0ae· MIT metadata only - Primary source
Contract: 2d4106fd43cadedb07d0af9c27a52dca681336a0e27274c025961e5ef5a2f519
Item digest: 2aa47cab42159b2c4d10c188b1f176c3bf6fa3799aff9b9f0e347853a9f92974
Graph snapshot: qcb-snapshot-ffa644f0da3031a1ce754b9a
Authored support steps: 4. This is not measured graph distance or model difficulty.