Theorems · Definition · category theory

CategoryTheory.ShiftedHom.map

{C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    {D : Type u_2} →
      [inst_1 : CategoryTheory.Category.{v_2, u_2} D] →
        {M : Type u_4} →
          [inst_2 : AddMonoid M] →
            [inst_3 : CategoryTheory.HasShift C M] →
              [inst_4 : CategoryTheory.HasShift D M] →
                {X Y : C} →
                  {a : M} →
                    CategoryTheory.ShiftedHom X Y a →
                      (F : CategoryTheory.Functor C D) →
                        [F.CommShift M] → CategoryTheory.ShiftedHom (F.obj X) (F.obj Y) a

The action on ShiftedHom of a functor which commutes with the shift.

Defined in

Mathlib.CategoryTheory.Shift.ShiftedHom

Cited by

41 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryCategoryTheory.CategoryAddMonoidCategoryTheory.HasShiftCategoryTheory.HasShiftCategoryTheory.Functor.CommShift