The monoidal skein category

The MonoidalCategory instance on SkeinObj f: the interchange on classes, the identity-strand tensor, the naturality squares, and the coherence diagrams, all collapsing through the bundle-map calculus.

theorem RS.tensorMapEquiv_finCongr {n₁ m₁ n₂ m₂ : ℕ} (h₁ : n₁ = m₁) (h₂ : n₂ = m₂) : tensorMapEquiv (finCongr h₁) (finCongr h₂) = finCongr ⋯

Block sums of casts are casts.

theorem RS.tensorMapEquiv_finCongr_refl_right {n₁ m₁ : ℕ} (h₁ : n₁ = m₁) (k : ℕ) : tensorMapEquiv (finCongr h₁) (Equiv.refl (Fin k)) = finCongr ⋯

Tensoring an arity cast with the identity is again a cast.

theorem RS.tensorMapEquiv_refl_finCongr_left (k : ℕ) {n₂ m₂ : ℕ} (h₂ : n₂ = m₂) : tensorMapEquiv (Equiv.refl (Fin k)) (finCongr h₂) = finCongr ⋯

And so is tensoring the identity with one.

@[instance_reducible]

noncomputable instance RS.skeinMonoidal {R : ℕ} (f : EdgeRankParameter R) : CategoryTheory.MonoidalCategory (SkeinObj f)

The monoidal skein category.

Equations

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