Documentation

Mathlib.CategoryTheory.Center.Preadditive

The center of an additive category #

source
šŸ“ coverage
@[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
šŸ“ coverage
@[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
šŸ“ coverage
@[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