Documentation

Mathlib.CategoryTheory.Center.Linear

Center of a linear category #

If C is a R-linear category, we define a ring morphism R →+* CatCenter C and conversely, if C is a preadditive category, and φ : R →+* CatCenter C is a ring morphism, we define a R-linear structure on C attached to φ.

The canonical morphism R →+* CatCenter C when C is a R-linear category.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    @[simp]
    theorem CategoryTheory.Linear.toCatCenter_apply_app (R : Type w) [Ring R] (C : Type u) [Category.{v, u} C] [Preadditive C] [Linear R C] (a : R) (X : C) :
    def CategoryTheory.Linear.smulOfRingMorphism {R : Type w} [Ring R] {C : Type u} [Category.{v, u} C] [Preadditive C] (φ : R →+* CatCenter C) (X Y : C) :
    SMul R (X Y)

    The scalar multiplication by R on the type X ⟶ Y of morphisms in a category C equipped with a ring morphism R →+* CatCenter C.

    Equations
    Instances For
      theorem CategoryTheory.Linear.smulOfRingMorphism_smul_eq {R : Type w} [Ring R] {C : Type u} [Category.{v, u} C] [Preadditive C] (φ : R →+* CatCenter C) {X Y : C} (a : R) (f : X Y) :
      a f = CategoryStruct.comp ((φ a).app X) f
      theorem CategoryTheory.Linear.smulOfRingMorphism_smul_eq' {R : Type w} [Ring R] {C : Type u} [Category.{v, u} C] [Preadditive C] (φ : R →+* CatCenter C) {X Y : C} (a : R) (f : X Y) :
      a f = CategoryStruct.comp f ((φ a).app Y)

      a • f = f ≫ (φ a).app Y.

      def CategoryTheory.Linear.homModuleOfRingMorphism {R : Type w} [Ring R] {C : Type u} [Category.{v, u} C] [Preadditive C] (φ : R →+* CatCenter C) (X Y : C) :
      Module R (X Y)

      The R-module structure on the type X ⟶ Y of morphisms in a category C equipped with a ring morphism R →+* CatCenter C.

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

        The R-linear structure on a preadditive category C equipped with a ring morphism R →+* CatCenter C.

        Equations
        Instances For