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 would just be a category enriched in Module R.

class CategoryTheory.Linear (R : Type w) [Semiring R] (C : Type u) [Category.{v, u} C] [Preadditive C] : 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) : CategoryStruct.comp (r • f) g = r • CategoryStruct.comp f g

  compatibility of the scalar multiplication with the post-composition

• comp_smul (X Y Z : C) (f : X ⟶ Y) (r : R) (g : Y ⟶ Z) : CategoryStruct.comp f (r • g) = r • CategoryStruct.comp f g

  compatibility of the scalar multiplication with the pre-composition

instance CategoryTheory.Linear.preadditiveNatLinear {C : Type u} [Category.{v, u} C] [Preadditive C] : Linear ℕ C

instance CategoryTheory.Linear.preadditiveIntLinear {C : Type u} [Category.{v, u} C] [Preadditive C] : Linear ℤ C

instance CategoryTheory.Linear.instModuleEnd {C : Type u} [Category.{v, u} C] [Preadditive C] {R : Type w} [Semiring R] [Linear R C] (X : C) : Module R (End X)

instance CategoryTheory.Linear.instAlgebraEnd {C : Type u} [Category.{v, u} C] [Preadditive C] {R : Type w} [CommSemiring R] [Linear R C] (X : C) : Algebra R (End X)

instance CategoryTheory.Linear.inducedCategory {C : Type u} [Category.{v, u} C] [Preadditive C] {R : Type w} [Semiring R] [Linear R C] {D : Type u'} (F : D → C) : Linear R (InducedCategory C F)

def CategoryTheory.InducedCategory.homLinearEquiv {C : Type u} [Category.{v, u} C] [Preadditive C] {R : Type w} [Semiring R] [Linear R C] {D : Type u'} {F : D → C} {X Y : InducedCategory C F} : (X ⟶ Y) ≃ₗ[R] F X ⟶ F Y

The linear equivalence (X ⟶ Y) ≃+ (F X ⟶ F Y) when F : D → C and C is a R-linear category.

@[simp]

theorem CategoryTheory.InducedCategory.homLinearEquiv_symm_apply_hom {C : Type u} [Category.{v, u} C] [Preadditive C] {R : Type w} [Semiring R] [Linear R C] {D : Type u'} {F : D → C} {X Y : InducedCategory C F} (a✝ : F X ⟶ F Y) : (homLinearEquiv.symm a✝).hom = a✝

@[simp]

theorem CategoryTheory.InducedCategory.homLinearEquiv_apply {C : Type u} [Category.{v, u} C] [Preadditive C] {R : Type w} [Semiring R] [Linear R C] {D : Type u'} {F : D → C} {X Y : InducedCategory C F} (a✝ : X ⟶ Y) : homLinearEquiv a✝ = a✝.hom

instance CategoryTheory.Linear.fullSubcategory {C : Type u} [Category.{v, u} C] [Preadditive C] {R : Type w} [Semiring R] [Linear R C] (Z : ObjectProperty C) : Linear R Z.FullSubcategory

def CategoryTheory.Linear.leftComp {C : Type u} [Category.{v, u} C] [Preadditive C] (R : Type w) [Semiring R] [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.

@[simp]

theorem CategoryTheory.Linear.leftComp_apply {C : Type u} [Category.{v, u} C] [Preadditive C] (R : Type w) [Semiring R] [Linear R C] {X Y : C} (Z : C) (f : X ⟶ Y) (g : Y ⟶ Z) : (leftComp R Z f) g = CategoryStruct.comp f g

def CategoryTheory.Linear.rightComp {C : Type u} [Category.{v, u} C] [Preadditive C] (R : Type w) [Semiring R] [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.

@[simp]

theorem CategoryTheory.Linear.rightComp_apply {C : Type u} [Category.{v, u} C] [Preadditive C] (R : Type w) [Semiring R] [Linear R C] (X : C) {Y Z : C} (g : Y ⟶ Z) (f : X ⟶ Y) : (rightComp R X g) f = CategoryStruct.comp f g

instance CategoryTheory.Linear.instEpiHSMulHomOfInvertible {C : Type u} [Category.{v, u} C] [Preadditive C] (R : Type w) [Semiring R] [Linear R C] {X Y : C} (f : X ⟶ Y) [Epi f] (r : R) [Invertible r] : Epi (r • f)

instance CategoryTheory.Linear.instMonoHSMulHomOfInvertible {C : Type u} [Category.{v, u} C] [Preadditive C] (R : Type w) [Semiring R] [Linear R C] {X Y : C} (f : X ⟶ Y) [Mono f] (r : R) [Invertible r] : Mono (r • f)

def CategoryTheory.Linear.homCongr (k : Type u_1) {C : Type u_2} [Category.{v_1, u_2} C] [Semiring k] [Preadditive C] [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).

theorem CategoryTheory.Linear.homCongr_apply (k : Type u_1) {C : Type u_2} [Category.{v_1, u_2} C] [Semiring k] [Preadditive C] [Linear k C] {X Y W Z : C} (f₁ : X ≅ Y) (f₂ : W ≅ Z) (f : X ⟶ W) : (homCongr k f₁ f₂) f = CategoryStruct.comp (CategoryStruct.comp f₁.inv f) f₂.hom

theorem CategoryTheory.Linear.homCongr_symm_apply (k : Type u_1) {C : Type u_2} [Category.{v_1, u_2} C] [Semiring k] [Preadditive C] [Linear k C] {X Y W Z : C} (f₁ : X ≅ Y) (f₂ : W ≅ Z) (f : Y ⟶ Z) : (homCongr k f₁ f₂).symm f = CategoryStruct.comp f₁.hom (CategoryStruct.comp f f₂.inv)

@[simp]

theorem CategoryTheory.Linear.units_smul_comp {C : Type u} [Category.{v, u} C] [Preadditive C] {R : Type w} [Semiring R] [Linear R C] {X Y Z : C} (r : Rˣ) (f : X ⟶ Y) (g : Y ⟶ Z) : CategoryStruct.comp (r • f) g = r • CategoryStruct.comp f g

@[simp]

theorem CategoryTheory.Linear.comp_units_smul {C : Type u} [Category.{v, u} C] [Preadditive C] {R : Type w} [Semiring R] [Linear R C] {X Y Z : C} (f : X ⟶ Y) (r : Rˣ) (g : Y ⟶ Z) : CategoryStruct.comp f (r • g) = r • CategoryStruct.comp f g

def CategoryTheory.Linear.comp {C : Type u} [Category.{v, u} C] [Preadditive C] {S : Type w} [CommSemiring S] [Linear S C] (X Y Z : C) : (X ⟶ Y) →ₗ[S] (Y ⟶ Z) →ₗ[S] X ⟶ Z

Composition as a bilinear map.

@[simp]

theorem CategoryTheory.Linear.comp_apply {C : Type u} [Category.{v, u} C] [Preadditive C] {S : Type w} [CommSemiring S] [Linear S C] (X Y Z : C) (f : X ⟶ Y) : (comp X Y Z) f = leftComp S Z f