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
- 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)
:
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
- CategoryTheory.Linear.smulOfRingMorphism φ X Y = { smul := fun (a : R) (f : X ⟶ Y) => CategoryTheory.CategoryStruct.comp ((φ a).app X) f }
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
- One or more equations did not get rendered due to their size.
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
.
Equations
- CategoryTheory.Linear.ofRingMorphism φ = { homModule := inferInstance, smul_comp := ⋯, comp_smul := ⋯ }