mathlib documentation

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.

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) [category_theory.category C] [category_theory.preadditive C] :
Type (max u v w)
  • hom_module : (Π (X Y : C), module R (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
@[simp]
theorem category_theory.linear.smul_comp {R : Type w} [semiring R] {C : Type u} [category_theory.category C] [category_theory.preadditive C] [self : category_theory.linear R 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} [category_theory.category C] [category_theory.preadditive C] [self : category_theory.linear R 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} [category_theory.category C] [category_theory.preadditive C] [self : category_theory.linear R 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} [category_theory.category C] [category_theory.preadditive C] [self : category_theory.linear R 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'
def category_theory.linear.left_comp {C : Type u} [category_theory.category C] [category_theory.preadditive C] (R : Type w) [semiring R] [category_theory.linear R C] {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} [category_theory.category C] [category_theory.preadditive C] (R : Type w) [semiring R] [category_theory.linear R C] {X Y : C} (Z : C) (f : X Y) (g : Y Z) :
@[simp]
theorem category_theory.linear.right_comp_apply {C : Type u} [category_theory.category C] [category_theory.preadditive C] (R : Type w) [semiring R] [category_theory.linear R C] (X : C) {Y Z : C} (g : Y Z) (f : X Y) :
def category_theory.linear.right_comp {C : Type u} [category_theory.category C] [category_theory.preadditive C] (R : Type w) [semiring R] [category_theory.linear R C] (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
def category_theory.linear.comp {C : Type u} [category_theory.category C] [category_theory.preadditive C] {S : Type w} [comm_semiring S] [category_theory.linear S C] (X Y Z : C) :
(X Y) →ₗ[S] (Y Z) →ₗ[S] X Z

Composition as a bilinear map.

Equations