Theorems · Definition · category theory

CategoryTheory.Localization.linear

(R : Type w) →
  [inst : Ring R] →
    {C : Type u₁} →
      [inst_1 : CategoryTheory.Category.{v₁, u₁} C] →
        {D : Type u₂} →
          [inst_2 : CategoryTheory.Category.{v₂, u₂} D] →
            [inst_3 : CategoryTheory.Preadditive C] →
              [inst_4 : CategoryTheory.Preadditive D] →
                (L : CategoryTheory.Functor C D) →
                  (W : CategoryTheory.MorphismProperty C) →
                    [L.IsLocalization W] → [L.Additive] → [CategoryTheory.Linear R C] → CategoryTheory.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.

Defined in

Mathlib.CategoryTheory.Localization.Linear

Cited by

1 results in Mathlib

Foundations

Depth 83 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

RingCategoryTheory.CategoryCategoryTheory.CategoryCategoryTheory.PreadditiveCategoryTheory.PreadditiveCategoryTheory.Functor.IsLocalizationCategoryTheory.Functor.AdditiveCategoryTheory.Linear