Merging monoidal powers

The block merge of two monoidal powers into the power of the sum (right unitor base, associator-threaded step), and its compatibility with the model transport: transporting blockwise and merging through the structure map agrees with merging first.

noncomputable def RS.powMerge (V : SuperVect) (a b : ℕ) : CategoryTheory.MonoidalCategoryStruct.tensorObj (superPow V a) (superPow V b) ⟶ superPow V (a + b)

The block merge of monoidal powers.

Equations

• One or more equations did not get rendered due to their size.
• RS.powMerge V x✝ 0 = (CategoryTheory.MonoidalCategoryStruct.rightUnitor (RS.superPow V x✝)).hom

theorem RS.stdToOmega_merge {R : ℕ} (f : EdgeRankParameter R) (P : DelignePackage (SkeinObj f)) {k ℓ : ℕ} (e : stdSuperPair k ℓ ⟶ P.ω.obj { arity := 1 }) (a b : ℕ) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom (stdToOmega f P e a) (stdToOmega f P e b)) (CategoryTheory.Functor.LaxMonoidal.μ P.ω { arity := a } { arity := b }) = CategoryTheory.CategoryStruct.comp (powMerge (stdSuperPair k ℓ) a b) (stdToOmega f P e (a + b))

The block transport: blockwise transports assembled by the structure map agree with the merged transport.