Theorems · Definition · category theory

CategoryTheory.ActionCategory.curry

{X : Type u} →
  {G : Type u_2} →
    [inst : Group G] →
      [inst_1 : MulAction G X] →
        {H : Type u_3} →
          [inst_2 : Group H] →
            CategoryTheory.Functor (CategoryTheory.ActionCategory G X) (CategoryTheory.SingleObj H) →
              G →* (X → H) ⋊[mulAutArrow] G

Given G acting on X, a functor from the corresponding action groupoid to a group H can be curried to a group homomorphism G →* (X → H) ⋊ G.

Defined in

Mathlib.CategoryTheory.Action

Cited by

2 results in Mathlib

Foundations

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

Assumes

GroupMulActionGroup