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
@[protected, instance]

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) :
@[protected]
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
@[protected, 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}
@[protected, instance]
Equations
@[protected, instance]

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

Equations
@[protected, 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
@[protected, 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) :
@[protected]
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) :