Documentation

Mathlib.CategoryTheory.Linear.Basic

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.

A category is called R-linear if P ⟶ Q is an R-module such that composition is R-linear in both variables.

Instances
    Equations
    • CategoryTheory.Linear.preadditiveNatLinear = CategoryTheory.Linear.mk
    Equations
    • CategoryTheory.Linear.preadditiveIntLinear = CategoryTheory.Linear.mk
    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.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      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.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        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).

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          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) :

          Composition as a bilinear map.

          Equations
          • One or more equations did not get rendered due to their size.
          Instances For