Theorems · Definition · category theory

CategoryTheory.actionAsFunctor

(M : Type u_1) →
  [inst : Monoid M] → (X : Type u) → [MulAction M X] → CategoryTheory.Functor (CategoryTheory.SingleObj M) (Type u)

A multiplicative action M ↻ X viewed as a functor mapping the single object of M to X and an element m : M to the map X → X given by multiplication by m.

Defined in

Mathlib.CategoryTheory.Action

Cited by

12 results in Mathlib

Foundations

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

Assumes

MonoidMulAction