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
@[protected, instance]
def category_theory.action_category.category (M : Type u_1) [monoid M] (X : Type u) [ X] :
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) :
@[protected]
def category_theory.action_category.back {M : Type u_1} [monoid M] {X : Type u} [ 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]
def category_theory.action_category.has_coe_t {M : Type u_1} [monoid M] {X : Type u} [ X] :
Equations
@[simp]
theorem category_theory.action_category.coe_back {M : Type u_1} [monoid M] {X : Type u} [ X] (x : X) :
@[simp]
theorem category_theory.action_category.back_coe {M : Type u_1} [monoid M] {X : Type u} [ X] (x : X) :
(x.back) = 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 p.back = q.back}
@[protected, instance]
def category_theory.action_category.inhabited (M : Type u_1) [monoid M] (X : Type u) [ X] [inhabited X] :
Equations
@[protected, instance]
def category_theory.action_category.nonempty (M : Type u_1) [monoid M] (X : Type u) [ X] [nonempty X] :
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) (f : category_theory.End x) :
@[protected, simp]
theorem category_theory.action_category.id_val {M : Type u_1} [monoid M] {X : Type u} [ X] (x : X) :
(𝟙 x).val = 1
@[protected, simp]
theorem category_theory.action_category.comp_val {M : Type u_1} [monoid M] {X : Type u} [ X] {x y z : X} (f : x y) (g : y z) :
(f g).val = (g.val) * f.val
@[protected, instance]
def category_theory.action_category.category_theory.is_connected {M : Type u_1} [monoid M] {X : Type u} [ X] [nonempty X] :
@[protected, instance]
noncomputable def category_theory.action_category.category_theory.groupoid {X : Type u} {G : Type u_2} [group G] [ X] :
Equations

Any subgroup of G is a vertex group in its action groupoid.

Equations
def category_theory.action_category.hom_of_pair {X : Type u} {G : Type u_2} [group 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] [ X] (t : X) (g : G) :
@[protected]
def category_theory.action_category.cases {X : Type u} {G : Type u_2} [group G] [ X] {P : Π ⦃a b : ⦄, (a b)Sort u_1} (hyp : Π (t : X) (g : G), ) ⦃a b : X⦄ (f : a b) :
P f

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

Equations
@[simp]
theorem category_theory.action_category.curry_apply_left {X : Type u} {G : Type u_2} [group G] [ X] {H : Type u_3} [group H] (g : G) (b : X) :
def category_theory.action_category.curry {X : Type u} {G : Type u_2} [group G] [ X] {H : Type u_3} [group 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.curry_apply_right {X : Type u} {G : Type u_2} [group G] [ X] {H : Type u_3} [group H] (g : G) :
@[simp]
theorem category_theory.action_category.uncurry_map {X : Type u} {G : Type u_2} [group 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 : X) (f : a b) :
f = (F f.val).left b.back
def category_theory.action_category.uncurry {X : Type u} {G : Type u_2} [group 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] [ X] {H : Type u_3} [group H] (F : G →* (X → H) ⋊[mul_aut_arrow] G) (sane : ∀ (g : G), (F g).right = g) (_x : X) :
_x = ()