Functoriality of action categories and subgroup restrictions

A map f : X → Y that is equivariant along a monoid homomorphism φ : M →* N, that is f (m • x) = φ m • f x, induces a functor ActionCategory.map φ f from the action category M ⋉ X to N ⋉ Y: it sends the point x to f x and the arrow labelled m to the arrow labelled φ m. It is faithful when φ is injective, and it is full exactly when every arrow between two image points lifts: whenever n • f x = f x', some m with φ m = n carries x to x' (CategoryTheory.ActionCategory.full_map_iff).

The main instance is the restriction of an action groupoid to a subset. Let H be a subgroup of a group G acting on X, and let S be a subset of X preserved by H, as a SubMulAction H X. The functor CategoryTheory.ActionCategory.inclusion S : H ⋉ S ⥤ G ⋉ X keeps each label of H as an element of G, so it is faithful and injective on objects, and its objects are exactly the points of S. It is full exactly when S is a slice for H: every element of G carrying a point of S into S lies in H (CategoryTheory.ActionCategory.full_inclusion_iff). In that case the inclusion identifies H ⋉ S with the full subgroupoid of G ⋉ X on the points of S. For a proper action of a discrete group, a slice at x for the stabilizer of x is the local isotropy model of the quotient [X/G] near the orbit of x. Labels acting trivially are kept, so the identification retains ineffective isotropy.

For a monoid M and an M-invariant subset U, CategoryTheory.ActionCategory.restrict U is the inclusion M ⋉ U ⥤ M ⋉ X keeping every label; it is fully faithful, so M ⋉ U is the full subcategory of M ⋉ X on the points of U. When U is open, this is the restriction of a topological action groupoid to a saturated open set of objects.

Main declarations

• CategoryTheory.ActionCategory.map: the functor induced by an equivariant map.
• CategoryTheory.ActionCategory.map_id, CategoryTheory.ActionCategory.map_comp: it preserves identities and composites.
• CategoryTheory.ActionCategory.faithful_map: it is faithful along an injective homomorphism.
• CategoryTheory.ActionCategory.full_map_iff: it is full exactly when arrows between image points lift.
• CategoryTheory.ActionCategory.restrict: the full inclusion of the action category on an invariant subset.
• CategoryTheory.ActionCategory.restrictLift: a functor whose objects lie in the invariant subset factors through that inclusion.
• CategoryTheory.ActionCategory.exists_functor_of_sections: a functor out of the action category on a subset of the objects of a category, given by sections of arrows labelled by the monoid.
• CategoryTheory.ActionCategory.singleObjFunctor: the functor SingleObj K ⥤ M ⋉ X at a point fixed by the image of a monoid homomorphism K →* M.
• CategoryTheory.ActionCategory.inclusion: the inclusion of the action category of a subgroup on an invariant subset.
• CategoryTheory.ActionCategory.full_inclusion_iff: the inclusion is full exactly for a slice.
• CategoryTheory.ActionCategory.range_inclusion_obj: its objects are the points of the subset.
• CategoryTheory.ActionCategory.range_inclusion_total: for a slice, its arrows are the arrows with source and target in the subset.

References

• I. Moerdijk and J. Mrčun, Introduction to foliations and Lie groupoids, Section 5.1.
• I. Moerdijk, Orbifolds as groupoids: an introduction, Section 2.

def CategoryTheory.ActionCategory.map {M : Type u_1} {N : Type u_2} [Monoid M] [Monoid N] {X : Type u_3} {Y : Type u_4} [MulAction M X] [MulAction N Y] (φ : M →* N) (f : X →ₑ[⇑φ] Y) : Functor (ActionCategory M X) (ActionCategory N Y)

The functor M ⋉ X ⥤ N ⋉ Y induced by a map f : X → Y that is equivariant along a monoid homomorphism φ : M →* N. It sends the point x to f x and the arrow labelled m to the arrow labelled φ m.

@[simp]

