Strand bundles

The identity fragments of the skein category: strandBundle t is the disjoint union of t parallel strands, with strand k joining boundary label k to boundary label t + k. Flags are pairs (k, b) with b = false at the incoming end (label k) and b = true at the outgoing end (label t + k).

def RS.strandBundle (t : ℕ) : Fragment (Fin (t + t))

The bundle of t parallel strands: strand k joins label k to label t + k.

Equations

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

theorem RS.strandBundle_boundaryFlag_low (t : ℕ) (ℓ : Fin (t + t)) (h : ↑ℓ < t) : (strandBundle t).boundaryFlag ℓ = (⟨↑ℓ, h⟩, false)

The boundary flag of an incoming label.

theorem RS.strandBundle_boundaryFlag_high (t : ℕ) (ℓ : Fin (t + t)) (h : ¬↑ℓ < t) : (strandBundle t).boundaryFlag ℓ = (⟨↑ℓ - t, ⋯⟩, true)

The boundary flag of an outgoing label.