# 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.

class CategoryTheory.Linear (R : Type w) [] (C : Type u) :
Type (max (max u v) w)

A category is called R-linear if P ⟶ Q is an R-module such that composition is R-linear in both variables.

• homModule : (X Y : C) → Module R (X Y)
• smul_comp : ∀ (X Y Z : C) (r : R) (f : X Y) (g : Y Z),

compatibility of the scalar multiplication with the post-composition

• comp_smul : ∀ (X Y Z : C) (f : X Y) (r : R) (g : Y Z),

compatibility of the scalar multiplication with the pre-composition

Instances
@[simp]
theorem CategoryTheory.Linear.smul_comp {R : Type w} [] {C : Type u} [self : ] (X : C) (Y : C) (Z : C) (r : R) (f : X Y) (g : Y Z) :

compatibility of the scalar multiplication with the post-composition

@[simp]
theorem CategoryTheory.Linear.comp_smul {R : Type w} [] {C : Type u} [self : ] (X : C) (Y : C) (Z : C) (f : X Y) (r : R) (g : Y Z) :

compatibility of the scalar multiplication with the pre-composition

Equations
• CategoryTheory.Linear.preadditiveNatLinear = { homModule := inferInstance, smul_comp := , comp_smul := }
Equations
• CategoryTheory.Linear.preadditiveIntLinear = { homModule := inferInstance, smul_comp := , comp_smul := }
instance CategoryTheory.Linear.instModuleEnd {C : Type u} {R : Type w} [] [] (X : C) :
Equations
• = id inferInstance
instance CategoryTheory.Linear.instAlgebraEnd {C : Type u} {R : Type w} [] [] (X : C) :
Equations
instance CategoryTheory.Linear.inducedCategory {C : Type u} {R : Type w} [] [] {D : Type u'} (F : DC) :
Equations
instance CategoryTheory.Linear.fullSubcategory {C : Type u} {R : Type w} [] [] (Z : CProp) :
Equations
@[simp]
theorem CategoryTheory.Linear.leftComp_apply {C : Type u} (R : Type w) [] [] {X : C} {Y : C} (Z : C) (f : X Y) (g : Y Z) :
def CategoryTheory.Linear.leftComp {C : Type u} (R : Type w) [] [] {X : C} {Y : C} (Z : C) (f : X Y) :
(Y Z) →ₗ[R] X Z

Composition by a fixed left argument as an R-linear map.

Equations
• = { toFun := fun (g : Y Z) => , map_add' := , map_smul' := }
Instances For
@[simp]
theorem CategoryTheory.Linear.rightComp_apply {C : Type u} (R : Type w) [] [] (X : C) {Y : C} {Z : C} (g : Y Z) (f : X Y) :
def CategoryTheory.Linear.rightComp {C : Type u} (R : Type w) [] [] (X : C) {Y : C} {Z : C} (g : Y Z) :
(X Y) →ₗ[R] X Z

Composition by a fixed right argument as an R-linear map.

Equations
• = { toFun := fun (f : X Y) => , map_add' := , map_smul' := }
Instances For
instance CategoryTheory.Linear.instEpiHSMulHomOfInvertible {C : Type u} (R : Type w) [] [] {X : C} {Y : C} (f : X Y) (r : R) [] :
Equations
• =
instance CategoryTheory.Linear.instMonoHSMulHomOfInvertible {C : Type u} (R : Type w) [] [] {X : C} {Y : C} (f : X Y) (r : R) [] :
Equations
• =
def CategoryTheory.Linear.homCongr (k : Type u_1) {C : Type u_2} [] [] [] {X : C} {Y : C} {W : C} {Z : C} (f₁ : X Y) (f₂ : W Z) :
(X W) ≃ₗ[k] Y Z

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).

Equations
• One or more equations did not get rendered due to their size.
Instances For
theorem CategoryTheory.Linear.homCongr_apply (k : Type u_1) {C : Type u_2} [] [] [] {X : C} {Y : C} {W : C} {Z : C} (f₁ : X Y) (f₂ : W Z) (f : X W) :
theorem CategoryTheory.Linear.homCongr_symm_apply (k : Type u_1) {C : Type u_2} [] [] [] {X : C} {Y : C} {W : C} {Z : C} (f₁ : X Y) (f₂ : W Z) (f : Y Z) :
@[simp]
theorem CategoryTheory.Linear.units_smul_comp {C : Type u} {R : Type w} [] [] {X : C} {Y : C} {Z : C} (r : Rˣ) (f : X Y) (g : Y Z) :
@[simp]
theorem CategoryTheory.Linear.comp_units_smul {C : Type u} {R : Type w} [] [] {X : C} {Y : C} {Z : C} (f : X Y) (r : Rˣ) (g : Y Z) :
@[simp]
theorem CategoryTheory.Linear.comp_apply {C : Type u} {S : Type w} [] [] (X : C) (Y : C) (Z : C) (f : X Y) :
f =
def CategoryTheory.Linear.comp {C : Type u} {S : Type w} [] [] (X : C) (Y : C) (Z : C) :
(X Y) →ₗ[S] (Y Z) →ₗ[S] X Z

Composition as a bilinear map.

Equations
• = { toFun := fun (f : X Y) => , map_add' := , map_smul' := }
Instances For