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.
Partition-diagram orbit basis and symmetric-group centralizer
Statement
Let be any field, , and , with the integer also denoting its scalar image in . Let have basis , and let act by permuting this basis and diagonally on . For a set partition diagram on the boundary labels, define when all indices attached to vertices in each block of are equal, and otherwise; extend linearly. The partition algebra from Typed Brauer and partition diagram categories acts by , and its image is , the algebra of linear maps commuting with this action. Order set partitions by refinement: means is a coarsening of . Let be the inverse of the finite integer incidence matrix , and view these integers as scalars in . Set . Then is the indicator matrix of the exact equality pattern when has at most blocks, and is zero when has more than blocks. Consequently is the span of those with more than blocks, and is injective exactly when . These statements hold even when divides .
Facts & Assumptions
Given: The partition-diagram composition from Typed Brauer and partition diagram categories and its associativity in Associativity of Brauer and partition diagram composition.
Typed Brauer and partition diagram categories: a partition diagram has one block for each set of boundary vertices and composition identifies the middle boundary blocks, weighting each removed component by .
Associativity of Brauer and partition diagram composition: this composition is associative.
Proof
Given: , , and the permutation action on the tensor basis of .
For basis tuples on the external boundary, the matrix coefficient of is the sum over middle tuples of . The equalities imposed by the two diagrams generate exactly the blocks of the stacked partition. Each generated block meeting an outer label has its index fixed by that label; each block wholly in the middle has independent choices. Hence the coefficient is when the outer labels satisfy the stacked partition and zero otherwise, where is the number of removed middle blocks. By [F1] this equals the coefficient of , so respects multiplication; [F2] supplies associativity of the domain algebra.
Index a tensor basis vector by an -tuple . A matrix coefficient of an operator is indexed by a pair . The operator commutes with all basis permutations exactly when its matrix coefficient is constant on simultaneous -orbits of . Two such pairs lie in the same orbit exactly when they have the same equality pattern on the labels: a permutation maps one pair to the other if and only if it maps their distinct used indices block by block. Thus orbit indicator matrices form a basis of the commutant over every field.
For a partition diagram , the matrix coefficient of is exactly when labels joined by a block of receive equal indices. It is therefore the sum of orbit indicators over exact equality patterns coarser than and having at most blocks. The finite-poset zeta matrix is triangular with diagonal entries one, so its inverse gives an invertible change of basis from the diagram basis to the elements . Möbius inversion therefore gives if is realizable and otherwise.
An exact pattern is realizable precisely when it has at most blocks, since one can assign distinct indices to its blocks. Its orbit indicator is then nonzero, and different exact patterns have disjoint supports, so these images are linearly independent. Step 2.1 shows they span the image and that every with more than blocks maps to zero; hence the kernel and image have the stated forms. The full diagram basis is independent in the image exactly when every partition of labels has at most blocks, which is equivalent to . No division by was used, so the argument is valid in every characteristic.
Depends on
Used by
Dependency tree · one level
2 results within one dependency step 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
- Halverson and Ram, Partition Algebras, Theorem 3.6(a) and proof (standard reference, not scraped)