Theorems · Definition · category theory

CategoryTheory.Functor.CommShift.commShiftIso

{C : Type u_1} →
  {D : Type u_2} →
    {inst : CategoryTheory.Category.{v_1, u_1} C} →
      {inst_1 : CategoryTheory.Category.{v_2, u_2} D} →
        (F : CategoryTheory.Functor C D) →
          {A : Type u_6} →
            {inst_2 : AddMonoid A} →
              {inst_3 : CategoryTheory.HasShift C A} →
                {inst_4 : CategoryTheory.HasShift D A} →
                  [self : F.CommShift A] →
                    (a : A) → (CategoryTheory.shiftFunctor C a).comp F ≅ F.comp (CategoryTheory.shiftFunctor D a)

The commutation isomorphisms for all a-shifts this functor is equipped with

Defined in

Mathlib.CategoryTheory.Shift.CommShift

Cited by

202 results in Mathlib

Foundations

Depth 23 from the axioms, rests on 126 definitions · uses propext, Classical.choice, Quot.sound

Assumes

CategoryTheory.Functor.CommShift