Isotropy, arrows and orbits of an action groupoid

For a group G acting on a type X, Mathlib's CategoryTheory.ActionCategory G X is the action groupoid G ⋉ X: its objects correspond to points of X through ActionCategory.objEquiv, and an arrow x ⟶ y is a group element g with g • x = y, its label. This file records the dictionary between the groupoid and the action that the orbifold point of view uses, where G ⋉ X is the presentation of the quotient [X/G].

Arrows remember their labels. The total set of arrows is G × X, by label and source (ActionCategory.totalEquiv); in these coordinates the source of (g, x) is x, its target is g • x, the identity at x is (1, x), inversion is labelled by g⁻¹ and composition by the product, (f ≫ f').hom = f'.hom * f.hom (Mathlib's ActionCategory.comp_hom).

The isotropy group of the object x is the stabilizer of x, with every element kept: an element acting trivially on all of X still gives its own automorphism. This is what separates an ineffective quotient from its effective reduction; for instance the point quotient [*/G] has isotropy G and, for nontrivial G, is not equivalent to the point with trivial isotropy. Two group laws on the isotropy group are in use, and both are compared with the stabilizer: Aut and End multiply in the order of function composition, g * h = h ≫ g, matching the stabilizer, while Mathlib's vertex group CategoryTheory.Groupoid.vertexGroup multiplies in diagrammatic order, so the stabilizer is its opposite. Transporting isotropy along an arrow is conjugation by its label.

Finally, the isomorphism classes of objects, the underlying set of the coarse space, are the orbits of the action.

Main declarations

• CategoryTheory.ActionCategory.totalEquiv: the arrows of G ⋉ X are G × X; this holds for any monoid action.
• CategoryTheory.ActionCategory.stabilizerMulEquivAut: the stabilizer of x is the automorphism group of x, compatibly with Mathlib's ActionCategory.stabilizerIsoEnd (CategoryTheory.ActionCategory.toEnd_stabilizerMulEquivAut) and with transport along arrows (CategoryTheory.ActionCategory.autMulEquivOfIso_stabilizerMulEquivAut).
• CategoryTheory.ActionCategory.stabilizerMulEquivVertexGroupMulOpposite: the stabilizer is the opposite of the vertex group.
• CategoryTheory.ActionCategory.stabilizer_eq_bot_of_faithful: if G ⋉ X has a faithful functor to a thin category, all stabilizers are trivial; in particular CategoryTheory.ActionCategory.isEmpty_equivalence_punit.
• CategoryTheory.ActionCategory.autMulEquivOfMemFixedPoints: the isotropy at a fixed point is all of G.
• CategoryTheory.ActionCategory.orbitQuotientEquivIsomorphismClasses: orbits are isomorphism classes.
• CategoryTheory.ActionCategory.commSq_inl_inr: for a semidirect product N ⋊[φ] K, arrows labelled n then k compose to the same arrow as arrows labelled k then φ k n.

References

• I. Moerdijk and J. Mrčun, Introduction to foliations and Lie groupoids, Section 5.1.
• A. Adem, J. Leida and Y. Ruan, Orbifolds and stringy topology, Chapter 1.

theorem CategoryTheory.ActionCategory.back_injective {M : Type u_1} [Monoid M] {X : Type u_2} [MulAction M X] : Function.Injective ActionCategory.back

Objects of the action category are determined by their underlying points.

theorem CategoryTheory.ActionCategory.hom_smul {M : Type u_1} [Monoid M] {X : Type u_2} [MulAction M X] {x y : X} (f : (objEquiv M X) x ⟶ (objEquiv M X) y) : f.hom • x = y

An arrow of the action category goes from a point to its translate by the arrow's label.

def CategoryTheory.ActionCategory.totalEquiv (M : Type u_1) [Monoid M] (X : Type u_2) [MulAction M X] : Quiver.Total (ActionCategory M X) ≃ M × X

The total set of arrows of the action category, identified with M × X by recording the label and the source of each arrow. The target of the arrow labelled (m, x) is m • x.

@[simp]

theorem CategoryTheory.ActionCategory.totalEquiv_apply {M : Type u_1} [Monoid M] {X : Type u_2} [MulAction M X] (f : Quiver.Total (ActionCategory M X)) : (totalEquiv M X) f = (f.hom.hom, f.left.back)

@[simp]

theorem CategoryTheory.ActionCategory.totalEquiv_symm_apply_left {M : Type u_1} [Monoid M] {X : Type u_2} [MulAction M X] (p : M × X) : ((totalEquiv M X).symm p).left = (objEquiv M X) p.2

@[simp]

theorem CategoryTheory.ActionCategory.totalEquiv_symm_apply_right {M : Type u_1} [Monoid M] {X : Type u_2} [MulAction M X] (p : M × X) : ((totalEquiv M X).symm p).right = (objEquiv M X) (p.1 • p.2)

@[simp]

theorem CategoryTheory.ActionCategory.totalEquiv_symm_apply_hom_hom {M : Type u_1} [Monoid M] {X : Type u_2} [MulAction M X] (p : M × X) : ((totalEquiv M X).symm p).hom.hom = p.1

@[simp]

theorem CategoryTheory.ActionCategory.eqToHom_hom {M : Type u_1} [Monoid M] {X : Type u_2} [MulAction M X] {a b : ActionCategory M X} (h : a = b) : (eqToHom h).hom = 1

An identity arrow written as eqToHom is labelled by 1.

@[simp]

theorem CategoryTheory.ActionCategory.inv_hom {G : Type u_1} [Group G] {X : Type u_2} [MulAction G X] {a b : ActionCategory G X} (f : a ⟶ b) : (inv f).hom = f.hom⁻¹

The inverse of an arrow of the action groupoid is labelled by the inverse group element.

def CategoryTheory.ActionCategory.stabilizerMulEquivAut (G : Type u_1) [Group G] {X : Type u_2} [MulAction G X] (x : X) : ↥(MulAction.stabilizer G x) ≃* Aut ((objEquiv G X) x)

The stabilizer of x is the automorphism group of the corresponding object of the action groupoid. Every element of the stabilizer, including one acting trivially on all of X, is kept as its own automorphism, and the multiplication matches g * h = h ≫ g.

@[simp]

theorem CategoryTheory.ActionCategory.stabilizerMulEquivAut_apply_hom_hom {G : Type u_1} [Group G] {X : Type u_2} [MulAction G X] (x : X) (g : ↥(MulAction.stabilizer G x)) : ((stabilizerMulEquivAut G x) g).asIso.hom.hom = ↑g

@[simp]

theorem CategoryTheory.ActionCategory.stabilizerMulEquivAut_apply_inv_hom {G : Type u_1} [Group G] {X : Type u_2} [MulAction G X] (x : X) (g : ↥(MulAction.stabilizer G x)) : ((stabilizerMulEquivAut G x) g).asIso.inv.hom = (↑g)⁻¹

@[simp]

theorem CategoryTheory.ActionCategory.coe_stabilizerMulEquivAut_symm_apply {G : Type u_1} [Group G] {X : Type u_2} [MulAction G X] (x : X) (e : Aut ((objEquiv G X) x)) : ↑((stabilizerMulEquivAut G x).symm e) = e.asIso.hom.hom

theorem CategoryTheory.ActionCategory.toEnd_stabilizerMulEquivAut {G : Type u_1} [Group G] {X : Type u_2} [MulAction G X] (x : X) (g : ↥(MulAction.stabilizer G x)) : Aut.toEnd ((stabilizerMulEquivAut G x) g) = (stabilizerIsoEnd G x) ⟨↑g, ⋯⟩

Under the inclusion of automorphisms into endomorphisms, stabilizerMulEquivAut restricts to Mathlib's ActionCategory.stabilizerIsoEnd on the stabilizer submonoid.

theorem CategoryTheory.ActionCategory.autMulEquivOfIso_stabilizerMulEquivAut {G : Type u_1} [Group G] {X : Type u_2} [MulAction G X] {x y : X} (f : (objEquiv G X) x ⟶ (objEquiv G X) y) (g : ↥(MulAction.stabilizer G x)) : (Aut.autMulEquivOfIso ((Groupoid.isoEquivHom ((objEquiv G X) x) ((objEquiv G X) y)).symm f)) ((stabilizerMulEquivAut G x) g) = (stabilizerMulEquivAut G y) ((MulAction.stabilizerEquivStabilizer ⋯) g)

Transport of automorphisms along an arrow f of the action groupoid corresponds to conjugation of stabilizers by the label of f.

def CategoryTheory.ActionCategory.stabilizerMulEquivVertexGroupMulOpposite (G : Type u_1) [Group G] {X : Type u_2} [MulAction G X] (x : X) : ↥(MulAction.stabilizer G x) ≃* ((objEquiv G X) x ⟶ (objEquiv G X) x)ᵐᵒᵖ

The stabilizer of x is the opposite of Mathlib's vertex group at the corresponding object. The vertex group multiplies in diagrammatic order, f * g = f ≫ g, while stabilizer labels compose as g * h = h ≫ g.

@[simp]

theorem CategoryTheory.ActionCategory.stabilizerMulEquivVertexGroupMulOpposite_apply_unop_hom {G : Type u_1} [Group G] {X : Type u_2} [MulAction G X] (x : X) (g : ↥(MulAction.stabilizer G x)) : (MulOpposite.unop ((stabilizerMulEquivVertexGroupMulOpposite G x) g)).hom = ↑g

@[simp]

theorem CategoryTheory.ActionCategory.coe_stabilizerMulEquivVertexGroupMulOpposite_symm_apply {G : Type u_1} [Group G] {X : Type u_2} [MulAction G X] (x : X) (f : ((objEquiv G X) x ⟶ (objEquiv G X) x)ᵐᵒᵖ) : ↑((stabilizerMulEquivVertexGroupMulOpposite G x).symm f) = (MulOpposite.unop f).hom

theorem CategoryTheory.ActionCategory.stabilizer_eq_bot_of_faithful {G : Type u_1} [Group G] {X : Type u_2} [MulAction G X] {D : Type u_3} [Category.{u_4, u_3} D] [Quiver.IsThin D] (F : Functor (ActionCategory G X) D) [F.Faithful] (x : X) : MulAction.stabilizer G x = ⊥

If the action groupoid admits a faithful functor to a thin category, for instance an equivalence with a discrete category, then every stabilizer is trivial.

def CategoryTheory.ActionCategory.autMulEquivOfMemFixedPoints (G : Type u_1) [Group G] {X : Type u_2} [MulAction G X] {x : X} (hx : x ∈ MulAction.fixedPoints G X) : Aut ((objEquiv G X) x) ≃* G

At a fixed point of the action, the isotropy group is all of G, including every element acting trivially on X.

@[simp]

theorem CategoryTheory.ActionCategory.autMulEquivOfMemFixedPoints_apply {G : Type u_1} [Group G] {X : Type u_2} [MulAction G X] {x : X} (hx : x ∈ MulAction.fixedPoints G X) (e : Aut ((objEquiv G X) x)) : (autMulEquivOfMemFixedPoints G hx) e = e.asIso.hom.hom

@[simp]

theorem CategoryTheory.ActionCategory.autMulEquivOfMemFixedPoints_symm_apply_hom_hom {G : Type u_1} [Group G] {X : Type u_2} [MulAction G X] {x : X} (hx : x ∈ MulAction.fixedPoints G X) (g : G) : ((autMulEquivOfMemFixedPoints G hx).symm g).asIso.hom.hom = g

theorem CategoryTheory.ActionCategory.isEmpty_equivalence_punit {G : Type u_1} [Group G] [Nontrivial G] {D : Type u_3} [Category.{u_4, u_3} D] [Quiver.IsThin D] : IsEmpty (ActionCategory G PUnit.{u_5 + 1} ≌ D)

If the group is nontrivial, the point quotient [*/G] is not equivalent to a thin category; in particular it is not equivalent to the point with trivial isotropy.

theorem CategoryTheory.ActionCategory.nonempty_hom_iff {X : Type u_2} {M : Type u_3} [Monoid M] [MulAction M X] {x y : X} : Nonempty ((objEquiv M X) x ⟶ (objEquiv M X) y) ↔ ∃ (m : M), m • x = y

There is an arrow from x to y in the action category exactly when y is a translate m • x of x, i.e. lies in the orbit of x.

theorem CategoryTheory.ActionCategory.isIsomorphic_iff_orbitRel {G : Type u_1} [Group G] {X : Type u_2} [MulAction G X] {x y : X} : IsIsomorphic ((objEquiv G X) x) ((objEquiv G X) y) ↔ (MulAction.orbitRel G X) x y

Two objects of the action groupoid are isomorphic exactly when the corresponding points lie in the same orbit.

theorem CategoryTheory.ActionCategory.orbitRel_iff_isIsomorphic_obj_of_full {G : Type u_1} [Group G] {X : Type u_2} [MulAction G X] {C : Type u_3} [Category.{u_4, u_3} C] (F : Functor (ActionCategory G X) C) [F.Full] {x y : X} : (MulAction.orbitRel G X) x y ↔ IsIsomorphic (F.obj ((objEquiv G X) x)) (F.obj ((objEquiv G X) y))

If a functor out of the action groupoid is full, two points lie in the same orbit exactly when the images of the corresponding objects are isomorphic.

def CategoryTheory.ActionCategory.orbitQuotientEquivIsomorphismClasses (G : Type u_1) [Group G] (X : Type u_2) [MulAction G X] : MulAction.orbitRel.Quotient G X ≃ _root_.Quotient (isIsomorphicSetoid (ActionCategory G X))

The orbit space of the action is the set of isomorphism classes of its action groupoid.

@[simp]

theorem CategoryTheory.ActionCategory.orbitQuotientEquivIsomorphismClasses_mk {G : Type u_1} [Group G] {X : Type u_2} [MulAction G X] (x : X) : (orbitQuotientEquivIsomorphismClasses G X) ⟦x⟧ = ⟦(objEquiv G X) x⟧

theorem CategoryTheory.ActionCategory.commSq_inl_inr {N : Type u_3} {K : Type u_4} [Group N] [Group K] {φ : K →* MulAut N} {X : Type u_5} [MulAction (N ⋊[φ] K) X] {x y y' z : ActionCategory (N ⋊[φ] K) X} {t : x ⟶ y} {r : y ⟶ z} {l : x ⟶ y'} {b : y' ⟶ z} {n : N} {k : K} (ht : t.hom = SemidirectProduct.inl n) (hr : r.hom = SemidirectProduct.inr k) (hl : l.hom = SemidirectProduct.inr k) (hb : b.hom = SemidirectProduct.inl ((φ k) n)) : CommSq t l r b

In the action category of a semidirect product N ⋊[φ] K, an arrow labelled n followed by an arrow labelled k is the arrow labelled k followed by an arrow labelled φ k n, because inr k * inl n = inl (φ k n) * inr k. This is the covariance of the two kinds of arrows.