# mathlibdocumentation

category_theory.linear.default

# 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 add_comm_group 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]
structure category_theory.linear (R : Type w) [semiring R] (C : Type u)  :
Type (max u v w)
• hom_module : (Π (X Y : C), (X Y)) . "apply_instance"
• smul_comp' : (∀ (X Y Z : C) (r : R) (f : X Y) (g : Y Z), (r f) g = r f g) . "obviously"
• comp_smul' : (∀ (X Y Z : C) (f : X Y) (r : R) (g : Y Z), f (r g) = r f g) . "obviously"

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

Instances of this typeclass
Instances of other typeclasses for category_theory.linear
• category_theory.linear.has_sizeof_inst
@[simp]
theorem category_theory.linear.smul_comp {R : Type w} [semiring R] {C : Type u} [self : C] (X Y Z : C) (r : R) (f : X Y) (g : Y Z) :
(r f) g = r f g
@[simp]
theorem category_theory.linear.comp_smul {R : Type w} [semiring R] {C : Type u} [self : C] (X Y Z : C) (f : X Y) (r : R) (g : Y Z) :
f (r g) = r f g
@[simp]
theorem category_theory.linear.smul_comp_assoc {R : Type w} [semiring R] {C : Type u} [self : C] (X Y Z : C) (r : R) (f : X Y) (g : Y Z) {X' : C} (f' : Z X') :
(r f) g f' = (r f g) f'
theorem category_theory.linear.comp_smul_assoc {R : Type w} [semiring R] {C : Type u} [self : C] (X Y Z : C) (f : X Y) (r : R) (g : Y Z) {X' : C} (f' : Z X') :
f (r g) f' = (r f g) f'
@[protected, instance]
Equations
@[protected, instance]
def category_theory.linear.category_theory.End.module {C : Type u} {R : Type w} [comm_ring R] (X : C) :
Equations
@[protected, instance]
def category_theory.linear.category_theory.End.algebra {C : Type u} {R : Type w} [comm_ring R] (X : C) :
Equations
@[protected, instance]
def category_theory.linear.induced_category.category {C : Type u} {R : Type w} [semiring R] {D : Type u'} (F : D → C) :
Equations
def category_theory.linear.left_comp {C : Type u} (R : Type w) [semiring R] {X Y : C} (Z : C) (f : X Y) :
(Y Z) →ₗ[R] X Z

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

Equations
@[simp]
theorem category_theory.linear.left_comp_apply {C : Type u} (R : Type w) [semiring R] {X Y : C} (Z : C) (f : X Y) (g : Y Z) :
g = f g
@[simp]
theorem category_theory.linear.right_comp_apply {C : Type u} (R : Type w) [semiring R] (X : C) {Y Z : C} (g : Y Z) (f : X Y) :
f = f g
def category_theory.linear.right_comp {C : Type u} (R : Type w) [semiring R] (X : C) {Y Z : C} (g : Y Z) :
(X Y) →ₗ[R] X Z

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

Equations
@[protected, instance]
def category_theory.linear.has_scalar.smul.category_theory.epi {C : Type u} (R : Type w) [semiring R] {X Y : C} (f : X Y) (r : R) [invertible r] :
@[protected, instance]
def category_theory.linear.has_scalar.smul.category_theory.mono {C : Type u} (R : Type w) [semiring R] {X Y : C} (f : X Y) (r : R) [invertible r] :
@[simp]
theorem category_theory.linear.comp_apply {C : Type u} {S : Type w} (X Y Z : C) (f : X Y) :
Z) f =
def category_theory.linear.comp {C : Type u} {S : Type w} (X Y Z : C) :
(X Y) →ₗ[S] (Y Z) →ₗ[S] X Z

Composition as a bilinear map.

Equations