Theorems · Theorem · category theory

CategoryTheory.ActionCategory.curry_apply_left

∀ {X : Type u} {G : Type u_2} [inst : Group G] [inst_1 : MulAction G X] {H : Type u_3} [inst_2 : Group H]
  (F : CategoryTheory.Functor (CategoryTheory.ActionCategory G X) (CategoryTheory.SingleObj H)) (g : G) (b : X),
  ((CategoryTheory.ActionCategory.curry F) g).left b = F.map (CategoryTheory.ActionCategory.homOfPair b g)

Defined in

Mathlib.CategoryTheory.Action

Cited by

0 results in Mathlib

Foundations

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

Assumes

GroupMulActionGroup