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_1 Y : } (x : X_1 Y) (x_1 : X), .map 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.

Equations
• One or more equations did not get rendered due to their size.
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.

Equations
• = .Elements
Instances For
instance CategoryTheory.instCategoryActionCategory (M : Type u_1) [] (X : Type u) [] :
Equations
• = id inferInstance
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.

Equations
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.

Equations
• x.back = x.snd
Instances For
instance CategoryTheory.ActionCategory.instCoeTC {M : Type u_1} [] {X : Type u} [] :
Equations
• CategoryTheory.ActionCategory.instCoeTC = { coe := fun (x : X) => (), x }
@[simp]
theorem CategoryTheory.ActionCategory.coe_back {M : Type u_1} [] {X : Type u} [] (x : X) :
@[simp]
theorem CategoryTheory.ActionCategory.back_coe {M : Type u_1} [] {X : Type u} [] (x : ) :
(), x.back = 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.

Equations
• = { toFun := fun (x : X) => (), x, invFun := fun (x : ) => x.back, left_inv := , right_inv := }
Instances For
theorem CategoryTheory.ActionCategory.hom_as_subtype (M : Type u_1) [] (X : Type u) [] (p : ) (q : ) :
(p q) = { m : M // m p.back = q.back }
instance CategoryTheory.ActionCategory.instInhabited (M : Type u_1) [] (X : Type u) [] [] :
Equations
• = { default := let_fun this := default; (), this }
instance CategoryTheory.ActionCategory.instNonempty (M : Type u_1) [] (X : Type u) [] [] :
Equations
• =
def CategoryTheory.ActionCategory.stabilizerIsoEnd (M : Type u_1) [] {X : Type u} [] (x : X) :

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

Equations
Instances For
@[simp]
theorem CategoryTheory.ActionCategory.stabilizerIsoEnd_apply (M : Type u_1) [] {X : Type u} [] (x : X) (f : ) :
@[simp]
theorem CategoryTheory.ActionCategory.stabilizerIsoEnd_symm_apply (M : Type u_1) [] {X : Type u} [] (x : X) (f : CategoryTheory.End (), x) :
f = f
@[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
instance CategoryTheory.ActionCategory.instGroupoid {X : Type u} {G : Type u_2} [] [] :
Equations
• CategoryTheory.ActionCategory.instGroupoid =

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

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

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

Equations
• = g,
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) → ) ⦃a : ⦃b : (f : a b) :
P f

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

Equations
• = cast (hyp b.back f)
Instances For
theorem CategoryTheory.ActionCategory.cases' {X : Type u} {G : Type u_2} [] [] ⦃a' : ⦃b' : (f : a' b') :
∃ (a : X) (b : X) (g : G) (ha : a' = (), a) (hb : b' = (), b) (hg : a = g⁻¹ b),
@[simp]
theorem CategoryTheory.ActionCategory.curry_apply_left {X : Type u} {G : Type u_2} [] [] {H : Type u_3} [] (g : G) (b : X) :
.left 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.

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[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 = ()
@[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 = (F f).left b.back
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.

Equations
• One or more equations did not get rendered due to their size.
Instances For