Actions as functors and as categories #
From a multiplicative action M ↻ X, we can construct a functor from M to the category of
types, mapping the single object of M to X and an element
m : M to map
X → X given by
This functor induces a category structure on X -- a special case of the category of elements.
x ⟶ y in this category is simply a scalar
m : M such that
m • x = y. In the case
where M is a group, this category is a groupoid -- the action groupoid.
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
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.
The stabilizer of a point is isomorphic to the endomorphism monoid at the corresponding point. In fact they are definitionally equivalent.
Any morphism in the action groupoid is given by some pair.
G acting on
X, a functor from the corresponding action groupoid to a group
can be curried to a group homomorphism
G →* (X → H) ⋊ G.
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