# Documentation

Mathlib.CategoryTheory.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.

@[simp]
theorem CategoryTheory.actionAsFunctor_map (M : Type u_1) [] (X : Type u) [] :
∀ {X Y : } (x : X Y) (x_1 : X), ().map CategoryTheory.CategoryStruct.toQuiver (Type u) CategoryTheory.CategoryStruct.toQuiver ().toPrefunctor X Y x x_1 = x x_1
@[simp]
theorem CategoryTheory.actionAsFunctor_obj (M : Type u_1) [] (X : Type u) [] :
∀ (x : ), ().obj x = X
def CategoryTheory.actionAsFunctor (M : Type u_1) [] (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.

Instances For
def CategoryTheory.ActionCategory (M : Type u_1) [] (X : Type u) [] :

A multiplicative action M ↻ X induces a category structure 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.

Instances For
instance CategoryTheory.instCategoryActionCategory (M : Type u_1) [] (X : Type u) [] :
def CategoryTheory.ActionCategory.π (M : Type u_1) [] (X : Type u) [] :

The projection from the action category to the monoid, mapping a morphism to its label.

Instances For
@[simp]
theorem CategoryTheory.ActionCategory.π_map (M : Type u_1) [] (X : Type u) [] (p : ) (q : ) (f : p q) :
().map f = f
@[simp]
theorem CategoryTheory.ActionCategory.π_obj (M : Type u_1) [] (X : Type u) [] (p : ) :
def CategoryTheory.ActionCategory.back {M : Type u_1} [] {X : Type u} [] :

The canonical map ActionCategory M X → X. It is given by fun x => x.snd, but has a more explicit type.

Instances For
@[simp]
theorem CategoryTheory.ActionCategory.coe_back {M : Type u_1} [] {X : Type u} [] (x : X) :
CategoryTheory.ActionCategory.back { fst := (), snd := x } = x
@[simp]
theorem CategoryTheory.ActionCategory.back_coe {M : Type u_1} [] {X : Type u} [] (x : ) :
{ fst := (), snd := } = x
def CategoryTheory.ActionCategory.objEquiv (M : Type u_1) [] (X : Type u) [] :

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

Instances For
theorem CategoryTheory.ActionCategory.hom_as_subtype (M : Type u_1) [] (X : Type u) [] (p : ) (q : ) :
(p q) =
def CategoryTheory.ActionCategory.stabilizerIsoEnd (M : Type u_1) [] {X : Type u} [] (x : X) :
{ x // } ≃* CategoryTheory.End { fst := (), snd := x }

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

Instances For
@[simp]
theorem CategoryTheory.ActionCategory.stabilizerIsoEnd_apply (M : Type u_1) [] {X : Type u} [] (x : X) (f : { x // }) :
@[simp]
theorem CategoryTheory.ActionCategory.stabilizerIsoEnd_symm_apply (M : Type u_1) [] {X : Type u} [] (x : X) (f : CategoryTheory.End { fst := (), snd := x }) :
@[simp]
theorem CategoryTheory.ActionCategory.id_val {M : Type u_1} [] {X : Type u} [] (x : ) :
@[simp]
theorem CategoryTheory.ActionCategory.comp_val {M : Type u_1} [] {X : Type u} [] {x : } {y : } {z : } (f : x y) (g : y z) :
= g * f
def CategoryTheory.ActionCategory.endMulEquivSubgroup {G : Type u_2} [] (H : ) :
CategoryTheory.End (↑() 1) ≃* { x // x H }

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

Instances For
def CategoryTheory.ActionCategory.homOfPair {X : Type u} {G : Type u_2} [] [] (t : X) (g : G) :
{ fst := (), snd := g⁻¹ t } { fst := (), snd := t }

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

Instances For
@[simp]
theorem CategoryTheory.ActionCategory.homOfPair.val {X : Type u} {G : Type u_2} [] [] (t : X) (g : G) :
def CategoryTheory.ActionCategory.cases {X : Type u} {G : Type u_2} [] [] {P : a b : ⦄ → (a b) → Sort u_3} (hyp : (t : X) → (g : G) → P { fst := (), snd := g⁻¹ t } { fst := (), snd := t } ()) ⦃a : ⦃b : (f : a b) :
P a b f

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

Instances For
theorem CategoryTheory.ActionCategory.cases' {X : Type u} {G : Type u_2} [] [] ⦃a' : ⦃b' : (f : a' b') :
a b g ha hb hg, f = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom (_ : a' = { fst := (), snd := g⁻¹ b })) (CategoryTheory.CategoryStruct.comp () (CategoryTheory.eqToHom (_ : { fst := (), snd := b } = b')))
@[simp]
theorem CategoryTheory.ActionCategory.curry_apply_left {X : Type u} {G : Type u_2} [] [] {H : Type u_3} [] (g : G) (b : X) :
SemidirectProduct.left (XH) G Pi.group inst✝ mulAutArrow () b = F.map ()
@[simp]
theorem CategoryTheory.ActionCategory.curry_apply_right {X : Type u} {G : Type u_2} [] [] {H : Type u_3} [] (g : G) :
().right = g
def CategoryTheory.ActionCategory.curry {X : Type u} {G : Type u_2} [] [] {H : Type u_3} [] :
G →* (XH) ⋊[mulAutArrow] 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.

Instances For
@[simp]
theorem CategoryTheory.ActionCategory.uncurry_map {X : Type u} {G : Type u_2} [] [] {H : Type u_3} [] (F : G →* (XH) ⋊[mulAutArrow] G) (sane : ∀ (g : G), (F g).right = g) :
∀ {x b : } (f : x b), ().map f = SemidirectProduct.left (XH) G Pi.group inst✝ mulAutArrow (F f) ()
@[simp]
theorem CategoryTheory.ActionCategory.uncurry_obj {X : Type u} {G : Type u_2} [] [] {H : Type u_3} [] (F : G →* (XH) ⋊[mulAutArrow] G) (sane : ∀ (g : G), (F g).right = g) :
∀ (x : ), ().obj x = ()
def CategoryTheory.ActionCategory.uncurry {X : Type u} {G : Type u_2} [] [] {H : Type u_3} [] (F : G →* (XH) ⋊[mulAutArrow] 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.

Instances For