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] :
category_theory.single_obj M ⥤ 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
- category_theory.action_as_functor M X = {obj := λ (_x : category_theory.single_obj M), X, map := λ (_x _x_1 : category_theory.single_obj M), has_scalar.smul, map_id' := _, map_comp' := _}
@[simp]
theorem
category_theory.action_as_functor_obj
(M : Type u_1)
[monoid M]
(X : Type u)
[mul_action M X]
(_x : category_theory.single_obj M) :
(category_theory.action_as_functor M X).obj _x = X
@[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]
def
category_theory.action_category.category
(M : Type u_1)
[monoid M]
(X : Type u)
[mul_action M X] :
The projection from the action category to the monoid, mapping a morphism to its label.
@[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) :
(category_theory.action_category.π M X).map f = f.val
@[simp]
theorem
category_theory.action_category.π_obj
(M : Type u_1)
[monoid M]
(X : Type u)
[mul_action M X]
(p : category_theory.action_category M X) :
@[protected]
def
category_theory.action_category.back
{M : Type u_1}
[monoid M]
{X : Type u}
[mul_action M X] :
category_theory.action_category M X → X
The canonical map action_category M X → X. It is given by λ x, x.snd, but
has a more explicit type.
Equations
- category_theory.action_category.back = λ (x : category_theory.action_category M X), x.snd
@[protected, instance]
def
category_theory.action_category.has_coe_t
{M : Type u_1}
[monoid M]
{X : Type u}
[mul_action M X] :
@[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) :
def
category_theory.action_category.obj_equiv
(M : Type u_1)
[monoid M]
(X : Type u)
[mul_action M X] :
An object of the action category given by M ↻ X corresponds to an element of X.
Equations
- category_theory.action_category.obj_equiv M X = {to_fun := coe coe_to_lift, inv_fun := λ (x : category_theory.action_category M X), x.back, left_inv := _, right_inv := _}
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) :
@[protected, instance]
def
category_theory.action_category.inhabited
(M : Type u_1)
[monoid M]
(X : Type u)
[mul_action M X]
[inhabited X] :
@[protected, instance]
def
category_theory.action_category.nonempty
(M : Type u_1)
[monoid M]
(X : Type u)
[mul_action M X]
[nonempty X] :
def
category_theory.action_category.stabilizer_iso_End
(M : Type u_1)
[monoid M]
{X : Type u}
[mul_action M X]
(x : X) :
The stabilizer of a point is isomorphic to the endomorphism monoid at the corresponding point. In fact they are definitionally equivalent.
@[simp]
theorem
category_theory.action_category.stabilizer_iso_End_apply
(M : Type u_1)
[monoid M]
{X : Type u}
[mul_action M X]
(x : X)
(f : ↥(mul_action.stabilizer.submonoid M x)) :
@[simp]
theorem
category_theory.action_category.stabilizer_iso_End_symm_apply
(M : Type u_1)
[monoid M]
{X : Type u}
[mul_action M 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}
[mul_action M X]
(x : category_theory.action_category M X) :
@[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) :
@[protected, instance]
def
category_theory.action_category.category_theory.is_connected
{M : Type u_1}
[monoid M]
{X : Type u}
[mul_action M X]
[mul_action.is_pretransitive M X]
[nonempty X] :
@[protected, instance]
noncomputable
def
category_theory.action_category.category_theory.groupoid
{X : Type u}
{G : Type u_2}
[group G]
[mul_action G X] :
def
category_theory.action_category.End_mul_equiv_subgroup
{G : Type u_2}
[group G]
(H : subgroup G) :
category_theory.End (⇑(category_theory.action_category.obj_equiv G (G ⧸ H)) ↑1) ≃* ↥H
Any subgroup of G is a vertex group in its action groupoid.
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
- category_theory.action_category.cases hyp f = cast _ (hyp b.back f.val)
@[simp]
theorem
category_theory.action_category.curry_apply_left
{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 : G)
(b : X) :
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
- category_theory.action_category.curry F = have F_map_eq : ∀ {a b : category_theory.action_category G X} {f : a ⟶ b}, F.map f = F.map (category_theory.action_category.hom_of_pair b.back f.val), from _, {to_fun := λ (g : G), ⟨λ (b : X), F.map (category_theory.action_category.hom_of_pair b g), g⟩, map_one' := _, map_mul' := _}
@[simp]
theorem
category_theory.action_category.curry_apply_right
{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 : G) :
(⇑(category_theory.action_category.curry F) g).right = g
@[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
- category_theory.action_category.uncurry F sane = {obj := λ (_x : category_theory.action_category G X), (), map := λ (a b : category_theory.action_category G X) (f : a ⟶ b), (⇑F f.val).left b.back, map_id' := _, map_comp' := _}
@[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) :
(category_theory.action_category.uncurry F sane).obj _x = ()