theorem CategoryTheory.ActionCategory.map_obj {M : Type u_1} {N : Type u_2} [Monoid M] [Monoid N] {X : Type u_3} {Y : Type u_4} [MulAction M X] [MulAction N Y] (φ : M →* N) (f : X →ₑ[⇑φ] Y) (x : X) : (map φ f).obj ((objEquiv M X) x) = (objEquiv N Y) (f x)

The functor induced by an equivariant map sends the point x to f x.

@[simp]

theorem CategoryTheory.ActionCategory.back_map_obj {M : Type u_1} {N : Type u_2} [Monoid M] [Monoid N] {X : Type u_3} {Y : Type u_4} [MulAction M X] [MulAction N Y] (φ : M →* N) (f : X →ₑ[⇑φ] Y) (a : ActionCategory M X) : ((map φ f).obj a).back = f a.back

The point underlying the image of an object is the image of its point.

@[simp]

theorem CategoryTheory.ActionCategory.map_map_hom {M : Type u_1} {N : Type u_2} [Monoid M] [Monoid N] {X : Type u_3} {Y : Type u_4} [MulAction M X] [MulAction N Y] (φ : M →* N) (f : X →ₑ[⇑φ] Y) {a b : ActionCategory M X} (g : a ⟶ b) : ((map φ f).map g).hom = φ g.hom

The functor induced by an equivariant map relabels arrows by the homomorphism.

@[simp]

theorem CategoryTheory.ActionCategory.mapTotal_totalEquiv_symm {M : Type u_1} {N : Type u_2} [Monoid M] [Monoid N] {X : Type u_3} {Y : Type u_4} [MulAction M X] [MulAction N Y] (φ : M →* N) (f : X →ₑ[⇑φ] Y) (m : M) (x : X) : (map φ f).toPrefunctor.mapTotal ((totalEquiv M X).symm (m, x)) = (totalEquiv N Y).symm (φ m, f x)

In label-source coordinates, the functor induced by an equivariant map applies the homomorphism to the label and the equivariant map to the source.

theorem CategoryTheory.ActionCategory.map_id (M : Type u_1) [Monoid M] (X : Type u_3) [MulAction M X] : map (MonoidHom.id M) (MulActionHom.id M) = Functor.id (ActionCategory M X)

The identity map induces the identity functor.

theorem CategoryTheory.ActionCategory.map_comp {M : Type u_1} {N : Type u_2} [Monoid M] [Monoid N] {X : Type u_3} {Y : Type u_4} [MulAction M X] [MulAction N Y] (φ : M →* N) (f : X →ₑ[⇑φ] Y) {P : Type u_5} {Z : Type u_6} [Monoid P] [MulAction P Z] {ψ : N →* P} (g : Y →ₑ[⇑ψ] Z) {χ : M →* P} [φ.CompTriple ψ χ] : (map φ f).comp (map ψ g) = map χ (g.comp f)

The functor induced by a composite of equivariant maps is the composite of the induced functors.

theorem CategoryTheory.ActionCategory.faithful_map {M : Type u_1} {N : Type u_2} [Monoid M] [Monoid N] {X : Type u_3} {Y : Type u_4} [MulAction M X] [MulAction N Y] (φ : M →* N) (f : X →ₑ[⇑φ] Y) (hφ : Function.Injective ⇑φ) : (map φ f).Faithful

The functor induced by an equivariant map along an injective homomorphism is faithful.

