The skein category is ℂ-linear

Hom spaces are ℂ-modules and the descended composition is bilinear, so the skein category is preadditive and ℂ-linear — two of the instance hypotheses of the Deligne package carrier.

@[instance_reducible]

noncomputable instance RS.skeinHomAddCommGroup {R : ℕ} (f : EdgeRankParameter R) (X Y : SkeinObj f) : AddCommGroup (X ⟶ Y)

Skein hom-spaces are abelian groups.

Equations

• One or more equations did not get rendered due to their size.

@[instance_reducible]

noncomputable instance RS.skeinHomModule {R : ℕ} (f : EdgeRankParameter R) (X Y : SkeinObj f) : Module ℂ (X ⟶ Y)

And ℂ-modules.

Equations

• RS.skeinHomModule f X Y = { smul := RS.skeinHomModule._aux_1 f X Y, mul_smul := ⋯, one_smul := ⋯, smul_zero := ⋯, smul_add := ⋯, add_smul := ⋯, zero_smul := ⋯ }

@[instance_reducible]

noncomputable instance RS.skeinPreadditive {R : ℕ} (f : EdgeRankParameter R) : CategoryTheory.Preadditive (SkeinObj f)

Composition is additive in each argument, so the category is preadditive.

Equations

• RS.skeinPreadditive f = { homGroup := RS.skeinHomAddCommGroup f, add_comp := ⋯, comp_add := ⋯ }

@[instance_reducible]

noncomputable instance RS.skeinLinear {R : ℕ} (f : EdgeRankParameter R) : CategoryTheory.Linear ℂ (SkeinObj f)

And bilinear, so it is ℂ-linear.

Equations

• RS.skeinLinear f = { homModule := RS.skeinHomModule f, smul_comp := ⋯, comp_smul := ⋯ }