The coarse topology of a groupoid

The coarse space of a categorical groupoid is the native quotient of its objects by CategoryTheory.isIsomorphicSetoid, with the quotient topology. A continuous source and an open target make the quotient projection open. A closed source-target range then makes the coarse space Hausdorff. In particular these conclusions apply to proper étale presentations. No topology on individual hom types, and no replacement groupoid carrier, is needed.

Second countability and local compactness descend along the open quotient by Topology.IsOpenQuotientMap.secondCountableTopology and Topology.IsOpenQuotientMap.locallyCompactSpace. Together with Hausdorffness, these give paracompactness when the object space is locally compact and second countable. This is the topology needed for partitions of unity and locally finite covers on an orbifold coarse space. The hypotheses concern actual total arrows; ineffective isotropy is not removed.

References

• I. Moerdijk, Orbifolds as groupoids: an introduction, Section 2.

theorem TauCeti.isomorphismClassesMk_eq_iff {C : Type u_1} [CategoryTheory.Groupoid C] {x y : C} : ⟦x⟧ = ⟦y⟧ ↔ Nonempty (x ⟶ y)

Two objects have the same isomorphism class exactly when there is an arrow between them.

theorem TauCeti.isomorphismClasses_preimage_image_eq {C : Type u_1} [CategoryTheory.Groupoid C] {U : Set C} : Quotient.mk (CategoryTheory.isIsomorphicSetoid C) ⁻¹' Quotient.mk (CategoryTheory.isIsomorphicSetoid C) '' U = Quiver.Total.right '' Quiver.Total.left ⁻¹' U

Saturating a set of objects amounts to taking targets of arrows with source in the set.

theorem TauCeti.setOf_isomorphismClassesMk_eq_eq_range {C : Type u_1} [CategoryTheory.Groupoid C] : {p : C × C | ⟦p.1⟧ = ⟦p.2⟧} = Set.range fun (a : Quiver.Total C) => (a.left, a.right)

The relation of having equal isomorphism classes is the range of the source-target map.

theorem TauCeti.injective_of_mk_eq_isomorphismClassesMk {C : Type u_1} [CategoryTheory.Groupoid C] {U : Set C} {r : Setoid ↑U} {φ : Quotient r → Quotient (CategoryTheory.isIsomorphicSetoid C)} (hr : ∀ (y y' : ↑U), Nonempty (↑y ⟶ ↑y') → r y y') (hφ : ∀ (y : ↑U), φ ⟦y⟧ = ⟦↑y⟧) : Function.Injective φ

Let r be a relation on a set U of objects that relates any two objects joined by an arrow, for instance the restriction of isIsomorphicSetoid C. A map from U / r to the isomorphism classes sending the class of each y to the isomorphism class of y is injective. Such a map exists only if r relates no other objects, so r is then the restriction of isIsomorphicSetoid C.

theorem TauCeti.isOpenQuotientMap_isomorphismClassesMk {C : Type u_1} [CategoryTheory.Groupoid C] [TopologicalSpace C] [TopologicalSpace (Quiver.Total C)] (hs : Continuous Quiver.Total.left) (ht : IsOpenMap Quiver.Total.right) : IsOpenQuotientMap (Quotient.mk (CategoryTheory.isIsomorphicSetoid C))

With continuous source and open target, the projection to isomorphism classes is an open quotient map. Local homeomorphisms satisfy both hypotheses.

theorem TauCeti.t2Space_isomorphismClasses {C : Type u_1} [CategoryTheory.Groupoid C] [TopologicalSpace C] [TopologicalSpace (Quiver.Total C)] (hs : Continuous Quiver.Total.left) (ht : IsOpenMap Quiver.Total.right) (hc : IsClosed (Set.range fun (a : Quiver.Total C) => (a.left, a.right))) : T2Space (Quotient (CategoryTheory.isIsomorphicSetoid C))

A groupoid with continuous source, open target and closed source-target range has a Hausdorff coarse quotient. Properness of the source-target map is sufficient; neither the objects nor arrows need an additional separation hypothesis here.

theorem TauCeti.paracompactSpace_isomorphismClasses {C : Type u_1} [CategoryTheory.Groupoid C] [TopologicalSpace C] [TopologicalSpace (Quiver.Total C)] [LocallyCompactSpace C] [SecondCountableTopology C] (hs : Continuous Quiver.Total.left) (ht : IsOpenMap Quiver.Total.right) (hc : IsClosed (Set.range fun (a : Quiver.Total C) => (a.left, a.right))) : ParacompactSpace (Quotient (CategoryTheory.isIsomorphicSetoid C))

The coarse quotient of a locally compact, second-countable groupoid is paracompact when source is continuous, target is open and the source-target range is closed. In particular this applies to Hausdorff second-countable proper étale manifold presentations.

theorem TauCeti.isOpenEmbedding_of_mk_eq_isomorphismClassesMk {C : Type u_1} [CategoryTheory.Groupoid C] [TopologicalSpace C] [TopologicalSpace (Quiver.Total C)] {U : Set C} {r : Setoid ↑U} {φ : Quotient r → Quotient (CategoryTheory.isIsomorphicSetoid C)} (hU : IsOpen U) (hs : Continuous Quiver.Total.left) (ht : IsOpenMap Quiver.Total.right) (hr : ∀ (y y' : ↑U), Nonempty (↑y ⟶ ↑y') → r y y') (hφ : ∀ (y : ↑U), φ ⟦y⟧ = ⟦↑y⟧) : Topology.IsOpenEmbedding φ

Open subsets give open pieces of the coarse space. Let r be a relation on an open set U of objects that relates any two objects joined by an arrow. With continuous source and open target, a map from U / r to the isomorphism classes sending the class of each y to the isomorphism class of y is an open embedding. So the coarse space of the full subgroupoid on U is an open subspace of the coarse space.