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 a R-linear structure such that L is a R-linear functor.

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] :
Linear R D

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
Instances For