Quotient manifolds of free properly discontinuous actions

Mathlib equips the orbit space of a free, properly discontinuous action on a charted space with charts pushed forward along the orbit projection (MulAction.instChartedSpaceQuotient). This file proves that for an action by C^n maps on a C^n manifold these charts form a C^n manifold, and that the orbit projection is a C^n local diffeomorphism.

The argument is local and applies to any surjective local homeomorphism f : M → M' with the pushed-forward charts IsLocalHomeomorph.chartedSpaceOfRightInverse. The only input is that f has C^n local deck transformations: whenever f z = f w, some map that is C^n at z sends z to w and commutes with f near z. Then every composite of a local inverse of f with f is locally such a map, so the transition maps of the pushed-forward atlas are C^n maps of M read in charts of M. For an orbit projection the deck transformations are the group elements themselves.

A properly discontinuous action that is not free is free on its free locus TauCeti.freeLocus, an open invariant subset. The free locus inherits the charts of the ambient manifold and the C^n action, so the results above make its orbit space a C^n manifold by instance search.

Main results

• IsLocalHomeomorph.isManifold_chartedSpaceOfRightInverse, IsLocalHomeomorph.contMDiff_chartedSpaceOfRightInverse, IsLocalHomeomorph.isLocalDiffeomorph_chartedSpaceOfRightInverse: the pushed-forward charts of a local homeomorphism with C^n local deck transformations form a C^n manifold, for which the map is a C^n local diffeomorphism.
• TauCeti.instIsManifoldQuotient: the orbit space of a free, properly discontinuous action by C^n maps on a C^n manifold is a C^n manifold.
• TauCeti.isLocalDiffeomorph_quotientMk: the orbit projection is a C^n local diffeomorphism.
• TauCeti.freeLocus.instChartedSpace, TauCeti.freeLocus.instIsManifold and TauCeti.freeLocus.instContMDiffConstSMul: the free locus of a properly discontinuous action is an open submanifold on which the group acts by C^n maps.

References

• John M. Lee, Introduction to Smooth Manifolds, second edition, Graduate Texts in Mathematics 218, Springer, 2013, Chapter 21 (quotients by discrete group actions).

theorem IsLocalHomeomorph.isManifold_chartedSpaceOfRightInverse {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {n : WithTop ℕ∞} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] {M' : Type u_5} [TopologicalSpace M'] {f : M → M'} (hf : IsLocalHomeomorph f) {g : M' → M} (hg : Function.RightInverse g f) [IsManifold I n M] (hdeck : ∀ (z w : M), f z = f w → ∃ (φ : M → M), ContMDiffAt I I n φ z ∧ φ z = w ∧ f ∘ φ =ᶠ[nhds z] f) : IsManifold I n M'

The charts that a local homeomorphism f with C^n local deck transformations pushes forward from a C^n manifold form a C^n manifold.

theorem IsLocalHomeomorph.contMDiff_chartedSpaceOfRightInverse {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {n : WithTop ℕ∞} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] {M' : Type u_5} [TopologicalSpace M'] {f : M → M'} (hf : IsLocalHomeomorph f) {g : M' → M} (hg : Function.RightInverse g f) [IsManifold I n M] (hdeck : ∀ (z w : M), f z = f w → ∃ (φ : M → M), ContMDiffAt I I n φ z ∧ φ z = w ∧ f ∘ φ =ᶠ[nhds z] f) : ContMDiff I I n f

A local homeomorphism with C^n local deck transformations is C^n for the charts it pushes forward from a C^n manifold.

theorem IsLocalHomeomorph.isLocalDiffeomorph_chartedSpaceOfRightInverse {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {n : WithTop ℕ∞} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] {M' : Type u_5} [TopologicalSpace M'] {f : M → M'} (hf : IsLocalHomeomorph f) {g : M' → M} (hg : Function.RightInverse g f) [IsManifold I n M] (hdeck : ∀ (z w : M), f z = f w → ∃ (φ : M → M), ContMDiffAt I I n φ z ∧ φ z = w ∧ f ∘ φ =ᶠ[nhds z] f) : IsLocalDiffeomorph I I n f

A local homeomorphism with C^n local deck transformations is a C^n local diffeomorphism for the charts it pushes forward from a C^n manifold.

instance TauCeti.instIsManifoldQuotient {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {n : WithTop ℕ∞} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] {G : Type u_5} [Group G] [MulAction G M] [ContMDiffConstSMul I n G M] [ProperlyDiscontinuousSMul G M] [ContinuousConstSMul G M] [IsCancelSMul G M] [T2Space M] [LocallyCompactSpace M] [IsManifold I n M] : IsManifold I n (MulAction.orbitRel.Quotient G M)

The orbit space of a free, properly discontinuous action by C^n maps on a C^n manifold is a C^n manifold, for the charts pushed forward along the orbit projection.

theorem TauCeti.isLocalDiffeomorph_quotientMk {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {n : WithTop ℕ∞} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] {G : Type u_5} [Group G] [MulAction G M] [ContMDiffConstSMul I n G M] [ProperlyDiscontinuousSMul G M] [ContinuousConstSMul G M] [IsCancelSMul G M] [T2Space M] [LocallyCompactSpace M] [IsManifold I n M] : IsLocalDiffeomorph I I n (Quotient.mk (MulAction.orbitRel G M))

The orbit projection of a free, properly discontinuous action by C^n maps on a C^n manifold is a C^n local diffeomorphism.

The free locus

@[instance_reducible]

noncomputable instance TauCeti.freeLocus.instChartedSpace {H : Type u_3} [TopologicalSpace H] {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] {G : Type u_5} [Group G] [MulAction G M] [ProperlyDiscontinuousSMul G M] [ContinuousConstSMul G M] [T2Space M] [LocallyCompactSpace M] : ChartedSpace H ↥(freeLocus G M)

The free locus of a properly discontinuous action is open, so it inherits the charts of the ambient charted space.

Equations

• One or more equations did not get rendered due to their size.

instance TauCeti.freeLocus.instIsManifold {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {n : WithTop ℕ∞} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] {G : Type u_5} [Group G] [MulAction G M] [ProperlyDiscontinuousSMul G M] [ContinuousConstSMul G M] [T2Space M] [LocallyCompactSpace M] [IsManifold I n M] : IsManifold I n ↥(freeLocus G M)

The free locus of a properly discontinuous action on a C^n manifold is a C^n manifold.

instance TauCeti.freeLocus.instContMDiffConstSMul {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {n : WithTop ℕ∞} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] {G : Type u_5} [Group G] [MulAction G M] [ProperlyDiscontinuousSMul G M] [ContinuousConstSMul G M] [T2Space M] [LocallyCompactSpace M] [ContMDiffConstSMul I n G M] : ContMDiffConstSMul I n G ↥(freeLocus G M)

An action by C^n maps restricts to an action by C^n maps on the free locus.