Localization of the center of a category

Given a localization functor L : C ⥤ D with respect to W : MorphismProperty C, we define a localization map CatCenter C → CatCenter D for the centers of these categories. In case L is an additive functor between preadditive categories, we promote this to a ring morphism CatCenter C →+* CatCenter D.

noncomputable def CategoryTheory.CatCenter.localization {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (r : CatCenter C) (L : Functor C D) (W : MorphismProperty C) [L.IsLocalization W] : CatCenter D

Given r : CatCenter C and L : C ⥤ D a localization functor with respect to W : MorphismProperty D, this is the induced element in CatCenter D obtained by localization.

Equations

• r.localization L W = CategoryTheory.Localization.liftNatTrans L W L L (CategoryTheory.Functor.id D) (CategoryTheory.Functor.id D) (CategoryTheory.whiskerRight r L)

@[simp]

theorem CategoryTheory.CatCenter.localization_app {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (r : CatCenter C) (L : Functor C D) (W : MorphismProperty C) [L.IsLocalization W] (X : C) : (r.localization L W).app (L.obj X) = L.map (r.app X)

theorem CategoryTheory.CatCenter.ext_of_localization {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (L : Functor C D) (W : MorphismProperty C) [L.IsLocalization W] (r s : CatCenter D) (h : ∀ (X : C), r.app (L.obj X) = s.app (L.obj X)) : r = s

theorem CategoryTheory.CatCenter.localization_one {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (L : Functor C D) (W : MorphismProperty C) [L.IsLocalization W] : localization 1 L W = 1

theorem CategoryTheory.CatCenter.localization_mul {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (r s : CatCenter C) (L : Functor C D) (W : MorphismProperty C) [L.IsLocalization W] : (r * s).localization L W = r.localization L W * s.localization L W

theorem CategoryTheory.CatCenter.localization_zero {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (L : Functor C D) (W : MorphismProperty C) [L.IsLocalization W] [Preadditive C] [Preadditive D] [L.Additive] : localization 0 L W = 0

theorem CategoryTheory.CatCenter.localization_add {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (r s : CatCenter C) (L : Functor C D) (W : MorphismProperty C) [L.IsLocalization W] [Preadditive C] [Preadditive D] [L.Additive] : (r + s).localization L W = r.localization L W + s.localization L W

noncomputable def CategoryTheory.CatCenter.localizationRingHom {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (L : Functor C D) (W : MorphismProperty C) [L.IsLocalization W] [Preadditive C] [Preadditive D] [L.Additive] : CatCenter C →+* CatCenter D

The morphism of rings CatCenter C →+* CatCenter D when L : C ⥤ D is an additive localization functor between preadditive categories.

Equations

• CategoryTheory.CatCenter.localizationRingHom L W = { toFun := fun (r : CategoryTheory.CatCenter C) => r.localization L W, map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ }