Theorems · Definition · category theory

CategoryTheory.Functor.mapActionCongr

{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] → {F F' : CategoryTheory.Functor V W} → (F ≅ F') → (F.mapAction G ≅ F'.mapAction G)

Functor.mapAction preserves isomorphisms of functors.

Defined in

Mathlib.CategoryTheory.Action.Basic

Cited by

2 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryCategoryTheory.CategoryMonoid