Documentation

Mathlib.CategoryTheory.Localization.Linear

Localization of linear categories #

If L : C ⥤ D is an additive localization functor between preadditive categories, and C is R-linear, we show that D can also be equipped with an R-linear structure such that L is an R-linear functor.

@[instance_reducible]

noncomputable def CategoryTheory.Localization.linear (R : Type w) [Ring R] {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] [Preadditive C] [Preadditive D] (L : Functor C D) (W : MorphismProperty C) [L.IsLocalization W] [L.Additive] [Linear R C] :

If L : C ⥤ D is a localization functor and C is R-linear, then D is R-linear if we already know that D is preadditive and L is additive.

Equations

CategoryTheory.Localization.linear R L W = CategoryTheory.Linear.ofRingMorphism ((CategoryTheory.CatCenter.localizationRingHom L W).comp (CategoryTheory.Linear.toCatCenter R C))

Instances For

theorem CategoryTheory.Localization.functor_linear (R : Type w) [Ring R] {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] [Preadditive C] [Preadditive D] (L : Functor C D) (W : MorphismProperty C) [L.IsLocalization W] [L.Additive] [Linear R C] :

Functor.Linear R L

@[instance_reducible]

noncomputable instance CategoryTheory.Localization.instLinearLocalization (R : Type w) [Ring R] {C : Type u₁} [Category.{v₁, u₁} C] [Preadditive C] (W : MorphismProperty C) [Linear R C] [Preadditive W.Localization] [W.Q.Additive] :

Linear R W.Localization

Equations

CategoryTheory.Localization.instLinearLocalization R W = CategoryTheory.Localization.linear R W.Q W

instance CategoryTheory.Localization.instLinearLocalizationQ (R : Type w) [Ring R] {C : Type u₁} [Category.{v₁, u₁} C] [Preadditive C] (W : MorphismProperty C) [Linear R C] [Preadditive W.Localization] [W.Q.Additive] :

Functor.Linear R W.Q

@[instance_reducible]

noncomputable instance CategoryTheory.Localization.instLinearLocalization' (R : Type w) [Ring R] {C : Type u₁} [Category.{v₁, u₁} C] [Preadditive C] (W : MorphismProperty C) [Linear R C] [W.HasLocalization] [Preadditive W.Localization'] [W.Q'.Additive] :

Linear R W.Localization'

Equations

CategoryTheory.Localization.instLinearLocalization' R W = CategoryTheory.Localization.linear R W.Q' W

instance CategoryTheory.Localization.instLinearLocalization'Q' (R : Type w) [Ring R] {C : Type u₁} [Category.{v₁, u₁} C] [Preadditive C] (W : MorphismProperty C) [Linear R C] [W.HasLocalization] [Preadditive W.Localization'] [W.Q'.Additive] :

Functor.Linear R W.Q'

theorem CategoryTheory.Localization.functor_linear_iff {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] [Preadditive C] [Preadditive D] {E : Type u_1} [Category.{v_1, u_1} E] (L : Functor C D) (W : MorphismProperty C) [L.IsLocalization W] [Preadditive E] (R : Type u_2) [Ring R] [Linear R C] [Linear R D] [Linear R E] [Functor.Linear R L] (F : Functor C E) (G : Functor D E) [Lifting L W F G] :

Functor.Linear R F ↔ Functor.Linear R G