The tensor product of fragments

The monoidal product of the skein category on representatives: the tensor of an (s, t)-fragment and a (u, v)-fragment is their disjoint union with interleaved boundary — the two low blocks side by side, then the two high blocks (interleaveEquiv). The four value lemmas locate each block of the interleaving, and tensorFragmentCongr shows the tensor respects fragment equivalence in both slots.

def RS.interleaveEquiv (s t u v : ℕ) : Fin (s + t) ⊕ Fin (u + v) ≃ Fin (s + u + (t + v))

The interleaving of two (low, high) boundaries: low block of the first, low block of the second, high block of the first, high block of the second.

Equations

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

theorem RS.interleaveEquiv_inl_low (s t u v : ℕ) (i : Fin s) : (interleaveEquiv s t u v) (Sum.inl (Fin.castAdd t i)) = Fin.castAdd (t + v) (Fin.castAdd u i)

The low block of the first factor sits first.

theorem RS.interleaveEquiv_inr_low (s t u v : ℕ) (j : Fin u) : (interleaveEquiv s t u v) (Sum.inr (Fin.castAdd v j)) = Fin.castAdd (t + v) (Fin.natAdd s j)

The low block of the second factor sits second.

theorem RS.interleaveEquiv_inl_high (s t u v : ℕ) (k : Fin t) : (interleaveEquiv s t u v) (Sum.inl (Fin.natAdd s k)) = Fin.natAdd (s + u) (Fin.castAdd v k)

The high block of the first factor sits third.

theorem RS.interleaveEquiv_inr_high (s t u v : ℕ) (l : Fin v) : (interleaveEquiv s t u v) (Sum.inr (Fin.natAdd u l)) = Fin.natAdd (s + u) (Fin.natAdd t l)

The high block of the second factor sits last.

theorem RS.interleaveEquiv_symm_low_left (s t u v : ℕ) (i : Fin s) : (interleaveEquiv s t u v).symm (Fin.castAdd (t + v) (Fin.castAdd u i)) = Sum.inl (Fin.castAdd t i)

The inverse interleaving on the first block.

theorem RS.interleaveEquiv_symm_low_right (s t u v : ℕ) (j : Fin u) : (interleaveEquiv s t u v).symm (Fin.castAdd (t + v) (Fin.natAdd s j)) = Sum.inr (Fin.castAdd v j)

The inverse interleaving on the second block.

theorem RS.interleaveEquiv_symm_high_left (s t u v : ℕ) (k : Fin t) : (interleaveEquiv s t u v).symm (Fin.natAdd (s + u) (Fin.castAdd v k)) = Sum.inl (Fin.natAdd s k)

The inverse interleaving on the third block.

theorem RS.interleaveEquiv_symm_high_right (s t u v : ℕ) (l : Fin v) : (interleaveEquiv s t u v).symm (Fin.natAdd (s + u) (Fin.natAdd t l)) = Sum.inr (Fin.natAdd u l)

The inverse interleaving on the last block.

noncomputable def RS.tensorFragment {s t u v : ℕ} (x : Fragment (Fin (s + t))) (z : Fragment (Fin (u + v))) : Fragment (Fin (s + u + (t + v)))

The tensor product of fragments: disjoint union with interleaved boundary.

Equations

• RS.tensorFragment x z = (x.disjUnion z).relabel (RS.interleaveEquiv s t u v)

noncomputable def RS.tensorFragmentCongr {s t u v : ℕ} {x₁ x₂ : Fragment (Fin (s + t))} {z₁ z₂ : Fragment (Fin (u + v))} (hx : x₁.Equiv x₂) (hz : z₁.Equiv z₂) : (tensorFragment x₁ z₁).Equiv (tensorFragment x₂ z₂)

The tensor respects fragment equivalence in both slots.

Equations

• RS.tensorFragmentCongr hx hz = (hx.disjUnionCongr hz).relabelCongr (RS.interleaveEquiv s t u v)