theorem CategoryTheory.ActionCategory.full_map_iff {M : Type u_1} {N : Type u_2} [Monoid M] [Monoid N] {X : Type u_3} {Y : Type u_4} [MulAction M X] [MulAction N Y] (φ : M →* N) (f : X →ₑ[⇑φ] Y) : (map φ f).Full ↔ ∀ (x x' : X) (n : N), n • f x = f x' → ∃ (m : M), φ m = n ∧ m • x = x'

The functor induced by an equivariant map is full exactly when every arrow between two image points lifts: if n • f x = f x', then some m with φ m = n carries x to x'.

theorem CategoryTheory.ActionCategory.full_map_of_injective {M : Type u_1} [Monoid M] {X : Type u_3} {Y : Type u_4} [MulAction M X] [MulAction M Y] (f : X →ₑ[id] Y) (hf : Function.Injective ⇑f) : (map (MonoidHom.id M) f).Full

An injective equivariant map for the same monoid induces a full functor, keeping every arrow label.

def CategoryTheory.ActionCategory.singleObjFunctor {M : Type u_1} [Monoid M] {X : Type u_3} [MulAction M X] {K : Type u_5} [Monoid K] (φ : K →* M) (x : X) (hx : ∀ (k : K), φ k • x = x) : Functor (SingleObj K) (ActionCategory M X)

The functor SingleObj K ⥤ M ⋉ X at a point x fixed by the image of φ : K →* M. It sends the unique object to x and k to the arrow x ⟶ x labelled φ k: this is Mathlib's SingleObj.functor for φ, corestricted to the stabilizer of x and composed with ActionCategory.stabilizerIsoEnd. Restricting a family of categories over M ⋉ X along it gives a categorical action of K on the category over x.

@[simp]

theorem CategoryTheory.ActionCategory.singleObjFunctor_obj {M : Type u_1} [Monoid M] {X : Type u_3} [MulAction M X] {K : Type u_5} [Monoid K] (φ : K →* M) (x : X) (hx : ∀ (k : K), φ k • x = x) (a : SingleObj K) : (singleObjFunctor φ x hx).obj a = (objEquiv M X) x

The functor at a fixed point sends the unique object to that point.

@[simp]

theorem CategoryTheory.ActionCategory.singleObjFunctor_map_hom {M : Type u_1} [Monoid M] {X : Type u_3} [MulAction M X] {K : Type u_5} [Monoid K] (φ : K →* M) (x : X) (hx : ∀ (k : K), φ k • x = x) {a b : SingleObj K} (k : a ⟶ b) : ((singleObjFunctor φ x hx).map k).hom = φ k

The functor at a fixed point labels the arrow of k by φ k.

def CategoryTheory.ActionCategory.restrict {M : Type u_1} [Monoid M] {X : Type u_2} [MulAction M X] (U : SubMulAction M X) : Functor (ActionCategory M ↥U) (ActionCategory M X)

The inclusion M ⋉ U ⥤ M ⋉ X of the action category on an invariant subset U. It sends a point of U to itself and keeps each label, so it identifies M ⋉ U with the full subcategory of M ⋉ X on the points of U.

theorem CategoryTheory.ActionCategory.restrict_eq_map {M : Type u_1} [Monoid M] {X : Type u_2} [MulAction M X] (U : SubMulAction M X) : restrict U = map (MonoidHom.id M) { toFun := Subtype.val, map_smul' := ⋯ }

The restriction inclusion is the functor induced by the inclusion of U, keeping labels.

@[simp]

theorem CategoryTheory.ActionCategory.back_restrict_obj {M : Type u_1} [Monoid M] {X : Type u_2} [MulAction M X] (U : SubMulAction M X) (a : ActionCategory M ↥U) : ((restrict U).obj a).back = ↑a.back

The point underlying the image of an object under the restriction inclusion is its point.

@[simp]

theorem CategoryTheory.ActionCategory.restrict_map_hom {M : Type u_1} [Monoid M] {X : Type u_2} [MulAction M X] (U : SubMulAction M X) {a b : ActionCategory M ↥U} (g : a ⟶ b) : ((restrict U).map g).hom = g.hom

The restriction inclusion keeps the label of each arrow.

instance CategoryTheory.ActionCategory.faithful_restrict {M : Type u_1} [Monoid M] {X : Type u_2} [MulAction M X] (U : SubMulAction M X) : (restrict U).Faithful

The restriction inclusion is faithful.

instance CategoryTheory.ActionCategory.full_restrict {M : Type u_1} [Monoid M] {X : Type u_2} [MulAction M X] (U : SubMulAction M X) : (restrict U).Full

The restriction inclusion is full: every arrow between points of U lies in M ⋉ U.

def CategoryTheory.ActionCategory.restrictLift {M : Type u_1} [Monoid M] {X : Type u_2} [MulAction M X] (U : SubMulAction M X) {J : Type u_3} [Category.{u_4, u_3} J] (F : Functor J (ActionCategory M X)) (hF : ∀ (j : J), (F.obj j).back ∈ U) : Functor J (ActionCategory M ↥U)

A functor into M ⋉ X all of whose objects lie in the invariant subset U factors through M ⋉ U: this lifts it along the restriction inclusion.

@[simp]

theorem CategoryTheory.ActionCategory.back_restrictLift_obj {M : Type u_1} [Monoid M] {X : Type u_2} [MulAction M X] (U : SubMulAction M X) {J : Type u_3} [Category.{u_4, u_3} J] (F : Functor J (ActionCategory M X)) (hF : ∀ (j : J), (F.obj j).back ∈ U) (j : J) : ((restrictLift U F hF).obj j).back = ⟨(F.obj j).back, ⋯⟩

The lift of a functor along the restriction inclusion sends an object to the point of U underlying its image.

@[simp]

theorem CategoryTheory.ActionCategory.restrictLift_map_hom {M : Type u_1} [Monoid M] {X : Type u_2} [MulAction M X] (U : SubMulAction M X) {J : Type u_3} [Category.{u_4, u_3} J] (F : Functor J (ActionCategory M X)) (hF : ∀ (j : J), (F.obj j).back ∈ U) {j j' : J} (g : j ⟶ j') : ((restrictLift U F hF).map g).hom = (F.map g).hom

The lift of a functor along the restriction inclusion keeps the label of each arrow.

@[simp]

theorem CategoryTheory.ActionCategory.restrictLift_comp_restrict {M : Type u_1} [Monoid M] {X : Type u_2} [MulAction M X] (U : SubMulAction M X) {J : Type u_3} [Category.{u_4, u_3} J] (F : Functor J (ActionCategory M X)) (hF : ∀ (j : J), (F.obj j).back ∈ U) : (restrictLift U F hF).comp (restrict U) = F

The lift of a functor along the restriction inclusion recovers the functor.

def CategoryTheory.ActionCategory.inclusion {G : Type u_1} [Group G] {X : Type u_2} [MulAction G X] {H : Subgroup G} (S : SubMulAction (↥H) X) : Functor (ActionCategory ↥H ↥S) (ActionCategory G X)

The inclusion H ⋉ S ⥤ G ⋉ X of the action category of a subgroup H on an H-invariant subset S. It sends a point of S to itself and keeps each label of H as an element of G.

theorem CategoryTheory.ActionCategory.inclusion_eq_map {G : Type u_1} [Group G] {X : Type u_2} [MulAction G X] {H : Subgroup G} (S : SubMulAction (↥H) X) : inclusion S = map H.subtype { toFun := Subtype.val, map_smul' := ⋯ }

The inclusion is the functor induced by the inclusion of S along the inclusion of H.

@[simp]

theorem CategoryTheory.ActionCategory.inclusion_obj {G : Type u_1} [Group G] {X : Type u_2} [MulAction G X] {H : Subgroup G} (S : SubMulAction (↥H) X) (y : ↥S) : (inclusion S).obj ((objEquiv ↥H ↥S) y) = (objEquiv G X) ↑y

The inclusion sends a point of the invariant subset to itself.

@[simp]

theorem CategoryTheory.ActionCategory.back_inclusion_obj {G : Type u_1} [Group G] {X : Type u_2} [MulAction G X] {H : Subgroup G} (S : SubMulAction (↥H) X) (a : ActionCategory ↥H ↥S) : ((inclusion S).obj a).back = ↑a.back

The point underlying the image of an object under the inclusion is its point.

@[simp]

theorem CategoryTheory.ActionCategory.inclusion_map_hom {G : Type u_1} [Group G] {X : Type u_2} [MulAction G X] {H : Subgroup G} (S : SubMulAction (↥H) X) {a b : ActionCategory ↥H ↥S} (g : a ⟶ b) : ((inclusion S).map g).hom = H.subtype g.hom

The inclusion keeps the label of each arrow.

instance CategoryTheory.ActionCategory.faithful_inclusion {G : Type u_1} [Group G] {X : Type u_2} [MulAction G X] {H : Subgroup G} (S : SubMulAction (↥H) X) : (inclusion S).Faithful

The inclusion of the action category of a subgroup is faithful.

theorem CategoryTheory.ActionCategory.inclusion_obj_injective {G : Type u_1} [Group G] {X : Type u_2} [MulAction G X] {H : Subgroup G} (S : SubMulAction (↥H) X) : Function.Injective (inclusion S).obj

The inclusion is injective on objects.

theorem CategoryTheory.ActionCategory.range_inclusion_obj {G : Type u_1} [Group G] {X : Type u_2} [MulAction G X] {H : Subgroup G} (S : SubMulAction (↥H) X) : Set.range (inclusion S).obj = {a : ActionCategory G X | a.back ∈ S}

The objects in the image of the inclusion are exactly the points of the invariant subset.

theorem CategoryTheory.ActionCategory.full_inclusion_iff {G : Type u_1} [Group G] {X : Type u_2} [MulAction G X] {H : Subgroup G} (S : SubMulAction (↥H) X) : (inclusion S).Full ↔ ∀ (g : G), ∀ y ∈ S, g • y ∈ S → g ∈ H

The inclusion of the action category of a subgroup H on an invariant subset S is full exactly when S is a slice for H: every element of G carrying a point of S into S lies in H.

theorem CategoryTheory.ActionCategory.range_inclusion_total {G : Type u_1} [Group G] {X : Type u_2} [MulAction G X] {H : Subgroup G} (S : SubMulAction (↥H) X) (hS : ∀ (g : G), ∀ y ∈ S, g • y ∈ S → g ∈ H) : Set.range (inclusion S).toPrefunctor.mapTotal = {f : Quiver.Total (ActionCategory G X) | f.left.back ∈ S ∧ f.right.back ∈ S}

For a slice S for H, the arrows of H ⋉ S are, through the inclusion, exactly the arrows of G ⋉ X with source and target in S.

theorem CategoryTheory.ActionCategory.exists_functor_of_sections {M : Type u_1} [Monoid M] {C : Type u_2} [Category.{u_3, u_2} C] {U : Set C} [MulAction M ↑U] {σ : M → C → Quiver.Total C} (hsmul : ∀ (g : M) (y : ↑U), ↑(g • y) = (σ g ↑y).right) (hσl : ∀ (g : M), ∀ y ∈ U, (σ g y).left = y) (hUσ : ∀ y ∈ U, ∀ (h : M), (σ h y).right ∈ U) (hone : ∀ y ∈ U, σ 1 y = { left := y, right := y, hom := CategoryStruct.id y }) (hmul : ∀ (y : C) (hy : y ∈ U) (g h : M), σ (g * h) y = (σ h y).comp (σ g (σ h y).right) ⋯) : ∃ (F : Functor (ActionCategory M ↑U) C), (∀ (a : ActionCategory M ↑U), F.obj a = ↑a.back) ∧ ∀ {a b : ActionCategory M ↑U} (f : a ⟶ b), { left := F.obj a, right := F.obj b, hom := F.map f } = σ f.hom ↑a.back

A functor out of the action category of a monoid acting on a subset U of the objects of C, given by a section σ g y of arrows with source y for each label g and point y: it is the identity on objects and sends the arrow labelled g at a to the arrow σ g a. The sections must have the unit and composition behaviour of the action: σ 1 y is the identity at y, and σ (g * h) y is σ h y followed by σ g at the target of σ h y.