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 φ.
def
CategoryTheory.Linear.toCatCenter
(R : Type w)
[Ring R]
(C : Type u)
[Category.{v, u} C]
[Preadditive C]
[Linear R C]
:
The canonical morphism R →+* CatCenter C when C is a R-linear category.
Equations
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)
:
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)
:
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 = 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)
:
The R-module structure on the type X ⟶ Y of morphisms in
a category C equipped with a ring morphism R →+* CatCenter C.
Equations
Instances For
def
CategoryTheory.Linear.ofRingMorphism
{R : Type w}
[Ring R]
{C : Type u}
[Category.{v, u} C]
[Preadditive C]
(φ : R →+* CatCenter C)
:
Linear R C
The R-linear structure on a preadditive category C equipped with
a ring morphism R →+* CatCenter C.