Theorems · Theorem · category theory

CategoryTheory.Quotient.functor_obj_shift

∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (r : HomRel C) (A : Type w) [inst_1 : AddMonoid A]
  [inst_2 : CategoryTheory.HasShift C A] [inst_3 : r.IsCompatibleWithShift A] (X : C) (n : A),
  (CategoryTheory.shiftFunctor (CategoryTheory.Quotient r) n).obj ((CategoryTheory.Quotient.functor r).obj X) =
    (CategoryTheory.Quotient.functor r).obj ((CategoryTheory.shiftFunctor C n).obj X)

Defined in

Mathlib.CategoryTheory.Shift.Quotient

Cited by

1 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryAddMonoidCategoryTheory.HasShiftHomRel.IsCompatibleWithShift