# mathlibdocumentation

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) [ X] :
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`.

Equations
@[simp]
theorem category_theory.action_as_functor_obj (M : Type u_1) [monoid M] (X : Type u) [ X] (_x : category_theory.single_obj M) :
_x = X

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

def category_theory.action_category (M : Type u_1) [monoid M] (X : Type u) [ 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
@[instance]
def category_theory.action_category.category (M : Type u_1) [monoid M] (X : Type u) [ X] :

@[instance]
def category_theory.action_category.category_theory.groupoid (X : Type u) (G : Type u_1) [group G] [ X] :

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

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) [ X] (p q : X) (f : p q) :
= f.val

@[simp]
theorem category_theory.action_category.π_obj (M : Type u_1) [monoid M] (X : Type u) [ X] (p : X) :

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

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

Equations
theorem category_theory.action_category.hom_as_subtype (M : Type u_1) [monoid M] (X : Type u) [ X] (p q : X) :
(p q) = {m // m =

@[instance]
def category_theory.action_category.inhabited (M : Type u_1) [monoid M] (X : Type u) [ X] [inhabited X] :

Equations
def category_theory.action_category.stabilizer_iso_End (M : Type u_1) [monoid M] {X : Type u} [ X] (x : X) :

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

Equations
@[simp]
theorem category_theory.action_category.stabilizer_iso_End_apply (M : Type u_1) [monoid M] {X : Type u} [ X] (x : X) (f : ) :

@[simp]
theorem category_theory.action_category.stabilizer_iso_End_symm_apply (M : Type u_1) [monoid M] {X : Type u} [ X] (x : X)  :