The categorical trace on Hom spaces

The trace of a (t + t)-fragment is its full strand closure: the closure pairing against the strand bundle, which threads each output label back to the matching input. The trace functional is therefore the connection pairing evaluated at the bundle; it kills the pairing kernel by construction and so descends to the Hom spaces of the skein category.

noncomputable def RS.fragTrace (f : ClosedFragment → ℂ) {t : ℕ} (F : Fragment (Fin (t + t))) : ℂ

The trace of a (t + t)-fragment under a parameter: the value of its strand closure.

Equations

• RS.fragTrace f F = f (RS.pairClose F (RS.strandBundle t))

noncomputable def RS.traceFunctional (f : ClosedFragment → ℂ) (t : ℕ) : (Fragment (Fin (t + t)) →₀ ℂ) →ₗ[ℂ] ℂ

The trace as a linear functional on the free module: the connection pairing evaluated at the strand bundle.

Equations

• RS.traceFunctional f t = LinearMap.proj (RS.strandBundle t) ∘ₗ RS.connectionMap f (t + t)

theorem RS.traceFunctional_single (f : ClosedFragment → ℂ) {t : ℕ} (F : Fragment (Fin (t + t))) : (traceFunctional f t) (Finsupp.single F 1) = fragTrace f F

The trace functional on a single fragment is its trace.

theorem RS.ker_le_ker_traceFunctional (f : ClosedFragment → ℂ) (t : ℕ) : (connectionMap f (t + t)).ker ≤ (traceFunctional f t).ker

The pairing kernel is contained in the trace kernel.

noncomputable def RS.HomSpace.traceMap (f : ClosedFragment → ℂ) (t : ℕ) : HomSpace f (t + t) →ₗ[ℂ] ℂ

The trace descends to the Hom space.

Equations

• RS.HomSpace.traceMap f t = (RS.connectionMap f (t + t)).ker.liftQ (RS.traceFunctional f t) ⋯

theorem RS.HomSpace.traceMap_ofFragment (f : ClosedFragment → ℂ) {t : ℕ} (F : Fragment (Fin (t + t))) : (traceMap f t) (ofFragment f F) = fragTrace f F

The descended trace on a fragment class is the fragment trace.