Center of a linear category

If C is an 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 an 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] : R →+* CatCenter C

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

Equations

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

@[simp]

theorem CategoryTheory.Linear.toCatCenter_apply_asHom_app (R : Type w) [Ring R] (C : Type u) [Category.{v, u} C] [Preadditive C] [Linear R C] (a : R) (X : C) : ((toCatCenter R C) a).asHom.app X = a • CategoryStruct.id X

@[instance_reducible]

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

• CategoryTheory.Linear.smulOfRingMorphism φ X Y = { smul := fun (a : R) (f : X ⟶ Y) => CategoryTheory.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 ((φ 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.

@[instance_reducible]

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.

@[instance_reducible]

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 := ⋯ }