Theorems · Definition · category theory

CategoryTheory.Functor.ShiftSequence.shiftIso

{C : Type u_1} →
  {A : Type u_3} →
    {inst : CategoryTheory.Category.{v_1, u_1} C} →
      {inst_1 : CategoryTheory.Category.{v_3, u_3} A} →
        {F : CategoryTheory.Functor C A} →
          {M : Type u_4} →
            {inst_2 : AddMonoid M} →
              {inst_3 : CategoryTheory.HasShift C M} →
                [self : F.ShiftSequence M] →
                  (n a a' : M) →
                    n + a = a' →
                      ((CategoryTheory.shiftFunctor C n).comp (CategoryTheory.Functor.ShiftSequence.sequence F a) ≅
                        CategoryTheory.Functor.ShiftSequence.sequence F a')

compatibility isomorphism with the shift

Defined in

Mathlib.CategoryTheory.Shift.ShiftSequence

Cited by

3 results in Mathlib

Foundations

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

Assumes

CategoryTheory.Functor.ShiftSequence