Theorems · Theorem · category theory

CategoryTheory.Functor.ShiftSequence.shiftIso_zero

∀ {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] (a : M),
  CategoryTheory.Functor.ShiftSequence.shiftIso 0 a a ⋯ =
    CategoryTheory.Functor.isoWhiskerRight (CategoryTheory.shiftFunctorZero C M)
        (CategoryTheory.Functor.ShiftSequence.sequence F a) ≪≫
      (CategoryTheory.Functor.ShiftSequence.sequence F a).leftUnitor

Defined in

Mathlib.CategoryTheory.Shift.ShiftSequence

Cited by

1 results in Mathlib

Foundations

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

Assumes

CategoryTheory.Functor.ShiftSequence