Theorems · Theorem · category theory

CategoryTheory.Localization.functor_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)
  [inst_5 : L.IsLocalization W] [inst_6 : L.Additive] [inst_7 : CategoryTheory.Linear R C],
  CategoryTheory.Functor.Linear R L

Defined in

Mathlib.CategoryTheory.Localization.Linear

Cited by

0 results in Mathlib

Foundations

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

Assumes

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