mathlib3 documentation

category_theory.action

Actions as functors and as categories #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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

source
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
source
@[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
source
@[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
source
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
Instances for category_theory.action_category
source
@[protected, instance]
def category_theory.action_category.category (M : Type u_1) [monoid M] (X : Type u) [mul_action M X] :
category_theory.category (category_theory.action_category M X)
source
def category_theory.action_category.π (M : Type u_1) [monoid M] (X : Type u) [mul_action M X] :
category_theory.action_category M X ⥤ category_theory.single_obj M

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

Equations
source
@[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
source
@[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) :
(category_theory.action_category.π M X).obj p = category_theory.single_obj.star M
source
@[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
source
@[protected, instance]
def category_theory.action_category.has_coe_t {M : Type u_1} [monoid M] {X : Type u} [mul_action M X] :
has_coe_t X (category_theory.action_category M X)
Equations
source
@[simp]
theorem category_theory.action_category.coe_back {M : Type u_1} [monoid M] {X : Type u} [mul_action M X] (x : X) :
↑x.back = x
source
@[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
source
def category_theory.action_category.obj_equiv (M : Type u_1) [monoid M] (X : Type u) [mul_action M X] :
X ≃ category_theory.action_category M X

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

Equations
source
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}
source
@[protected, instance]
def category_theory.action_category.inhabited (M : Type u_1) [monoid M] (X : Type u) [mul_action M X] [inhabited X] :
inhabited (category_theory.action_category M X)
Equations
source
@[protected, instance]
def category_theory.action_category.nonempty (M : Type u_1) [monoid M] (X : Type u) [mul_action M X] [nonempty X] :
nonempty (category_theory.action_category M X)
source
def category_theory.action_category.stabilizer_iso_End (M : Type u_1) [monoid M] {X : Type u} [mul_action M X] (x : X) :
↥(mul_action.stabilizer.submonoid M x) ≃* category_theory.End ↑x

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

Equations
source
@[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)) :
(category_theory.action_category.stabilizer_iso_End M x).to_fun f = f
source
@[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) :
(category_theory.action_category.stabilizer_iso_End M x).inv_fun f = f
source
@[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
source
@[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
source
@[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] :
category_theory.is_connected (category_theory.action_category M X)
source
@[protected, instance]
noncomputable def category_theory.action_category.category_theory.groupoid {X : Type u} {G : Type u_2} [group G] [mul_action G X] :
category_theory.groupoid (category_theory.action_category G X)
Equations
source
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.

Equations
source
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) :
↑(g⁻¹ • t) ⟶ ↑t

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

Equations
source
@[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) :
(category_theory.action_category.hom_of_pair t g).val = g
source
@[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
source
@[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) :
(⇑(category_theory.action_category.curry F) g).left b = F.map (category_theory.action_category.hom_of_pair b g)
source
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
source
@[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
source
@[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) :
(category_theory.action_category.uncurry F sane).map f = (⇑F f.val).left b.back
source
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) :
category_theory.action_category G X ⥤ category_theory.single_obj H

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
source
@[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 = unit.star()