Theorems · Definition · category theory

CategoryTheory.Functor.mapActionComp

{V : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} V] →
    {W : Type u_2} →
      [inst_1 : CategoryTheory.Category.{v_2, u_2} W] →
        (G : Type u_3) →
          [inst_2 : Monoid G] →
            {T : Type u_4} →
              [inst_3 : CategoryTheory.Category.{v_3, u_4} T] →
                (F : CategoryTheory.Functor V W) →
                  (F' : CategoryTheory.Functor W T) → (F.comp F').mapAction G ≅ (F.mapAction G).comp (F'.mapAction G)

Functor.mapAction is functorial in the functor.

Defined in

Mathlib.CategoryTheory.Action.Basic

Cited by

2 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryCategoryTheory.CategoryMonoidCategoryTheory.Category