Theorems · Definition · category theory

CategoryTheory.ActionCategory.uncurry

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

Given G acting on X, a group homomorphism φ : G →* (X → H) ⋊ G can be uncurried to a functor from the action groupoid to H, provided that φ g = (_, g) for all 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