Theorems · Definition · category theory

CategoryTheory.ActionCategory

(M : Type u_1) → [inst : Monoid M] → (X : Type u) → [MulAction M X] → Type (max 0 u)

A multiplicative action M ↻ X induces a category structure on X, where a morphism from x to y is a scalar taking x to y. Due to implementation details, the object type of this category is not equal to X, but is in bijection with X.

Defined in

Mathlib.CategoryTheory.Action

Cited by

12 results in Mathlib

Foundations

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

Assumes

MonoidMulAction