Linear categories #
An R
-linear category is a category in which X ⟶ Y
is an R
-module in such a way that
composition of morphisms is R
-linear in both variables.
Note that sometimes in the literature a "linear category" is further required to be abelian.
Implementation #
Corresponding to the fact that we need to have an AddCommGroup X
structure in place
to talk about a Module R X
structure,
we need Preadditive C
as a prerequisite typeclass for Linear R C
.
This makes for longer signatures than would be ideal.
Future work #
It would be nice to have a usable framework of enriched categories in which this just became
a category enriched in Module R
.
- smul_comp : ∀ (X Y Z : C) (r : R) (f : X ⟶ Y) (g : Y ⟶ Z), CategoryTheory.CategoryStruct.comp (r • f) g = r • CategoryTheory.CategoryStruct.comp f g
compatibility of the scalar multiplication with the post-composition
- comp_smul : ∀ (X Y Z : C) (f : X ⟶ Y) (r : R) (g : Y ⟶ Z), CategoryTheory.CategoryStruct.comp f (r • g) = r • CategoryTheory.CategoryStruct.comp f g
compatibility of the scalar multiplication with the pre-composition
A category is called R
-linear if P ⟶ Q
is an R
-module such that composition is
R
-linear in both variables.
Instances
Composition by a fixed left argument as an R
-linear map.
Instances For
Composition by a fixed right argument as an R
-linear map.
Instances For
Given isomorphic objects X ≅ Y, W ≅ Z
in a k
-linear category, we have a k
-linear
isomorphism between Hom(X, W)
and Hom(Y, Z).
Instances For
Composition as a bilinear map.