Theorems · Theorem · category theory

CategoryTheory.Shift.linear_of_localization

∀ (R : Type u_1) [inst : Ring R] {C : Type u_4} [inst_1 : CategoryTheory.Category.{v_1, u_4} C]
  [inst_2 : CategoryTheory.Preadditive C] [inst_3 : CategoryTheory.Linear R C] {D : Type u_2}
  [inst_4 : CategoryTheory.Category.{v_2, u_2} D] [inst_5 : CategoryTheory.Preadditive D]
  [inst_6 : CategoryTheory.Linear R D] {M : Type u_3} [inst_7 : AddMonoid M] [inst_8 : CategoryTheory.HasShift C M]
  [∀ (n : M), CategoryTheory.Functor.Linear R (CategoryTheory.shiftFunctor C n)] (L : CategoryTheory.Functor C D)
  (W : CategoryTheory.MorphismProperty C) [L.IsLocalization W] [CategoryTheory.Functor.Linear R L]
  [inst_12 : CategoryTheory.HasShift D M] [L.CommShift M] (n : M),
  CategoryTheory.Functor.Linear R (CategoryTheory.shiftFunctor D n)

Defined in

Mathlib.CategoryTheory.Shift.Linear

Cited by

0 results in Mathlib

Foundations

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

Assumes

RingCategoryTheory.CategoryCategoryTheory.PreadditiveCategoryTheory.LinearCategoryTheory.CategoryCategoryTheory.PreadditiveCategoryTheory.LinearAddMonoidCategoryTheory.HasShiftCategoryTheory.Functor.LinearCategoryTheory.Functor.IsLocalizationCategoryTheory.Functor.LinearCategoryTheory.HasShiftCategoryTheory.Functor.CommShift