The monoidal product descends to the Hom spaces

With the tensor ideal two-sided (Lemma 3.3(b), both slots), the bilinear tensor of free modules descends to a bilinear tensor of Hom spaces — the monoidal product of the skein category. On fragment classes it is the tensor of fragments.

noncomputable def RS.homTensorAux {R : ℕ} (f : EdgeRankParameter R) (s t u v : ℕ) (x : Fragment (Fin (s + t)) →₀ ℂ) : HomSpace f.val (u + v) →ₗ[ℂ] HomSpace f.val (s + u + (t + v))

The tensor into the quotient, for a fixed left factor.

Equations

• RS.homTensorAux f s t u v x = (RS.connectionMap f.val (u + v)).ker.liftQ ((RS.connectionMap f.val (s + u + (t + v))).ker.mkQ ∘ₗ (RS.tensorFinsupp s t u v) x) ⋯

theorem RS.homTensorAux_mk {R : ℕ} (f : EdgeRankParameter R) (s t u v : ℕ) (x : Fragment (Fin (s + t)) →₀ ℂ) (y : Fragment (Fin (u + v)) →₀ ℂ) : (homTensorAux f s t u v x) ((connectionMap f.val (u + v)).ker.mkQ y) = (connectionMap f.val (s + u + (t + v))).ker.mkQ (((tensorFinsupp s t u v) x) y)

The auxiliary tensor on a fragment class.

noncomputable def RS.HomSpace.tensor {R : ℕ} (f : EdgeRankParameter R) (s t u v : ℕ) : HomSpace f.val (s + t) →ₗ[ℂ] HomSpace f.val (u + v) →ₗ[ℂ] HomSpace f.val (s + u + (t + v))

The descended monoidal product of the skein category.

Equations

• RS.HomSpace.tensor f s t u v = (RS.connectionMap f.val (s + t)).ker.liftQ { toFun := RS.homTensorAux f s t u v, map_add' := ⋯, map_smul' := ⋯ } ⋯

theorem RS.HomSpace.tensor_mk {R : ℕ} (f : EdgeRankParameter R) (s t u v : ℕ) (x : Fragment (Fin (s + t)) →₀ ℂ) (y : Fragment (Fin (u + v)) →₀ ℂ) : ((tensor f s t u v) ((connectionMap f.val (s + t)).ker.mkQ x)) ((connectionMap f.val (u + v)).ker.mkQ y) = (connectionMap f.val (s + u + (t + v))).ker.mkQ (((tensorFinsupp s t u v) x) y)

The descended tensor on quotient classes.

theorem RS.HomSpace.tensor_ofFragment {R : ℕ} (f : EdgeRankParameter R) (s t u v : ℕ) (F : Fragment (Fin (s + t))) (G : Fragment (Fin (u + v))) : ((tensor f s t u v) (ofFragment f.val F)) (ofFragment f.val G) = ofFragment f.val (tensorFragment F G)

Tensor of fragment classes is the class of the tensor.