Binomial expansion of a tensor power of a biproduct #
(X ⊞ Y) ^ ⊗ n decomposes into 2 ^ n mixed words: for each
w : Fin n → Bool the word power wordPow X Y n w tensors an X
for each true letter and a Y for each false one, in slot
order. The letterwise biproduct inclusions and projections fold to
mixedInto and mixedFrom, which exhibit the word powers as a
biproduct decomposition of the full power: same-word round trips
are identities, different-word round trips vanish, and the sum of
all mixedFrom ≫ mixedInto is the identity of (X ⊞ Y) ^ ⊗ n.
The sorted words are the standardWords — all Xs below all
Ys — whose word power is X ^ ⊗ p ⊗ Y ^ ⊗ q up to the
structural isomorphism standardMixedIso, and on which mixedInto
is the concatenation of the two pure-power inclusions. The sorting
lemma closes the file: every word is a sorted word up to the
symmetric-group action — mixedInto for w, followed by the
action of sortPerm w, is the base-point inclusion at
(popCount w, n − popCount w), up to an isomorphism of the source
and an arity transport eqToHom at the target.
mixedPow in RS/Definitions.lean already names the dual-mixed
power of a rigid object, so the word-indexed power here is called
wordPow instead.
Word powers #
The word power: tensor an X for each true letter of w
and a Y for each false one, by the recursion of tensorPow.
Equations
- RS.wordPow X Y 0 x_2 = CategoryTheory.MonoidalCategoryStruct.tensorUnit A
- RS.wordPow X Y n.succ w = CategoryTheory.MonoidalCategoryStruct.tensorObj (RS.wordPow X Y n (w ∘ Fin.castSucc)) (bif w (Fin.last n) then X else Y)
Instances For
The defining recursion of wordPow: one more letter tensors
the selected object on the right.
Letterwise inclusions and projections #
The biproduct inclusion selected by one letter.
Equations
Instances For
The biproduct projection selected by one letter.
Equations
Instances For
A letter's round trip through the biproduct is the identity.
Different letters' round trips vanish.
The inclusion of a word power into the tensor power of the
biproduct: the fold of the letterwise inclusions, by the recursion
of wordPow.
Equations
- RS.mixedInto X Y 0 x_2 = CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategoryStruct.tensorUnit A)
- RS.mixedInto X Y n.succ w = CategoryTheory.MonoidalCategoryStruct.tensorHom (RS.mixedInto X Y n (w ∘ Fin.castSucc)) (RS.letterInto X Y (w (Fin.last n)))
Instances For
The projection onto a word power from the tensor power of the biproduct: the fold of the letterwise projections.
Equations
- RS.mixedFrom X Y 0 x_2 = CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategoryStruct.tensorUnit A)
- RS.mixedFrom X Y n.succ w = CategoryTheory.MonoidalCategoryStruct.tensorHom (RS.mixedFrom X Y n (w ∘ Fin.castSucc)) (RS.letterFrom X Y (w (Fin.last n)))
Instances For
Round trips #
Each round-trip computation happens factorwise. The helpers are
stated at general objects and applied by exact, so that no
tensor-power arity enters the rewriting.
Completeness #
Summed over all words, the round trips through the word powers
decompose the identity of (X ⊞ Y) ^ ⊗ n. The words of length
n + 1 are reindexed by Fin.snocEquiv as pairs of a last letter
and a shorter word; the letter sum is biprod.total and the word
sum is the inductive hypothesis.
Completeness of the word decomposition: the round trips through the word powers sum to the identity of the full power.
Counting letters and the sorted words #
The sorting permutation of a word: the last slot is routed
below the tail — to the top of the X block when its letter is
true, and kept in place when it is false — and the rest is
sorted recursively. This is the ofSplit decomposition the
tensor-power action recurses on.
Equations
- RS.sortPerm x_2 = 1
- RS.sortPerm w = RS.ofSplit (bif w (Fin.last n) then ⟨RS.popCount (w ∘ Fin.castSucc), ⋯⟩ else Fin.last n) (RS.sortPerm (w ∘ Fin.castSucc))
Instances For
The sorted word: true on the first block of p slots and
false on the last q.
Equations
- RS.standardWord p q i = decide (↑i < p)
Instances For
With an empty second block the sorted word is all true.
Restricting a sorted word drops one false letter.
The last letter of a sorted word with false letters is
false.
The sorted word power #
An all-true word power is a pure power of X.
The sorted word power with empty second block is the pure
power of X.
One more false letter of a sorted word tensors a Y.
The sorted word power is a concatenation of pure powers:
with all Xs below all Ys, the word power reassociates to
X ^ ⊗ p ⊗ Y ^ ⊗ q. Built by the recursion of the word, so that
consumers can compose with it stage by stage.
Equations
- One or more equations did not get rendered due to their size.
- RS.standardMixedIso X Y p 0 = CategoryTheory.eqToIso ⋯ ≪≫ (CategoryTheory.MonoidalCategoryStruct.rightUnitor (RS.tensorPow A X p)).symm
Instances For
The base-point inclusion #
On a sorted word, mixedInto is the concatenation of the two
pure-power inclusions. The gluing helpers are stated at general
objects and applied by exact, so that no tensor-power arity
enters the rewriting.
Transport of mixedInto along an equality of words.
Splitting mixedInto at the last letter, with the recursion's
word and letter replaced by given values.
On an all-true word the inclusion is the pure power of
biprod.inl.
The last-letter split of mixedInto at a false letter, with
the selected object and inclusion spelled as Y and biprod.inr.
The last-letter split of mixedInto at a true letter, with
the selected object and inclusion spelled as X and biprod.inl.
Sorting #
Every word's inclusion is the base-point inclusion of its sorted
form, up to the symmetric-group action. The categorical content is
a single full rotation: bubbling the top factor all the way down is
the braiding against the whole tail, followed by a merge of the new
bottom factor into the concatenation — insertTop_full and
putBelow_concat below.
The recursion of the action, at a split permutation.
Merging a factor at the bottom: the structural morphism
Z ⊗ Z ^ ⊗ m ⟶ Z ^ ⊗ (m + 1), by the recursion of the power.
Equations
- One or more equations did not get rendered due to their size.
- RS.putBelow Z 0 = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.rightUnitor Z).hom (CategoryTheory.MonoidalCategoryStruct.leftUnitor Z).inv
Instances For
The full rotation is a braiding: bubbling the top factor of
Z ^ ⊗ (m + 1) all the way to the bottom is the braiding of the
factor against the whole tail, followed by the bottom merge.
The bottom merge concatenates: merging a factor below the second block and concatenating is reassociating it onto the first block, up to the arity transport.
Sorting one appended X: the base-point inclusion with one
more X in the last slot, bubbled down past the whole Y block,
is the base-point inclusion of the grown X block — up to braiding
the appended factor past the Y power on the mixed side and the
arity transport (p + 1) + m = p + (m + 1) at the target.
The sorting lemma: every mixed inclusion is a permuted
base-point inclusion. For each word w there is an isomorphism of
the word power with X ^ ⊗ popCount w ⊗ Y ^ ⊗ (n − popCount w)
under which mixedInto, followed by the action of sortPerm w, is
the concatenation of the two pure-power inclusions, transported
along popCount w + (n − popCount w) = n at the target.
The sorting isomorphism, chosen once and for all from the
sorting lemma: wordPow X Y n w against the sorted concatenation
of pure powers.
Equations
- RS.sortIso X Y n w = ⋯.choose
Instances For
The sorting square, for the chosen isomorphism sortIso.