Theorems · Theorem · category theory

CategoryTheory.Localization.functor_linear_iff

∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  [inst_2 : CategoryTheory.Preadditive C] [inst_3 : CategoryTheory.Preadditive D] {E : Type u_1}
  [inst_4 : CategoryTheory.Category.{v_1, u_1} E] (L : CategoryTheory.Functor C D)
  (W : CategoryTheory.MorphismProperty C) [L.IsLocalization W] [inst_6 : CategoryTheory.Preadditive E] (R : Type u_2)
  [inst_7 : Ring R] [inst_8 : CategoryTheory.Linear R C] [inst_9 : CategoryTheory.Linear R D]
  [inst_10 : CategoryTheory.Linear R E] [CategoryTheory.Functor.Linear R L] (F : CategoryTheory.Functor C E)
  (G : CategoryTheory.Functor D E) [CategoryTheory.Localization.Lifting L W F G],
  CategoryTheory.Functor.Linear R F ↔ CategoryTheory.Functor.Linear R G

Defined in

Mathlib.CategoryTheory.Localization.Linear

Cited by

1 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryCategoryTheory.CategoryCategoryTheory.PreadditiveCategoryTheory.PreadditiveCategoryTheory.CategoryCategoryTheory.Functor.IsLocalizationCategoryTheory.PreadditiveRingCategoryTheory.LinearCategoryTheory.LinearCategoryTheory.LinearCategoryTheory.Functor.LinearCategoryTheory.Localization.Lifting