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.

source

class CategoryTheory.Linear (R : Type w) [Semiring R] (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] :

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), CategoryTheory.CategoryStruct.comp (r • f) g = r • CategoryTheory.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), CategoryTheory.CategoryStruct.comp f (r • g) = r • CategoryTheory.CategoryStruct.comp f g
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

source

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

CategoryTheory.Linear ℕ C

source

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

CategoryTheory.Linear ℤ C

source

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

Module R (CategoryTheory.End X)

source

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

Algebra R (CategoryTheory.End X)

source

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

CategoryTheory.Linear R (CategoryTheory.InducedCategory C F)

source

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

CategoryTheory.Linear R (CategoryTheory.FullSubcategory Z)

source

@[simp]

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

↑(CategoryTheory.Linear.leftComp R Z f) g = CategoryTheory.CategoryStruct.comp f g

source

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

source

@[simp]

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

↑(CategoryTheory.Linear.rightComp R X g) f = CategoryTheory.CategoryStruct.comp f g

source

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

source

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

CategoryTheory.Epi (r • f)

source

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

CategoryTheory.Mono (r • f)

source

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

source

theorem CategoryTheory.Linear.homCongr_apply (k : Type u_1) {C : Type u_2} [CategoryTheory.Category.{u_3, u_2} C] [Semiring k] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] {X : C} {Y : C} {W : C} {Z : C} (f₁ : X ≅ Y) (f₂ : W ≅ Z) (f : X ⟶ W) :

↑(CategoryTheory.Linear.homCongr k f₁ f₂) f = CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp f₁.inv f) f₂.hom

source

theorem CategoryTheory.Linear.homCongr_symm_apply (k : Type u_1) {C : Type u_2} [CategoryTheory.Category.{u_3, u_2} C] [Semiring k] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] {X : C} {Y : C} {W : C} {Z : C} (f₁ : X ≅ Y) (f₂ : W ≅ Z) (f : Y ⟶ Z) :

↑(LinearEquiv.symm (CategoryTheory.Linear.homCongr k f₁ f₂)) f = CategoryTheory.CategoryStruct.comp f₁.hom (CategoryTheory.CategoryStruct.comp f f₂.inv)

source

@[simp]

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

↑(CategoryTheory.Linear.comp X Y Z) f = CategoryTheory.Linear.leftComp S Z f

source

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

(X ⟶ Y) →ₗ[S] (Y ⟶ Z) →ₗ[S] X ⟶ Z

Composition as a bilinear map.

Instances For