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
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
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
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
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
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.{u_3, 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]
: