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.

source

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

Instances

source

@[instance_reducible]

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

Linear ℕ C

Equations

CategoryTheory.Linear.preadditiveNatLinear = { homModule := inferInstance, smul_comp := ⋯, comp_smul := ⋯ }

source

@[instance_reducible]

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

Linear ℤ C

Equations

CategoryTheory.Linear.preadditiveIntLinear = { homModule := inferInstance, smul_comp := ⋯, comp_smul := ⋯ }

source

@[instance_reducible]

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)

Equations

CategoryTheory.Linear.instModuleEnd X = AddEquiv.module R CategoryTheory.End.addEquiv

source

@[simp]

theorem CategoryTheory.End.smul_asHom {C : Type u} [Category.{v, u} C] [Preadditive C] {R : Type w} [Semiring R] [Linear R C] {X : C} (r : R) (e : End X) :

(r • e).asHom = r • e.asHom

source

@[implicit_reducible]

def CategoryTheory.End.linearEquiv {C : Type u} [Category.{v, u} C] [Preadditive C] {R : Type w} [Semiring R] [Linear R C] {X : C} :

End X ≃ₗ[R] X ⟶ X

The linear equivalence End X ≃ₗ[R] (X ⟶ X) when X is an object of a R-linear category.

Equations

CategoryTheory.End.linearEquiv = { toFun := CategoryTheory.End.addEquiv.toFun, map_add' := ⋯, map_smul' := ⋯, invFun := CategoryTheory.End.addEquiv.invFun, left_inv := ⋯, right_inv := ⋯ }

Instances For

source

@[simp]

theorem CategoryTheory.End.linearEquiv_symm_apply {C : Type u} [Category.{v, u} C] [Preadditive C] {R : Type w} [Semiring R] [Linear R C] {X : C} (a✝ : X ⟶ X) :

linearEquiv.symm a✝ = addEquiv.invFun a✝

source

@[simp]

theorem CategoryTheory.End.linearEquiv_apply {C : Type u} [Category.{v, u} C] [Preadditive C] {R : Type w} [Semiring R] [Linear R C] {X : C} (a✝ : End X) :

linearEquiv a✝ = addEquiv.toFun a✝

source

@[instance_reducible]

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)

Equations

CategoryTheory.Linear.instAlgebraEnd X = Algebra.ofModule ⋯ ⋯

source

@[instance_reducible]

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)

Equations

One or more equations did not get rendered due to their size.

source

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.

Equations

One or more equations did not get rendered due to their size.

Instances For

source

@[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

source

@[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✝

source

@[instance_reducible]

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

Equations

CategoryTheory.Linear.fullSubcategory Z = CategoryTheory.Linear.inducedCategory CategoryTheory.ObjectProperty.FullSubcategory.obj

source

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.

Equations

CategoryTheory.Linear.leftComp R Z f = { toFun := fun (g : Y ⟶ Z) => CategoryTheory.CategoryStruct.comp f g, map_add' := ⋯, map_smul' := ⋯ }

Instances For

source

@[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

source

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.

Equations

CategoryTheory.Linear.rightComp R X g = { toFun := fun (f : X ⟶ Y) => CategoryTheory.CategoryStruct.comp f g, map_add' := ⋯, map_smul' := ⋯ }

Instances For

source

@[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

source

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)

source

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)

source

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).

Equations

One or more equations did not get rendered due to their size.

Instances For

source

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

source

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)

source

@[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

source

@[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

source

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.

Equations

CategoryTheory.Linear.comp X Y Z = { toFun := fun (f : X ⟶ Y) => CategoryTheory.Linear.leftComp S Z f, map_add' := ⋯, map_smul' := ⋯ }

Instances For

source

@[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

Documentation

Mathlib.CategoryTheory.Linear.Basic

Linear categories #

Implementation #

Future work #