The symmetric skein category #
Kernel descents of the braiding-naturality squares, the hexagon
label identities, and the BraidedCategory/SymmetricCategory
instances on SkeinObj f.
theorem
RS.mem_ker_braidNatLeft
{R : ℕ}
(f : EdgeRankParameter R)
{s t : ℕ}
(k : ℕ)
(x : Fragment (Fin (s + t)) →₀ ℂ)
:
((composeFinsupp (s + k) (t + k) (k + t)) (((tensorFinsupp s t k k) x) (Finsupp.single (strandBundle k) 1)))
(Finsupp.single (bundleMap (transposeEquiv t k)) 1) - ((composeFinsupp (s + k) (k + s) (k + t)) (Finsupp.single (bundleMap (transposeEquiv s k)) 1))
(((tensorFinsupp k k s t) (Finsupp.single (strandBundle k) 1)) x) ∈ (connectionMap f.val (s + k + (k + t))).ker
The left braiding-naturality difference lies in the kernel.
theorem
RS.mem_ker_braidNatRight
{R : ℕ}
(f : EdgeRankParameter R)
{s t : ℕ}
(k : ℕ)
(x : Fragment (Fin (s + t)) →₀ ℂ)
:
((composeFinsupp (k + s) (k + t) (t + k)) (((tensorFinsupp k k s t) (Finsupp.single (strandBundle k) 1)) x))
(Finsupp.single (bundleMap (transposeEquiv k t)) 1) - ((composeFinsupp (k + s) (s + k) (t + k)) (Finsupp.single (bundleMap (transposeEquiv k s)) 1))
(((tensorFinsupp s t k k) x) (Finsupp.single (strandBundle k) 1)) ∈ (connectionMap f.val (k + s + (t + k))).ker
The right braiding-naturality difference lies in the kernel.
theorem
RS.braidNatLeft_class
{R : ℕ}
(f : EdgeRankParameter R)
{s t : ℕ}
(k : ℕ)
(p : HomSpace f.val (s + t))
:
((HomSpace.comp f (s + k) (t + k) (k + t))
(((HomSpace.tensor f s t k k) p) (HomSpace.ofFragment f.val (strandBundle k))))
(bundleMapClass f (transposeEquiv t k)) = ((HomSpace.comp f (s + k) (k + s) (k + t)) (bundleMapClass f (transposeEquiv s k)))
(((HomSpace.tensor f k k s t) (HomSpace.ofFragment f.val (strandBundle k))) p)
Left braiding naturality on Hom classes.
theorem
RS.braidNatRight_class
{R : ℕ}
(f : EdgeRankParameter R)
{s t : ℕ}
(k : ℕ)
(p : HomSpace f.val (s + t))
:
((HomSpace.comp f (k + s) (k + t) (t + k))
(((HomSpace.tensor f k k s t) (HomSpace.ofFragment f.val (strandBundle k))) p))
(bundleMapClass f (transposeEquiv k t)) = ((HomSpace.comp f (k + s) (s + k) (t + k)) (bundleMapClass f (transposeEquiv k s)))
(((HomSpace.tensor f s t k k) p) (HomSpace.ofFragment f.val (strandBundle k)))
Right braiding naturality on Hom classes.
theorem
RS.hexagonF_label
(a b c : ℕ)
:
(finCongr ⋯).trans ((transposeEquiv a (b + c)).trans (finCongr ⋯)) = (tensorMapEquiv (transposeEquiv a b) (Equiv.refl (Fin c))).trans
((finCongr ⋯).trans (tensorMapEquiv (Equiv.refl (Fin b)) (transposeEquiv a c)))
The forward hexagon label identity.
theorem
RS.hexagonR_label
(a b c : ℕ)
:
(finCongr ⋯).trans ((transposeEquiv (a + b) c).trans (finCongr ⋯)) = (tensorMapEquiv (Equiv.refl (Fin a)) (transposeEquiv b c)).trans
((finCongr ⋯).trans (tensorMapEquiv (transposeEquiv a c) (Equiv.refl (Fin b))))
The reverse hexagon label identity.
@[instance_reducible]
The braided skein category.
Equations
- One or more equations did not get rendered due to their size.
@[instance_reducible]
The symmetric skein category.
Equations
- RS.skeinSymmetric f = { toBraidedCategory := RS.skeinBraided f, symmetry := ⋯ }