The center of a category

Given a category C, we introduce an abbreviation CatCenter C for the center of the category C, which is End (𝟭 C), the type of endomorphisms of the identity functor of C.

References

• https://ncatlab.org/nlab/show/center+of+a+category

@[reducible, inline]

abbrev CategoryTheory.CatCenter (C : Type u) [Category.{v, u} C] : Type (max u v)

The center of a category C is the type End (𝟭 C) of the endomorphisms of the identify functor of C.

Equations

• CategoryTheory.CatCenter C = CategoryTheory.End (CategoryTheory.Functor.id C)

theorem CategoryTheory.CatCenter.ext {C : Type u} [Category.{v, u} C] (x y : CatCenter C) (h : ∀ (X : C), x.app X = y.app X) : x = y

theorem CategoryTheory.CatCenter.ext_iff {C : Type u} [Category.{v, u} C] {x y : CatCenter C} : x = y ↔ ∀ (X : C), x.app X = y.app X

theorem CategoryTheory.CatCenter.mul_app' {C : Type u} [Category.{v, u} C] (x y : CatCenter C) (X : C) : (x * y).app X = CategoryStruct.comp (y.app X) (x.app X)

theorem CategoryTheory.CatCenter.mul_app'_assoc {C : Type u} [Category.{v, u} C] (x y : CatCenter C) (X : C) {Z : C} (h : X ⟶ Z) : CategoryStruct.comp ((x * y).app X) h = CategoryStruct.comp (y.app X) (CategoryStruct.comp (x.app X) h)

theorem CategoryTheory.CatCenter.mul_app {C : Type u} [Category.{v, u} C] (x y : CatCenter C) (X : C) : (x * y).app X = CategoryStruct.comp (x.app X) (y.app X)

theorem CategoryTheory.CatCenter.mul_app_assoc {C : Type u} [Category.{v, u} C] (x y : CatCenter C) (X : C) {Z : C} (h : X ⟶ Z) : CategoryStruct.comp ((x * y).app X) h = CategoryStruct.comp (x.app X) (CategoryStruct.comp (y.app X) h)

instance CategoryTheory.CatCenter.instIsMulCommutative {C : Type u} [Category.{v, u} C] : IsMulCommutative (CatCenter C)