Units of the fragment tensor

Tensoring with the empty closed fragment is a relabel by the arithmetic cast, on either side. These power the unitors of the monoidal skein category.

theorem RS.interleave_unit_left (s t : ℕ) (ℓ : Fin (s + t)) : (interleaveEquiv 0 0 s t) (Sum.inr ℓ) = (finCongr ⋯) ℓ

The interleave against an empty left factor is the cast.

theorem RS.interleave_unit_right (s t : ℕ) (ℓ : Fin (s + t)) : (interleaveEquiv s t 0 0) (Sum.inl ℓ) = (finCongr ⋯) ℓ

The interleave against an empty right factor is the cast.

noncomputable def RS.tensorFragmentUnitLeft {s t : ℕ} (X : Fragment (Fin (s + t))) : (tensorFragment emptyClosedFragment X).Equiv (X.relabel (finCongr ⋯))

The left unit: the empty fragment tensors away.

Equations

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

noncomputable def RS.tensorFragmentUnitRight {s t : ℕ} (X : Fragment (Fin (s + t))) : (tensorFragment X emptyClosedFragment).Equiv (X.relabel (finCongr ⋯))

The right unit: the empty fragment tensors away.

Equations

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