Continuous maps from group quotients and compact orbit spaces

This file records continuity results for maps out of group quotients that do not require transitivity of an action, and a compactness criterion for orbit spaces.

The orbit space of an action is compact as soon as some compact set meets every orbit, since the orbit space is then the image of that set under the continuous orbit projection. When the action is by homeomorphisms and the space is weakly locally compact, for instance a finite-dimensional manifold, this is also necessary: the orbit projection is open, so the compact orbit space is the image of a compact set. For a free properly discontinuous action this is how compactness of a quotient manifold is read off from a compact fundamental domain upstairs.

Main results

• TauCeti.continuous_ofQuotientStabilizer proves continuity of the orbit map descended to a stabilizer quotient when the corresponding orbit map is continuous.
• TauCeti.continuous_orbitRelQuotientLift_iff: the descent of a G-invariant map to the orbit space is continuous exactly when the map is.
• TauCeti.continuous_section_orbitRelQuotientRec_iff: the descent of a G-invariant section of the pullback of a family V over the orbit space is continuous, as a map into the total space, exactly when the section upstairs is.
• MulActionHom.isEmbedding_orbitRelQuotientMap: an equivariant embedding descends to an embedding of orbit spaces when the acting-group map is surjective and the target action is by homeomorphisms.
• SubMulAction.isOpenEmbedding_orbitRelQuotientMap: for an open slice S for a subgroup H, an H-invariant open set moved into itself only by elements of H, the map S / H → X / G of orbit spaces is an open embedding. For H = ⊥ this recovers TauCeti.isOpenEmbedding_quotientMk_domRestrict_of_disjoint_smul.
• TauCeti.MulAction.compactSpace_orbitRelQuotient_of_isCompact: if a compact set meets every orbit, the orbit space is compact.
• TauCeti.MulAction.compactSpace_orbitRelQuotient_iff_exists_isCompact: for an action by homeomorphisms of a weakly locally compact space, the orbit space is compact exactly when some compact set meets every orbit.

Both compactness statements have additive versions for AddAction.orbitRel.Quotient.

theorem TauCeti.continuous_orbitRelQuotientLift_iff {G : Type u_1} {X : Type u_2} {Y : Type u_3} [Group G] [MulAction G X] [TopologicalSpace X] [TopologicalSpace Y] {f : X → Y} {hf : ∀ (g : G) (x : X), f (g • x) = f x} : Continuous (MulAction.orbitRelQuotientLift f hf) ↔ Continuous f

The descent of a G-invariant map to the orbit space is continuous exactly when the map is.

theorem TauCeti.continuous_section_orbitRelQuotientRec_iff {G : Type u_1} {X : Type u_2} [Group G] [MulAction G X] [TopologicalSpace X] {F : Type u_4} {V : MulAction.orbitRel.Quotient G X → Type u_5} [TopologicalSpace (Bundle.TotalSpace F V)] {t : (x : X) → V ⟦x⟧} {ht : ∀ (g : G) (x : X), t (g • x) ≍ t x} : (Continuous fun (q : MulAction.orbitRel.Quotient G X) => Bundle.TotalSpace.mk' F q (MulAction.orbitRelQuotientRec t ht q)) ↔ Continuous fun (x : X) => Bundle.TotalSpace.mk' F ⟦x⟧ (t x)

The descent of an invariant section is continuous, as a map into the total space, exactly when the section upstairs is.

theorem SubMulAction.isOpenEmbedding_orbitRelQuotientMap {G : Type u_1} {X : Type u_2} [Group G] [MulAction G X] [TopologicalSpace X] [ContinuousConstSMul G X] {H : Subgroup G} (S : SubMulAction (↥H) X) (hS_open : IsOpen ↑S) (hS : ∀ (g : G), ∀ y ∈ S, g • y ∈ S → g ∈ H) : Topology.IsOpenEmbedding S.orbitRelQuotientMap

Orbit spaces of open slices. Let S be an open H-invariant subset of X such that every element of G carrying a point of S into S lies in H. Then the map S / H → X / G sending an H-orbit to its G-orbit is an open embedding of orbit spaces.

theorem MulActionHom.isEmbedding_orbitRelQuotientMap {G : Type u_1} {H : Type u_2} {X : Type u_3} {Y : Type u_4} [Group G] [Group H] [MulAction G X] [MulAction H Y] [TopologicalSpace X] [TopologicalSpace Y] [ContinuousConstSMul H Y] {σ : G → H} (φ : X →ₑ[σ] Y) (hφ : Topology.IsEmbedding ⇑φ) (hσ : Function.Surjective σ) : Topology.IsEmbedding φ.orbitRelQuotientMap

An equivariant embedding descends to an embedding of orbit spaces when the map of acting groups is surjective and the target action is by homeomorphisms.

theorem TauCeti.MulAction.compactSpace_orbitRelQuotient_of_isCompact {G : Type u_1} {X : Type u_2} [Group G] [MulAction G X] [TopologicalSpace X] {K : Set X} (hK : IsCompact K) (hKG : ∀ (x : X), ∃ (g : G), g • x ∈ K) : CompactSpace (MulAction.orbitRel.Quotient G X)

Compact fundamental domain. If a compact set K meets every orbit, the orbit space is compact: it is the image of K under the continuous orbit projection.

theorem TauCeti.AddAction.compactSpace_orbitRelQuotient_of_isCompact {G : Type u_1} {X : Type u_2} [AddGroup G] [AddAction G X] [TopologicalSpace X] {K : Set X} (hK : IsCompact K) (hKG : ∀ (x : X), ∃ (g : G), g +ᵥ x ∈ K) : CompactSpace (AddAction.orbitRel.Quotient G X)

Compact fundamental domain. If a compact set K meets every orbit of an additive action, the orbit space is compact: it is the image of K under the continuous orbit projection.

theorem TauCeti.MulAction.compactSpace_orbitRelQuotient_iff_exists_isCompact {G : Type u_1} {X : Type u_2} [Group G] [MulAction G X] [TopologicalSpace X] [ContinuousConstSMul G X] [WeaklyLocallyCompactSpace X] : CompactSpace (MulAction.orbitRel.Quotient G X) ↔ ∃ (K : Set X), IsCompact K ∧ ∀ (x : X), ∃ (g : G), g • x ∈ K

For an action by homeomorphisms of a weakly locally compact space, the orbit space is compact exactly when some compact set meets every orbit.

theorem TauCeti.AddAction.compactSpace_orbitRelQuotient_iff_exists_isCompact {G : Type u_1} {X : Type u_2} [AddGroup G] [AddAction G X] [TopologicalSpace X] [ContinuousConstVAdd G X] [WeaklyLocallyCompactSpace X] : CompactSpace (AddAction.orbitRel.Quotient G X) ↔ ∃ (K : Set X), IsCompact K ∧ ∀ (x : X), ∃ (g : G), g +ᵥ x ∈ K

For an additive action by homeomorphisms of a weakly locally compact space, the orbit space is compact exactly when some compact set meets every orbit.

theorem TauCeti.continuous_ofQuotientStabilizer (G : Type u_1) {X : Type u_2} [Group G] [TopologicalSpace G] [TopologicalSpace X] [MulAction G X] (b : X) (hb : Continuous fun (g : G) => g • b) : Continuous (MulAction.ofQuotientStabilizer G b)

The orbit map descended to the stabilizer quotient is continuous when the orbit map is.