Theorems · Definition · category theory

CategoryTheory.Functor.ShiftSequence.isoZero

{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] → CategoryTheory.Functor.ShiftSequence.sequence F 0 ≅ F

sequence 0 identifies to the given functor

Defined in

Mathlib.CategoryTheory.Shift.ShiftSequence

Cited by

1 results in Mathlib

Foundations

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

Assumes

CategoryTheory.Functor.ShiftSequence