Monoidal preadditivity and linearity through the tower

The skein tensor is a bundled bilinear map, so the skein category is monoidal-preadditive and monoidal-linear; both properties lift through the Karoubi and matrix layers entrywise, giving the full instance chain for the envelope.

The skein base

instance RS.skeinMonoidalPreadditive {R : ℕ} (f : EdgeRankParameter R) : CategoryTheory.MonoidalPreadditive (SkeinObj f)

The skein tensor is additive in each argument.

instance RS.skeinMonoidalLinear {R : ℕ} (f : EdgeRankParameter R) : CategoryTheory.MonoidalLinear ℂ (SkeinObj f)

And ℂ-linear in each argument, being a bundled bilinear map.

The Karoubi lift (general)

instance RS.karoubiMonoidalPreadditive (C : Type u_1) [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.MonoidalPreadditive C] : CategoryTheory.MonoidalPreadditive (CategoryTheory.Idempotents.Karoubi C)

Monoidal preadditivity lifts to the Karoubi envelope, where tensoring acts on underlying morphisms.

instance RS.karoubiMonoidalLinear (C : Type u_1) [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.MonoidalPreadditive C] [CategoryTheory.Linear ℂ C] [CategoryTheory.MonoidalLinear ℂ C] : CategoryTheory.MonoidalLinear ℂ (CategoryTheory.Idempotents.Karoubi C)

And so does monoidal linearity.

The matrix lift

instance RS.matMonoidalPreadditive (C : Type u_1) [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.MonoidalPreadditive C] : CategoryTheory.MonoidalPreadditive (CategoryTheory.Mat_ C)

Monoidal preadditivity lifts to the matrix layer entrywise.

@[instance_reducible]

noncomputable instance RS.matHomSMul' (C : Type u_1) [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear ℂ C] (M N : CategoryTheory.Mat_ C) : SMul ℂ (M ⟶ N)

The entrywise linear structure on matrix Homs (general base).

Equations

• RS.matHomSMul' C M N = { smul := fun (c : ℂ) (φ : M ⟶ N) (i : M.ι) (j : N.ι) => c • φ i j }

@[instance_reducible]

noncomputable instance RS.matHomModule' (C : Type u_1) [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear ℂ C] (M N : CategoryTheory.Mat_ C) : Module ℂ (M ⟶ N)

The matrix layer's hom-sets are ℂ-modules, entrywise.

Equations

• RS.matHomModule' C M N = { toSMul := RS.matHomSMul' C M N, mul_smul := ⋯, one_smul := ⋯, smul_zero := ⋯, smul_add := ⋯, add_smul := ⋯, zero_smul := ⋯ }

@[instance_reducible]

noncomputable instance RS.matLinear' (C : Type u_1) [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear ℂ C] : CategoryTheory.Linear ℂ (CategoryTheory.Mat_ C)

Hence the matrix layer is ℂ-linear.

Equations

• RS.matLinear' C = { homModule := inferInstance, smul_comp := ⋯, comp_smul := ⋯ }

instance RS.matMonoidalLinear (C : Type u_1) [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.MonoidalPreadditive C] [CategoryTheory.Linear ℂ C] [CategoryTheory.MonoidalLinear ℂ C] : CategoryTheory.MonoidalLinear ℂ (CategoryTheory.Mat_ C)

And monoidal-linear, completing the instance chain for the envelope.

The envelope chain