The strand bundle is a tensor of strand bundles

strandBundle (a + b) ≃ strandBundle a ⊗ strandBundle b: the first a strands form the first factor, the rest the second. This is the object-level compatibility of the identity fragments with the monoidal product, the entry point for the trace multiplicativity (Lemma 3.5(b)).

def RS.bundleFlagEquiv (a b : ℕ) : Fin (a + b) × Bool ≃ Fin a × Bool ⊕ Fin b × Bool

The strand split: strands below a to the left factor, strands above to the right.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def RS.strandBundleTensor (a b : ℕ) : (strandBundle (a + b)).Equiv (tensorFragment (strandBundle a) (strandBundle b))

The bundle splits: the (a + b)-strand bundle is the tensor of the a- and b-strand bundles.

Equations

• One or more equations did not get rendered due to their size.