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) :
def category_theory.action_category.back {M : Type u_1} [monoid M] {X : Type u} [mul_action M X] :

The canonical map action_category M X → X. It is given by λ x, x.snd, but has a more explicit type.

Equations
@[instance]
Equations
@[simp]
theorem category_theory.action_category.coe_back {M : Type u_1} [monoid M] {X : Type u} [mul_action M X] (x : X) :
@[simp]
theorem category_theory.action_category.back_coe {M : Type u_1} [monoid M] {X : Type u} [mul_action M X] (x : category_theory.action_category M X) :
(x.back) = 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) [mul_action M X] (p q : category_theory.action_category M X) :
(p q) = {m // m p.back = q.back}
@[instance]

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.id_val {M : Type u_1} [monoid M] {X : Type u} [mul_action M X] (x : category_theory.action_category M X) :
(𝟙 x).val = 1
@[simp]
theorem category_theory.action_category.comp_val {M : Type u_1} [monoid M] {X : Type u} [mul_action M X] {x y z : category_theory.action_category M X} (f : x y) (g : y z) :
(f g).val = (g.val) * f.val
def category_theory.action_category.hom_of_pair {X : Type u} {G : Type u_2} [group G] [mul_action G X] (t : X) (g : G) :

A target vertex t and a scalar g determine a morphism in the action groupoid.

Equations
@[simp]
theorem category_theory.action_category.hom_of_pair.val {X : Type u} {G : Type u_2} [group G] [mul_action G X] (t : X) (g : G) :
def category_theory.action_category.cases {X : Type u} {G : Type u_2} [group G] [mul_action G X] {P : Π ⦃a b : category_theory.action_category G X⦄, (a b)Sort u_1} (hyp : Π (t : X) (g : G), P (category_theory.action_category.hom_of_pair t g)) ⦃a b : category_theory.action_category G X⦄ (f : a b) :
P f

Any morphism in the action groupoid is given by some pair.

Equations
def category_theory.action_category.curry {X : Type u} {G : Type u_2} [group G] [mul_action G X] {H : Type u_3} [group H] (F : category_theory.action_category G X category_theory.single_obj H) :
G →* (X → H) ⋊[mul_aut_arrow] G

Given G acting on X, a functor from the corresponding action groupoid to a group H can be curried to a group homomorphism G →* (X → H) ⋊ G.

Equations
@[simp]
theorem category_theory.action_category.uncurry_map {X : Type u} {G : Type u_2} [group G] [mul_action G X] {H : Type u_3} [group H] (F : G →* (X → H) ⋊[mul_aut_arrow] G) (sane : ∀ (g : G), (F g).right = g) (a b : category_theory.action_category G X) (f : a b) :
def category_theory.action_category.uncurry {X : Type u} {G : Type u_2} [group G] [mul_action G X] {H : Type u_3} [group H] (F : G →* (X → H) ⋊[mul_aut_arrow] G) (sane : ∀ (g : G), (F g).right = g) :

Given 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 g.

Equations
@[simp]
theorem category_theory.action_category.uncurry_obj {X : Type u} {G : Type u_2} [group G] [mul_action G X] {H : Type u_3} [group H] (F : G →* (X → H) ⋊[mul_aut_arrow] G) (sane : ∀ (g : G), (F g).right = g) (_x : category_theory.action_category G X) :