Braiding naturality, fragment level

Value lemmas for the tensor swap, the braiding-naturality label meets, and the fragment-level naturality squares.

Values of the tensor swap

theorem RS.tensorSwapEquiv_in_left (s t u v : ℕ) (i : Fin u) : (tensorSwapEquiv s t u v) (Fin.castAdd (v + t) (Fin.castAdd s i)) = Fin.castAdd (t + v) (Fin.natAdd s i)

The tensor swap on an incoming label of the left factor.

theorem RS.tensorSwapEquiv_in_right (s t u v : ℕ) (j : Fin s) : (tensorSwapEquiv s t u v) (Fin.castAdd (v + t) (Fin.natAdd u j)) = Fin.castAdd (t + v) (Fin.castAdd u j)

On an incoming label of the right factor.

theorem RS.tensorSwapEquiv_out_left (s t u v : ℕ) (l : Fin v) : (tensorSwapEquiv s t u v) (Fin.natAdd (u + s) (Fin.castAdd t l)) = Fin.natAdd (s + u) (Fin.natAdd t l)

On an outgoing label of the left factor.

theorem RS.tensorSwapEquiv_out_right (s t u v : ℕ) (m : Fin t) : (tensorSwapEquiv s t u v) (Fin.natAdd (u + s) (Fin.natAdd v m)) = Fin.natAdd (s + u) (Fin.castAdd v m)

On an outgoing label of the right factor.

The left naturality label meet

theorem RS.braidNatLeft_label (s t k : ℕ) : (tensorSwapEquiv s t k k).trans (finSumFinEquiv.symm.trans (((Equiv.refl (Fin (s + k))).sumCongr (transposeEquiv t k)).trans finSumFinEquiv)) = finSumFinEquiv.symm.trans (((transposeEquiv s k).symm.sumCongr (Equiv.refl (Fin (k + t)))).trans finSumFinEquiv)

The left naturality square meets on labels: swapping then braiding the right leg relabels the same way as braiding the left leg then swapping.

noncomputable def RS.braidNatLeftFrag {s t : ℕ} (k : ℕ) (F : Fragment (Fin (s + t))) : ((tensorFragment F (strandBundle k)).compose (bundleMap (transposeEquiv t k))).Equiv ((bundleMap (transposeEquiv s k)).compose (tensorFragment (strandBundle k) F))

The left braiding-naturality square, fragment level.

Equations

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

The right naturality label meet

theorem RS.braidNatRight_label (s t k : ℕ) : (tensorSwapEquiv k k s t).trans (finSumFinEquiv.symm.trans (((Equiv.refl (Fin (k + s))).sumCongr (transposeEquiv k t)).trans finSumFinEquiv)) = finSumFinEquiv.symm.trans (((transposeEquiv k s).symm.sumCongr (Equiv.refl (Fin (t + k)))).trans finSumFinEquiv)

The mirrored square, braiding on the other side.

noncomputable def RS.braidNatRightFrag {s t : ℕ} (k : ℕ) (F : Fragment (Fin (s + t))) : ((tensorFragment (strandBundle k) F).compose (bundleMap (transposeEquiv k t))).Equiv ((bundleMap (transposeEquiv k s)).compose (tensorFragment F (strandBundle k)))

The right braiding-naturality square, fragment level.

Equations

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