The topology of an action groupoid

For a continuous action of a topological group G on X, equip the objects and total arrows of Mathlib's native CategoryTheory.ActionCategory G X with the topologies transported from X and G × X. The arrow coordinates record the label and source, including labels acting trivially. Source, target, unit, inversion and composition are continuous with these topologies, and both spaces are Hausdorff and second countable when the labels and points are.

The source-target map is proper precisely when the action is proper. For a discrete group, each fixed-label slice is an open bisection: source and target are local homeomorphisms. Thus these topologies give the topological action presentations used for finite quotient charts, without imposing faithfulness or discarding ineffective isotropy. The basic topology, units, composition and source charts are also available for monoid actions. The functor CategoryTheory.ActionCategory.map φ f induced by a continuous map f equivariant along a continuous monoid homomorphism φ is continuous on total arrows, and jointly continuous in a parameter when f varies continuously (TauCeti.ActionGroupoid.continuous_mapTotal_map, TauCeti.ActionGroupoid.continuous_uncurry_mapTotal_map).

In these coordinates, the functor CategoryTheory.ActionCategory.map φ f induced by a map f equivariant along a homomorphism φ acts on total arrows as Prod.map φ f (TauCeti.ActionGroupoid.mapTotal_map_eq), so it is an embedding or an open embedding on total arrows when φ and f both are. In particular, the inclusion CategoryTheory.ActionCategory.restrict U of the action groupoid on an invariant subset is an embedding on total arrows (TauCeti.ActionGroupoid.isEmbedding_mapTotal_restrict).

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.

The algebraic identifications are CategoryTheory.ActionCategory.objEquiv and CategoryTheory.ActionCategory.totalEquiv; properness uses Mathlib's ProperSMul.

@[instance_reducible]

instance TauCeti.ActionGroupoid.instTopologicalSpaceObjects (G : Type u_1) (X : Type u_2) [Monoid G] [MulAction G X] [TopologicalSpace X] : TopologicalSpace (CategoryTheory.ActionCategory G X)

The object topology of the native action category, transported from X.

def TauCeti.ActionGroupoid.objectHomeomorph (G : Type u_1) (X : Type u_2) [Monoid G] [MulAction G X] [TopologicalSpace X] : CategoryTheory.ActionCategory G X ≃ₜ X

Objects of the native action category are homeomorphic to the acted-on space.

@[simp]

theorem TauCeti.ActionGroupoid.objectHomeomorph_apply (G : Type u_1) (X : Type u_2) [Monoid G] [MulAction G X] [TopologicalSpace X] (x : CategoryTheory.ActionCategory G X) : (objectHomeomorph G X) x = x.back

The object homeomorphism reads the point underlying a native action-category object.

@[simp]

theorem TauCeti.ActionGroupoid.objectHomeomorph_symm_apply (G : Type u_1) (X : Type u_2) [Monoid G] [MulAction G X] [TopologicalSpace X] (x : X) : (objectHomeomorph G X).symm x = (CategoryTheory.ActionCategory.objEquiv G X) x

The inverse object homeomorphism is the native object equivalence.

instance TauCeti.ActionGroupoid.instT2SpaceObjects (G : Type u_1) (X : Type u_2) [Monoid G] [MulAction G X] [TopologicalSpace X] [T2Space X] : T2Space (CategoryTheory.ActionCategory G X)

The objects of the action category of a Hausdorff space are Hausdorff.

instance TauCeti.ActionGroupoid.instSecondCountableTopologyObjects (G : Type u_1) (X : Type u_2) [Monoid G] [MulAction G X] [TopologicalSpace X] [SecondCountableTopology X] : SecondCountableTopology (CategoryTheory.ActionCategory G X)

The objects of the action category of a second-countable space are second countable.

@[instance_reducible]

instance TauCeti.ActionGroupoid.instTopologicalSpaceArrows (G : Type u_1) (X : Type u_2) [Monoid G] [MulAction G X] [TopologicalSpace X] [TopologicalSpace G] : TopologicalSpace (Quiver.Total (CategoryTheory.ActionCategory G X))

The total-arrow topology of the native action category, transported from label-source pairs.

def TauCeti.ActionGroupoid.arrowHomeomorph (G : Type u_1) (X : Type u_2) [Monoid G] [MulAction G X] [TopologicalSpace X] [TopologicalSpace G] : Quiver.Total (CategoryTheory.ActionCategory G X) ≃ₜ G × X

