mathlib documentation

category_theory.action

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'.

def category_theory.action_as_functor (M : Type u_1) [monoid M] (X : Type u) [mul_action M X] :

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
@[simp]

@[simp]
theorem category_theory.action_as_functor_map (M : Type u_1) [monoid M] (X : Type u) [mul_action M X] (_x _x_1 : category_theory.single_obj M) (ᾰ : _x _x_1) (ᾰ_1 : X) :
(category_theory.action_as_functor M X).map ᾰ_1 = ᾰ_1

def category_theory.action_category (M : Type u_1) [monoid M] (X : Type u) [mul_action M X] :
Type u

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.

Equations
@[simp]
theorem category_theory.action_category.π_map (M : Type u_1) [monoid M] (X : Type u) [mul_action M X] (p q : category_theory.action_category M X) (f : p q) :

An object of the action category given by M ↻ X corresponds to an element of X.

Equations

The stabilizer of a point is isomorphic to the endomorphism monoid at the corresponding point. In fact they are definitionally equivalent.

Equations