Documentation

Mathlib.CategoryTheory.Center.Preadditive

The center of an additive category #

source
@[simp]
theorem CategoryTheory.CatCenter.app_zero {C : Type u} [Category.{v, u} C] [Preadditive C] (X : C) :
app 0 X = 0
source
@[simp]
theorem CategoryTheory.CatCenter.app_add {C : Type u} [Category.{v, u} C] [Preadditive C] (z₁ z₂ : CatCenter C) (X : C) :
(z₁ + z₂).app X = z₁.app X + z₂.app X
source
@[simp]
theorem CategoryTheory.CatCenter.app_sub {C : Type u} [Category.{v, u} C] [Preadditive C] (z₁ z₂ : CatCenter C) (X : C) :
(z₁ - z₂).app X = z₁.app X - z₂.app X
source
@[simp]
theorem CategoryTheory.CatCenter.app_neg {C : Type u} [Category.{v, u} C] [Preadditive C] (z : CatCenter C) (X : C) :
(-z).app X = -z.app X