Composition descends to the Hom spaces

With the pairing kernel a two-sided ideal (Lemma 3.3(a), both halves), the bilinear composition of free modules descends to a bilinear composition of Hom spaces — the composition of the skein category. On fragment classes it is composition of fragments.

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

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

Equations

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

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

The auxiliary composition on a fragment class.

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

The descended composition of the skein category: the bilinear composition of Hom spaces.

Equations

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

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

The descended composition on quotient classes.

theorem RS.HomSpace.comp_ofFragment {R : ℕ} (f : EdgeRankParameter R) (s t u : ℕ) (F : Fragment (Fin (s + t))) (G : Fragment (Fin (t + u))) : ((comp f s t u) (ofFragment f.val F)) (ofFragment f.val G) = ofFragment f.val (F.compose G)

Composition of fragment classes is the class of the composition.