Theorems · Definition · category theory

CategoryTheory.ActionCategory.cases

{X : Type u} →
  {G : Type u_2} →
    [inst : Group G] →
      [inst_1 : MulAction G X] →
        {P : ⦃a b : CategoryTheory.ActionCategory G X⦄ → (a ⟶ b) → Sort u_3} →
          ((t : X) → (g : G) → P (CategoryTheory.ActionCategory.homOfPair t g)) →
            ⦃a b : CategoryTheory.ActionCategory G X⦄ → (f : a ⟶ b) → P f

Any morphism in the action groupoid is given by some pair.

Defined in

Mathlib.CategoryTheory.Action

Cited by

0 results in Mathlib

Foundations

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

Assumes

GroupMulAction