# Documentation

Mathlib.CategoryTheory.Linear.Basic

# 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)
• 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

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

Instances
instance CategoryTheory.Linear.inducedCategory {C : Type u} {R : Type w} [] [] {D : Type u'} (F : DC) :
instance CategoryTheory.Linear.fullSubcategory {C : Type u} {R : Type w} [] [] (Z : CProp) :
@[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.

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.

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

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

Instances For