The skein trace

The trace of an n-strand endomorphism -- its closure against the strand bundle -- and the one fact the trace calculus needs of it: closing a tensor product multiplies the two closures, proved by bilinear induction down to single fragments.

noncomputable def RS.skeinTrace {R : ℕ} (f : EdgeRankParameter R) (n : ℕ) (g : skeinEnd f n) : ℂ

The trace of an n-strand endomorphism: the closure against the strand bundle.

Equations

• RS.skeinTrace f n g = (RS.HomSpace.traceMap f.val n) g

theorem RS.skeinTrace_tensorHom {R : ℕ} (f : EdgeRankParameter R) {a b : ℕ} (u : skeinEnd f a) (v : skeinEnd f b) : skeinTrace f (a + b) (have this := CategoryTheory.MonoidalCategoryStruct.tensorHom u v; this) = skeinTrace f a u * skeinTrace f b v

The trace of a tensor product is the product of traces.

theorem RS.skeinTrace_zero_one {R : ℕ} (f : EdgeRankParameter R) : skeinTrace f 0 1 = 1

The trace of the empty identity is one.