The monoidal structure data of the skein category

Tensor on objects is arity addition, tensor on morphisms is the descended tensor, and every structural isomorphism — associator, unitors — is the class of a cast bundle map. The iso laws and the coherence lemmas provable without the interchange law (identity tensoring, pentagon, triangle) all collapse through the bundle-map calculus.

noncomputable def RS.castIso {R : ℕ} (f : EdgeRankParameter R) {n m : ℕ} (h : n = m) : { arity := n } ≅ { arity := m }

The cast isomorphism between equal-arity objects.

Equations

• RS.castIso f h = { hom := RS.bundleMapClass f (finCongr h), inv := RS.bundleMapClass f (finCongr ⋯), hom_inv_id := ⋯, inv_hom_id := ⋯ }

@[instance_reducible]

noncomputable instance RS.skeinMonoidalStruct {R : ℕ} (f : EdgeRankParameter R) : CategoryTheory.MonoidalCategoryStruct (SkeinObj f)

The monoidal structure of the skein category.

Equations

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

theorem RS.bundleMapClass_tensor {R : ℕ} (f : EdgeRankParameter R) {n₁ m₁ n₂ m₂ : ℕ} (e₁ : Fin n₁ ≃ Fin m₁) (e₂ : Fin n₂ ≃ Fin m₂) : ((HomSpace.tensor f n₁ m₁ n₂ m₂) (bundleMapClass f e₁)) (bundleMapClass f e₂) = bundleMapClass f (tensorMapEquiv e₁ e₂)

Tensoring bundle-map classes is the class of the block sum.

theorem RS.skein_tensor_id {R : ℕ} (f : EdgeRankParameter R) (X Y : SkeinObj f) : CategoryTheory.MonoidalCategoryStruct.tensorHom (CategoryTheory.CategoryStruct.id X) (CategoryTheory.CategoryStruct.id Y) = CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y)

Tensoring identities is the identity (tensor_id).

theorem RS.id_eq_bundleMapClass {R : ℕ} (f : EdgeRankParameter R) (n : ℕ) : HomSpace.ofFragment f.val (strandBundle n) = bundleMapClass f (Equiv.refl (Fin n))

The identity class is a bundle-map class.

theorem RS.bundleMapClass_tensor_id_right {R : ℕ} (f : EdgeRankParameter R) {n₁ m₁ : ℕ} (k : ℕ) (e₁ : Fin n₁ ≃ Fin m₁) : ((HomSpace.tensor f n₁ m₁ k k) (bundleMapClass f e₁)) (HomSpace.ofFragment f.val (strandBundle k)) = bundleMapClass f (tensorMapEquiv e₁ (Equiv.refl (Fin k)))

Tensoring a bundle-map class with an identity strand on the right.

theorem RS.bundleMapClass_tensor_id_left {R : ℕ} (f : EdgeRankParameter R) (k : ℕ) {n₂ m₂ : ℕ} (e₂ : Fin n₂ ≃ Fin m₂) : ((HomSpace.tensor f k k n₂ m₂) (HomSpace.ofFragment f.val (strandBundle k))) (bundleMapClass f e₂) = bundleMapClass f (tensorMapEquiv (Equiv.refl (Fin k)) e₂)

Tensoring a bundle-map class with an identity strand on the left.

theorem RS.transposeEquiv_trans_self (a b : ℕ) : (transposeEquiv a b).trans (transposeEquiv b a) = Equiv.refl (Fin (a + b))

The block transposes compose to the identity.

noncomputable def RS.skeinBraiding {R : ℕ} (f : EdgeRankParameter R) (X Y : SkeinObj f) : CategoryTheory.MonoidalCategoryStruct.tensorObj X Y ≅ CategoryTheory.MonoidalCategoryStruct.tensorObj Y X

The braiding isomorphism of the skein category: the block-transpose bundle map.

Equations

• RS.skeinBraiding f X Y = { hom := RS.bundleMapClass f (RS.transposeEquiv X.arity Y.arity), inv := RS.bundleMapClass f (RS.transposeEquiv Y.arity X.arity), hom_inv_id := ⋯, inv_hom_id := ⋯ }

theorem RS.skeinBraiding_symmetry {R : ℕ} (f : EdgeRankParameter R) (X Y : SkeinObj f) : CategoryTheory.CategoryStruct.comp (skeinBraiding f X Y).hom (skeinBraiding f Y X).hom = CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y)

The braiding is symmetric: swapping twice is the identity (the symmetry axiom, at class level).