Total arrows of the native action category are homeomorphic to label-source pairs.

@[simp]

theorem TauCeti.ActionGroupoid.arrowHomeomorph_apply (G : Type u_1) (X : Type u_2) [Monoid G] [MulAction G X] [TopologicalSpace X] [TopologicalSpace G] (f : Quiver.Total (CategoryTheory.ActionCategory G X)) : (arrowHomeomorph G X) f = (f.hom.hom, f.left.back)

The arrow homeomorphism records the label and the point underlying the source.

@[simp]

theorem TauCeti.ActionGroupoid.arrowHomeomorph_symm_apply (G : Type u_1) (X : Type u_2) [Monoid G] [MulAction G X] [TopologicalSpace X] [TopologicalSpace G] (p : G × X) : (arrowHomeomorph G X).symm p = (CategoryTheory.ActionCategory.totalEquiv G X).symm p

The inverse arrow homeomorphism uses the native algebraic total-arrow equivalence.

instance TauCeti.ActionGroupoid.instT2SpaceArrows (G : Type u_1) (X : Type u_2) [Monoid G] [MulAction G X] [TopologicalSpace X] [TopologicalSpace G] [T2Space G] [T2Space X] : T2Space (Quiver.Total (CategoryTheory.ActionCategory G X))

The total arrows of the action category are Hausdorff when the labels and points are.

instance TauCeti.ActionGroupoid.instSecondCountableTopologyArrows (G : Type u_1) (X : Type u_2) [Monoid G] [MulAction G X] [TopologicalSpace X] [TopologicalSpace G] [SecondCountableTopology G] [SecondCountableTopology X] : SecondCountableTopology (Quiver.Total (CategoryTheory.ActionCategory G X))

The total arrows of the action category are second countable when the labels and points are; for a discrete monoid this means that it is countable.

theorem TauCeti.ActionGroupoid.continuous_source (G : Type u_1) (X : Type u_2) [Monoid G] [MulAction G X] [TopologicalSpace X] [TopologicalSpace G] : Continuous Quiver.Total.left

The source of the action groupoid is continuous.

theorem TauCeti.ActionGroupoid.continuous_label (G : Type u_1) (X : Type u_2) [Monoid G] [MulAction G X] [TopologicalSpace X] [TopologicalSpace G] : Continuous fun (f : Quiver.Total (CategoryTheory.ActionCategory G X)) => f.hom.hom

The label of a total arrow is continuous.

theorem TauCeti.ActionGroupoid.continuous_unit (G : Type u_1) (X : Type u_2) [Monoid G] [MulAction G X] [TopologicalSpace X] [TopologicalSpace G] : Continuous fun (x : CategoryTheory.ActionCategory G X) => { left := x, right := x, hom := CategoryTheory.CategoryStruct.id x }

The unit map of the action groupoid is continuous.

theorem TauCeti.ActionGroupoid.continuous_target (G : Type u_1) (X : Type u_2) [Monoid G] [MulAction G X] [TopologicalSpace X] [TopologicalSpace G] [ContinuousSMul G X] : Continuous Quiver.Total.right

The target of the action groupoid is continuous.

