Documentation

Mathlib.CategoryTheory.Localization.Preadditive

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] :
liftNatTrans L W F₁ F₂ F₁' F₂' 0 = 0
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₂' τ'