Localization of natural transformations to preadditive categories #
theorem
CategoryTheory.Localization.liftNatTrans_zero
{C : Type u_1}
{D : Type u_2}
{E : Type u_3}
[Category.{u_4, u_1} C]
[Category.{u_6, u_2} D]
[Category.{u_5, u_3} E]
(L : Functor C D)
(W : MorphismProperty C)
[L.IsLocalization W]
(F₁ F₂ : Functor C E)
(F₁' F₂' : Functor D E)
[Lifting L W F₁ F₁']
[Lifting L W F₂ F₂']
[Limits.HasZeroMorphisms E]
:
theorem
CategoryTheory.Localization.liftNatTrans_add
{C : Type u_1}
{D : Type u_2}
{E : Type u_3}
[Category.{u_4, u_1} C]
[Category.{u_6, u_2} D]
[Category.{u_5, u_3} E]
(L : Functor C D)
(W : MorphismProperty C)
[L.IsLocalization W]
[Preadditive E]
(F₁ F₂ : Functor C E)
(F₁' F₂' : Functor D E)
[Lifting L W F₁ F₁']
[Lifting L W F₂ F₂']
(τ τ' : F₁ ⟶ F₂)
:
liftNatTrans L W F₁ F₂ F₁' F₂' (τ + τ') = liftNatTrans L W F₁ F₂ F₁' F₂' τ + liftNatTrans L W F₁ F₂ F₁' F₂' τ'