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
multiplication by m.
This functor induces a category structure on X -- a special case of the category of elements.
A morphism 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 m.
Equations
- category_theory.action_as_functor M X = {obj := λ (_x : category_theory.single_obj M), X, map := λ (_x _x_1 : category_theory.single_obj M), has_scalar.smul, map_id' := _, map_comp' := _}
A multiplicative action M ↻ X induces a category strucure 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.
Equations
The projection from the action category to the monoid, mapping a morphism to its label.
An object of the action category given by M ↻ X corresponds to an element of X.
Equations
- category_theory.action_category.obj_equiv M X = {to_fun := λ (x : X), ⟨category_theory.single_obj.star M, x⟩, inv_fun := λ (p : category_theory.action_category M X), p.snd, left_inv := _, right_inv := _}
Equations
The stabilizer of a point is isomorphic to the endomorphism monoid at the corresponding point. In fact they are definitionally equivalent.