theorem TauCeti.ActionGroupoid.continuous_comp (G : Type u_1) (X : Type u_2) [Monoid G] [MulAction G X] [TopologicalSpace X] [TopologicalSpace G] [ContinuousMul G] : Continuous fun (p : { p : Quiver.Total (CategoryTheory.ActionCategory G X) × Quiver.Total (CategoryTheory.ActionCategory G X) // p.1.right = p.2.left }) => (↑p).1.comp (↑p).2 ⋯

Multiplication is continuous on the subspace of composable pairs of total arrows. The first arrow is followed by the second, so the second label multiplies on the left.

def TauCeti.ActionGroupoid.sourceChart (G : Type u_1) (X : Type u_2) [Monoid G] [MulAction G X] [TopologicalSpace X] [TopologicalSpace G] [DiscreteTopology G] (g : G) : OpenPartialHomeomorph (Quiver.Total (CategoryTheory.ActionCategory G X)) (CategoryTheory.ActionCategory G X)

The open source chart of arrows with one fixed label. It keeps distinct labels even when they induce the same action on objects.

@[simp]

theorem TauCeti.ActionGroupoid.sourceChart_apply (G : Type u_1) (X : Type u_2) [Monoid G] [MulAction G X] [TopologicalSpace X] [TopologicalSpace G] [DiscreteTopology G] (g : G) (f : Quiver.Total (CategoryTheory.ActionCategory G X)) : ↑(sourceChart G X g) f = f.left

The fixed-label source chart sends an arrow to its source object.

@[simp]

theorem TauCeti.ActionGroupoid.sourceChart_source (G : Type u_1) (X : Type u_2) [Monoid G] [MulAction G X] [TopologicalSpace X] [TopologicalSpace G] [DiscreteTopology G] (g : G) : (sourceChart G X g).source = {f : Quiver.Total (CategoryTheory.ActionCategory G X) | f.hom.hom = g}

The domain of a fixed-label source chart is exactly that label slice.

@[simp]

theorem TauCeti.ActionGroupoid.sourceChart_target (G : Type u_1) (X : Type u_2) [Monoid G] [MulAction G X] [TopologicalSpace X] [TopologicalSpace G] [DiscreteTopology G] (g : G) : (sourceChart G X g).target = Set.univ

Every object occurs as the source of an arrow with the prescribed label.

@[simp]

theorem TauCeti.ActionGroupoid.sourceChart_symm_apply (G : Type u_1) (X : Type u_2) [Monoid G] [MulAction G X] [TopologicalSpace X] [TopologicalSpace G] [DiscreteTopology G] (g : G) (x : CategoryTheory.ActionCategory G X) : ↑(sourceChart G X g).symm x = (arrowHomeomorph G X).symm (g, x.back)

The inverse source chart constructs the arrow with the prescribed label and source.

theorem TauCeti.ActionGroupoid.isLocalHomeomorph_source (G : Type u_1) (X : Type u_2) [Monoid G] [MulAction G X] [TopologicalSpace X] [TopologicalSpace G] [DiscreteTopology G] : IsLocalHomeomorph Quiver.Total.left

The source of the action category of a discrete monoid is a local homeomorphism.

theorem TauCeti.ActionGroupoid.eventually_back_right_eq_smul {G : Type u_1} {X : Type u_2} [Monoid G] [MulAction G X] [TopologicalSpace X] [TopologicalSpace G] [DiscreteTopology G] (f : Quiver.Total (CategoryTheory.ActionCategory G X)) : ∀ᶠ (a : Quiver.Total (CategoryTheory.ActionCategory G X)) in nhds f, a.right.back = f.hom.hom • a.left.back

Near an arrow f, every arrow has the label of f, so there its target is the translate of its source by that fixed label.

theorem TauCeti.ActionGroupoid.mapTotal_map_eq {G : Type u_1} {X : Type u_2} {N : Type u_3} {Y : Type u_4} [Monoid G] [Monoid N] [MulAction G X] [MulAction N Y] [TopologicalSpace G] [TopologicalSpace N] [TopologicalSpace X] [TopologicalSpace Y] (φ : G →* N) (f : X →ₑ[⇑φ] Y) : (CategoryTheory.ActionCategory.map φ f).toPrefunctor.mapTotal = ⇑(arrowHomeomorph N Y).symm ∘ Prod.map ⇑φ ⇑f ∘ ⇑(arrowHomeomorph G X)

In label-source coordinates, the functor induced by a map f equivariant along φ acts on total arrows as the product of φ and f.

theorem TauCeti.ActionGroupoid.isEmbedding_mapTotal_map {G : Type u_1} {X : Type u_2} {N : Type u_3} {Y : Type u_4} [Monoid G] [Monoid N] [MulAction G X] [MulAction N Y] [TopologicalSpace G] [TopologicalSpace N] [TopologicalSpace X] [TopologicalSpace Y] (φ : G →* N) (f : X →ₑ[⇑φ] Y) (hφ : Topology.IsEmbedding ⇑φ) (hf : Topology.IsEmbedding ⇑f) : Topology.IsEmbedding (CategoryTheory.ActionCategory.map φ f).toPrefunctor.mapTotal

The functor induced by an equivariant embedding along an embedding of monoids is an embedding on total arrows.

theorem TauCeti.ActionGroupoid.isOpenEmbedding_mapTotal_map {G : Type u_1} {X : Type u_2} {N : Type u_3} {Y : Type u_4} [Monoid G] [Monoid N] [MulAction G X] [MulAction N Y] [TopologicalSpace G] [TopologicalSpace N] [TopologicalSpace X] [TopologicalSpace Y] (φ : G →* N) (f : X →ₑ[⇑φ] Y) (hφ : Topology.IsOpenEmbedding ⇑φ) (hf : Topology.IsOpenEmbedding ⇑f) : Topology.IsOpenEmbedding (CategoryTheory.ActionCategory.map φ f).toPrefunctor.mapTotal

The functor induced by an equivariant open embedding along an open embedding of monoids is an open embedding on total arrows.

theorem TauCeti.ActionGroupoid.isEmbedding_mapTotal_restrict {M : Type u_3} {X : Type u_4} [Monoid M] [MulAction M X] (U : SubMulAction M X) [TopologicalSpace M] [TopologicalSpace X] : Topology.IsEmbedding (CategoryTheory.ActionCategory.restrict U).toPrefunctor.mapTotal

The inclusion of the action groupoid on an invariant subset is an embedding on total arrows. In label-source coordinates it is the product of the identity of M and the inclusion of the subset.

theorem TauCeti.ActionGroupoid.continuous_inverse (G : Type u_1) (X : Type u_2) [Group G] [MulAction G X] [TopologicalSpace G] [TopologicalSpace X] [ContinuousInv G] [ContinuousSMul G X] : Continuous fun (f : Quiver.Total (CategoryTheory.ActionCategory G X)) => { left := f.right, right := f.left, hom := CategoryTheory.inv f.hom }

Inversion of arrows is continuous for a continuous action with continuous inversion.

theorem TauCeti.ActionGroupoid.isProperMap_source_target_iff (G : Type u_1) (X : Type u_2) [Group G] [MulAction G X] [TopologicalSpace G] [TopologicalSpace X] : (IsProperMap fun (f : Quiver.Total (CategoryTheory.ActionCategory G X)) => (f.left, f.right)) ↔ ProperSMul G X

Properness of the source-target map of the native action groupoid is exactly properness of the action, with the full group of labels retained.

theorem TauCeti.ActionGroupoid.isLocalHomeomorph_target (G : Type u_1) (X : Type u_2) [Group G] [MulAction G X] [TopologicalSpace G] [TopologicalSpace X] [DiscreteTopology G] [ContinuousConstSMul G X] : IsLocalHomeomorph Quiver.Total.right

The target of the action groupoid of a discrete group is a local homeomorphism.

theorem TauCeti.ActionGroupoid.continuous_uncurry_mapTotal_map {X : Type u_2} {M : Type u_3} {N : Type u_4} {Y : Type u_5} [Monoid M] [Monoid N] [MulAction M X] [MulAction N Y] [TopologicalSpace M] [TopologicalSpace N] [TopologicalSpace X] [TopologicalSpace Y] {T : Type u_6} [TopologicalSpace T] {φ : M →* N} (hφ : Continuous ⇑φ) {f : T → X →ₑ[⇑φ] Y} (hf : Continuous fun (p : T × X) => (f p.1) p.2) : Continuous fun (p : T × Quiver.Total (CategoryTheory.ActionCategory M X)) => (CategoryTheory.ActionCategory.map φ (f p.1)).toPrefunctor.mapTotal p.2

The functors of action groupoids induced by a family of equivariant maps along a continuous monoid homomorphism, depending continuously on a parameter and the point, are jointly continuous in the parameter and the total arrow.

theorem TauCeti.ActionGroupoid.continuous_mapTotal_map {X : Type u_2} {M : Type u_3} {N : Type u_4} {Y : Type u_5} [Monoid M] [Monoid N] [MulAction M X] [MulAction N Y] [TopologicalSpace M] [TopologicalSpace N] [TopologicalSpace X] [TopologicalSpace Y] {φ : M →* N} (hφ : Continuous ⇑φ) {f : X →ₑ[⇑φ] Y} (hf : Continuous ⇑f) : Continuous (CategoryTheory.ActionCategory.map φ f).toPrefunctor.mapTotal

The functor of action groupoids induced by a continuous equivariant map along a continuous monoid homomorphism is continuous on total arrows.