Permutation fragments

The symmetric-group generators of the skein category: for a permutation σ of Fin t, the fragment permFragment σ consists of t disjoint strands, strand k joining incoming boundary label k to outgoing boundary label t + σ k. The identity permutation gives the strand bundle.

def RS.permFragment {t : ℕ} (σ : Equiv.Perm (Fin t)) : Fragment (Fin (t + t))

The permutation fragment of σ: strand k joins incoming label k to outgoing label t + σ k.

Equations

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

theorem RS.permFragment_one (t : ℕ) : permFragment 1 = strandBundle t

The identity permutation gives the strand bundle.

def RS.permHighEquiv {t : ℕ} (σ : Equiv.Perm (Fin t)) : Fin (t + t) ≃ Fin (t + t)

The label re-indexing that fixes incoming labels and permutes outgoing labels by σ.

Equations

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

noncomputable def RS.permFragmentRelabelBundle {t : ℕ} (σ : Equiv.Perm (Fin t)) : (permFragment σ).Equiv ((strandBundle t).relabel (permHighEquiv σ))

A permutation fragment is the strand bundle with its outgoing labels re-indexed.

Equations

• RS.permFragmentRelabelBundle σ = { flagEquiv := Equiv.refl (RS.permFragment σ).Flag, vertexEquiv := Equiv.refl (RS.permFragment σ).Vertex, attach_comm := ⋯, pairing_comm := ⋯, circles_eq := ⋯ }