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)

@[reducible, inline]

abbrev CategoryTheory.CatCenter.app {C : Type u} [Category.{v, u} C] (x : CatCenter C) (X : C) : X ⟶ X

The action of the center of a category on an object. (This is necessary as NatTrans.app x X is syntactically an endomorphism of (𝟭 C).obj X rather than of X.)

Equations

• x.app X = x.asHom.app X

@[simp]

theorem CategoryTheory.CatCenter.app_one {C : Type u} [Category.{v, u} C] (X : C) : app 1 X = CategoryStruct.id X

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.naturality {C : Type u} [Category.{v, u} C] (z : CatCenter C) {X Y : C} (f : X ⟶ Y) : CategoryStruct.comp f (z.app Y) = CategoryStruct.comp (z.app X) f

theorem CategoryTheory.CatCenter.naturality_assoc {C : Type u} [Category.{v, u} C] (z : CatCenter C) {X Y : C} (f : X ⟶ Y) {Z : C} (h : Y ⟶ Z) : CategoryStruct.comp f (CategoryStruct.comp (z.app Y) h) = CategoryStruct.comp (z.app X) (CategoryStruct.comp f 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 (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)

@[instance_reducible]

instance CategoryTheory.CatCenter.instSMulHom {C : Type u} [Category.{v, u} C] {X Y : C} : SMul (CatCenter C) (X ⟶ Y)

Equations

• CategoryTheory.CatCenter.instSMulHom = { smul := fun (z : CategoryTheory.CatCenter C) (f : X ⟶ Y) => CategoryTheory.CategoryStruct.comp f (z.app Y) }

theorem CategoryTheory.CatCenter.smul_eq {C : Type u} [Category.{v, u} C] (z : CatCenter C) {X Y : C} (f : X ⟶ Y) : z • f = CategoryStruct.comp f (z.app Y)

theorem CategoryTheory.CatCenter.smul_eq' {C : Type u} [Category.{v, u} C] (z : CatCenter C) {X Y : C} (f : X ⟶ Y) : z • f = CategoryStruct.comp (z.app X) f

@[instance_reducible]

instance CategoryTheory.CatCenter.instSMulUnitsIso {C : Type u} [Category.{v, u} C] {X Y : C} : SMul (CatCenter C)ˣ (X ≅ Y)

Equations

• CategoryTheory.CatCenter.instSMulUnitsIso = { smul := fun (z : (CategoryTheory.CatCenter C)ˣ) (e : X ≅ Y) => { hom := ↑z • e.hom, inv := ↑z⁻¹ • e.inv, hom_inv_id := ⋯, inv_hom_id := ⋯ } }

theorem CategoryTheory.CatCenter.smul_iso_hom_eq {C : Type u} [Category.{v, u} C] (z : (CatCenter C)ˣ) {X Y : C} (f : X ≅ Y) : (z • f).hom = CategoryStruct.comp f.hom ((↑z).app Y)

theorem CategoryTheory.CatCenter.smul_iso_hom_eq_assoc {C : Type u} [Category.{v, u} C] (z : (CatCenter C)ˣ) {X Y : C} (f : X ≅ Y) {Z : C} (h : Y ⟶ Z) : CategoryStruct.comp (z • f).hom h = CategoryStruct.comp f.hom (CategoryStruct.comp ((↑z).app Y) h)

theorem CategoryTheory.CatCenter.smul_iso_hom_eq' {C : Type u} [Category.{v, u} C] (z : (CatCenter C)ˣ) {X Y : C} (f : X ≅ Y) : (z • f).hom = CategoryStruct.comp ((↑z).app X) f.hom

theorem CategoryTheory.CatCenter.smul_iso_hom_eq'_assoc {C : Type u} [Category.{v, u} C] (z : (CatCenter C)ˣ) {X Y : C} (f : X ≅ Y) {Z : C} (h : Y ⟶ Z) : CategoryStruct.comp (z • f).hom h = CategoryStruct.comp ((↑z).app X) (CategoryStruct.comp f.hom h)

theorem CategoryTheory.CatCenter.smul_iso_inv_eq {C : Type u} [Category.{v, u} C] (z : (CatCenter C)ˣ) {X Y : C} (f : X ≅ Y) : (z • f).inv = CategoryStruct.comp f.inv ((↑z⁻¹).app X)

theorem CategoryTheory.CatCenter.smul_iso_inv_eq_assoc {C : Type u} [Category.{v, u} C] (z : (CatCenter C)ˣ) {X Y : C} (f : X ≅ Y) {Z : C} (h : X ⟶ Z) : CategoryStruct.comp (z • f).inv h = CategoryStruct.comp f.inv (CategoryStruct.comp ((↑z⁻¹).app X) h)

theorem CategoryTheory.CatCenter.smul_iso_inv_eq' {C : Type u} [Category.{v, u} C] (z : (CatCenter C)ˣ) {X Y : C} (f : X ≅ Y) : (z • f).inv = CategoryStruct.comp ((↑z⁻¹).app Y) f.inv

theorem CategoryTheory.CatCenter.smul_iso_inv_eq'_assoc {C : Type u} [Category.{v, u} C] (z : (CatCenter C)ˣ) {X Y : C} (f : X ≅ Y) {Z : C} (h : X ⟶ Z) : CategoryStruct.comp (z • f).inv h = CategoryStruct.comp ((↑z⁻¹).app Y) (CategoryStruct.comp f.inv h)