mathlib3 documentation

category_theory.linear.basic

Linear categories #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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]
  • 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 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} [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]

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

Equations
def category_theory.linear.hom_congr (k : Type u_1) {C : Type u_2} [category_theory.category C] [semiring k] [category_theory.preadditive C] [category_theory.linear k C] {X Y W 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
theorem category_theory.linear.hom_congr_apply (k : Type u_1) {C : Type u_2} [category_theory.category C] [semiring k] [category_theory.preadditive C] [category_theory.linear k C] {X Y W Z : C} (f₁ : X Y) (f₂ : W Z) (f : X W) :
(category_theory.linear.hom_congr k f₁ f₂) f = (f₁.inv f) f₂.hom
theorem category_theory.linear.hom_congr_symm_apply (k : Type u_1) {C : Type u_2} [category_theory.category C] [semiring k] [category_theory.preadditive C] [category_theory.linear k C] {X Y W Z : C} (f₁ : X Y) (f₂ : W Z) (f : Y Z) :
((category_theory.linear.hom_congr k f₁ f₂).symm) f = f₁.hom f f₂.inv

Composition as a bilinear map.

Equations