Rigidity of the skein category

Every object is self-dual: the exact self-pairing at arity n is assembled by induction from the single-strand pairing, using the unit pairing at arity zero and the tensor product of exact pairings for the step (the arity arithmetic n + 1 is definitional, and the flip 1 + n = n + 1 is transported along eqToIso).

@[instance_reducible]

noncomputable def RS.strandPairingAll {R : ℕ} (f : EdgeRankParameter R) (n : ℕ) : CategoryTheory.ExactPairing { arity := n } { arity := n }

The exact self-pairing at every arity.

Equations

• RS.strandPairingAll f 0 = CategoryTheory.exactPairingUnit
• RS.strandPairingAll f n.succ = CategoryTheory.exactPairingCongrRight (CategoryTheory.eqToIso ⋯)

@[instance_reducible]

noncomputable instance RS.skeinHasRightDual {R : ℕ} (f : EdgeRankParameter R) (X : SkeinObj f) : CategoryTheory.HasRightDual X

Every skein object is its own right dual.

Equations

• RS.skeinHasRightDual f X = { rightDual := X, exact := RS.strandPairingAll f X.arity }

@[instance_reducible]

noncomputable instance RS.skeinHasLeftDual {R : ℕ} (f : EdgeRankParameter R) (X : SkeinObj f) : CategoryTheory.HasLeftDual X

And its own left dual — the category is rigid.

Equations

• RS.skeinHasLeftDual f X = { leftDual := X, exact := RS.strandPairingAll f X.arity }

@[instance_reducible]

noncomputable instance RS.skeinRigid {R : ℕ} (f : EdgeRankParameter R) : CategoryTheory.RigidCategory (SkeinObj f)

The skein category is rigid.

Equations

• RS.skeinRigid f = { rightDual := RS.skeinHasRightDual f, leftDual := RS.skeinHasLeftDual f }