Theorems · Definition · category theory

Action.mkIso

{V : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} V] →
    {G : Type u_2} →
      [inst_1 : Monoid G] →
        {M N : Action V G} →
          (f : M.V ≅ N.V) →
            autoParam
                (∀ (g : G),
                  CategoryTheory.CategoryStruct.comp (M.ρ g) f.hom = CategoryTheory.CategoryStruct.comp f.hom (N.ρ g))
                Action.mkIso._auto_1 →
              (M ≅ N)

Construct an isomorphism of G actions/representations from an isomorphism of the underlying objects, where the forward direction commutes with the group action.

Defined in

Mathlib.CategoryTheory.Action.Basic

Cited by

14 results in Mathlib

Foundations

Depth 21 from the axioms · uses propext, Quot.sound

Assumes

CategoryTheory.CategoryMonoid