(G, X)-manifolds

Let a group G act on a topological space X by homeomorphisms. Thurston's pseudogroup generated by G consists of the homeomorphisms between open subsets of X that agree, near each point of their domain, with the action of some element of G. In Mathlib's language this is a structure groupoid on X, TauCeti.smulGroupoid G X, built from the pregroupoid TauCeti.smulPregroupoid G X exactly as contDiffGroupoid and conformalGroupoid are built from theirs.

A (G, X)-manifold is then a charted space M over X whose transition maps lie in this groupoid, that is [ChartedSpace X M] [HasGroupoid M (smulGroupoid G X)]; no new structure is introduced. Specialising (G, X) gives the classical geometric structures: Euclidean manifolds for the isometries of Euclidean space, spherical manifolds for the orthogonal group acting on the sphere, and hyperbolic manifolds for the isometries of hyperbolic space.

Two results connect this notion to the rest of the manifold library.

• If X is a C^n manifold modelled on I and G acts by C^n maps, then a (G, X)-manifold is a C^n manifold for the charts obtained by composing its X-valued charts with the charts of X (TauCeti.isManifold_of_hasGroupoid_smulGroupoid). So geometric structures are in particular smooth structures.
• The orbit space X / Γ of a free, properly discontinuous action of a group Γ, with the charts of MulAction.instChartedSpaceQuotient, is a (Γ, X)-manifold (TauCeti.hasGroupoid_smulGroupoid_quotient), and a (G, X)-manifold when Γ is a subgroup of G (TauCeti.hasGroupoid_smulGroupoid_quotient_subgroup). This is the source of (G, X)-manifolds of the form X / Γ. More generally, the charts pushed forward along a surjective local homeomorphism X → M whose deck transformations are locally given by G form a (G, X)-atlas (IsLocalHomeomorph.hasGroupoid_smulGroupoid_chartedSpaceOfRightInverse).

The deck-transformation hypothesis has the shape of the one in IsLocalHomeomorph.isManifold_chartedSpaceOfRightInverse (TauCeti/Geometry/Manifold/Instances/Quotient.lean), where the deck transformations are only required to be C^n. The developing map and completeness of a (G, X)-structure are not treated here.

Main definitions

• TauCeti.smulPregroupoid G X: maps of X that agree near each point of a set with the action of an element of G.
• TauCeti.smulGroupoid G X: the structure groupoid of open partial homeomorphisms of X that are locally given by the action of G.

Main results

• TauCeti.mem_smulGroupoid_iff: an open partial homeomorphism lies in smulGroupoid G X as soon as it is locally given by the action of G; the inverse is then automatically of the same kind.
• TauCeti.hasGroupoid_smulGroupoid_iff: a charted space over X is a (G, X)-manifold exactly when its transition maps are locally given by the action of G.
• TauCeti.exists_smul_eventuallyEq_chartAt: near each point of its source, a chart of a (G, X)-manifold is the preferred chart there followed by the action of an element of G.
• TauCeti.smulGroupoid_le: a group whose action is realised by another group's action gives a smaller groupoid.
• TauCeti.contMDiffOn_of_mem_smulGroupoid: for an action by C^n maps, every member of smulGroupoid G X is C^n on its source.
• TauCeti.smulGroupoid_le_contMDiffGroupoid: for an action by C^n maps, smulGroupoid G X is contained in the groupoid TauCeti.contMDiffGroupoid I n X of C^n local diffeomorphisms.
• TauCeti.isManifold_of_hasGroupoid_smulGroupoid: a (G, X)-manifold is a C^n manifold when G acts by C^n maps on the C^n manifold X.
• TauCeti.contMDiffOn_of_mem_atlas_of_hasGroupoid_smulGroupoid: each X-valued chart of such a manifold is then C^n on its source.
• TauCeti.hasGroupoid_smulGroupoid_quotient: the orbit space of a free, properly discontinuous action of Γ on X is a (Γ, X)-manifold.

References

• W. P. Thurston, Three-Dimensional Geometry and Topology, Vol. 1, Princeton University Press, 1997, Definitions 3.1.1 and 3.1.2 (pseudogroups and 𝒢-manifolds) and Section 3.3 ((G, X)- manifolds, Examples 3.3.2, 3.3.5 and 3.3.6).

def TauCeti.smulPregroupoid (G : Type u_1) (X : Type u_2) [Monoid G] [TopologicalSpace X] [MulAction G X] [ContinuousConstSMul G X] : Pregroupoid X

The pregroupoid of maps of X that are locally given by the action of G: a map f has the property on u if near each point of u it agrees with x ↦ g • x for some g : G.

def TauCeti.smulGroupoid (G : Type u_1) (X : Type u_2) [Monoid G] [TopologicalSpace X] [MulAction G X] [ContinuousConstSMul G X] : StructureGroupoid X

The structure groupoid of open partial homeomorphisms of X that are locally given by the action of G. When G is a group, this is Thurston's pseudogroup generated by G, and a charted space over X with this groupoid is a (G, X)-manifold.

@[simp]

theorem TauCeti.smulPregroupoid_property {G : Type u_1} {X : Type u_2} [Monoid G] [TopologicalSpace X] [MulAction G X] [ContinuousConstSMul G X] {f : X → X} {u : Set X} : (smulPregroupoid G X).property f u ↔ ∀ x ∈ u, ∃ (g : G), f =ᶠ[nhds x] fun (x : X) => g • x

theorem TauCeti.smulGroupoid_le {G : Type u_1} {X : Type u_2} [Monoid G] [TopologicalSpace X] [MulAction G X] [ContinuousConstSMul G X] {G' : Type u_3} [Monoid G'] [MulAction G' X] [ContinuousConstSMul G' X] (h : ∀ (g : G), ∃ (g' : G'), ∀ (x : X), g • x = g' • x) : smulGroupoid G X ≤ smulGroupoid G' X

If the action of each element of G on X is the action of some element of G', then every map locally given by G is locally given by G'. This applies in particular to a subgroup of G' and to a group acting through a homomorphism to G'.

theorem TauCeti.mem_smulGroupoid_iff {G : Type u_1} {X : Type u_2} [Group G] [TopologicalSpace X] [MulAction G X] [ContinuousConstSMul G X] {e : OpenPartialHomeomorph X X} : e ∈ smulGroupoid G X ↔ ∀ x ∈ e.source, ∃ (g : G), ↑e =ᶠ[nhds x] fun (x : X) => g • x

An open partial homeomorphism of X lies in smulGroupoid G X exactly when it is locally given by the action of G on its source. The same condition on the inverse then holds automatically.

theorem TauCeti.smul_mem_smulGroupoid {G : Type u_1} {X : Type u_2} [Group G] [TopologicalSpace X] [MulAction G X] [ContinuousConstSMul G X] (g : G) : (Homeomorph.smul g).toOpenPartialHomeomorph ∈ smulGroupoid G X

The action of an element of G, as a homeomorphism of X, lies in smulGroupoid G X.

theorem TauCeti.hasGroupoid_smulGroupoid_iff {G : Type u_1} {X : Type u_2} [Group G] [TopologicalSpace X] [MulAction G X] [ContinuousConstSMul G X] {M : Type u_3} [TopologicalSpace M] [ChartedSpace X M] : HasGroupoid M (smulGroupoid G X) ↔ ∀ e ∈ atlas X M, ∀ e' ∈ atlas X M, ∀ x ∈ (e.symm.trans e').source, ∃ (g : G), ↑(e.symm.trans e') =ᶠ[nhds x] fun (x : X) => g • x

A charted space over X is a (G, X)-manifold exactly when each transition map between two of its charts agrees, near each point of its source, with the action of an element of G.

theorem TauCeti.exists_smul_eventuallyEq_chartAt {G : Type u_1} {X : Type u_2} [Group G] [TopologicalSpace X] [MulAction G X] [ContinuousConstSMul G X] {M : Type u_3} [TopologicalSpace M] [ChartedSpace X M] [HasGroupoid M (smulGroupoid G X)] {e : OpenPartialHomeomorph M X} (he : e ∈ atlas X M) {y : M} (hy : y ∈ e.source) : ∃ (g : G), ↑e =ᶠ[nhds y] fun (z : M) => g • ↑(chartAt X y) z

Near a point y of its source, every chart of a (G, X)-manifold is the preferred chart at y followed by the action of an element of G.

instance TauCeti.instClosedUnderRestrictionSmulGroupoid {G : Type u_1} {X : Type u_2} [Group G] [TopologicalSpace X] [MulAction G X] [ContinuousConstSMul G X] : ClosedUnderRestriction (smulGroupoid G X)

The groupoid smulGroupoid G X is closed under restriction, so open subsets of a (G, X)-manifold inherit the same (G, X)-structure.

(G, X)-manifolds are C^n manifolds

theorem TauCeti.contMDiffOn_of_mem_smulGroupoid {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {n : WithTop ℕ∞} {G : Type u_4} {X : Type u_5} [Monoid G] [TopologicalSpace X] [ChartedSpace H X] [MulAction G X] [ContinuousConstSMul G X] [ContMDiffConstSMul I n G X] {e : OpenPartialHomeomorph X X} (he : e ∈ smulGroupoid G X) : ContMDiffOn I I n (↑e) e.source

When G acts on X by C^n maps, every member of smulGroupoid G X is C^n on its source.

theorem TauCeti.smulGroupoid_le_contMDiffGroupoid {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] (I : ModelWithCorners 𝕜 E H) (n : WithTop ℕ∞) (G : Type u_4) (X : Type u_5) [Monoid G] [TopologicalSpace X] [ChartedSpace H X] [MulAction G X] [ContinuousConstSMul G X] [ContMDiffConstSMul I n G X] : smulGroupoid G X ≤ contMDiffGroupoid I n X

When G acts on X by C^n maps, every member of smulGroupoid G X is a C^n local diffeomorphism of X.

theorem TauCeti.isManifold_of_hasGroupoid_smulGroupoid {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] (I : ModelWithCorners 𝕜 E H) (n : WithTop ℕ∞) (G : Type u_4) {X : Type u_5} [Monoid G] [TopologicalSpace X] [ChartedSpace H X] [MulAction G X] [ContinuousConstSMul G X] [ContMDiffConstSMul I n G X] [IsManifold I n X] (M : Type u_6) [TopologicalSpace M] [ChartedSpace X M] [HasGroupoid M (smulGroupoid G X)] : IsManifold I n M

A (G, X)-manifold, for an action of G by C^n maps on a C^n manifold X modelled on I, is a C^n manifold for the composite charts ChartedSpace.comp H X M.

theorem TauCeti.contMDiffOn_of_mem_atlas_of_hasGroupoid_smulGroupoid {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {n : WithTop ℕ∞} (G : Type u_4) {X : Type u_5} [Group G] [TopologicalSpace X] [ChartedSpace H X] [MulAction G X] [ContinuousConstSMul G X] [ContMDiffConstSMul I n G X] {M : Type u_6} [TopologicalSpace M] [ChartedSpace X M] [HasGroupoid M (smulGroupoid G X)] {e : OpenPartialHomeomorph M X} (he : e ∈ atlas X M) : ContMDiffOn I I n (↑e) e.source

In a (G, X)-manifold, for an action of G by C^n maps, every X-valued chart is C^n on its source for the composite charts ChartedSpace.comp H X M.

Quotients and deck transformations

theorem IsLocalHomeomorph.hasGroupoid_smulGroupoid_chartedSpaceOfRightInverse {G : Type u_1} {X : Type u_2} [Group G] [TopologicalSpace X] [MulAction G X] [ContinuousConstSMul G X] {M : Type u_3} [TopologicalSpace M] {f : X → M} (hf : IsLocalHomeomorph f) {s : M → X} (hs : Function.RightInverse s f) (hdeck : ∀ (z w : X), f z = f w → ∃ (g : G), g • z = w ∧ (f ∘ fun (x : X) => g • x) =ᶠ[nhds z] f) : HasGroupoid M (TauCeti.smulGroupoid G X)

Let f : X → M be a local homeomorphism with a right inverse, whose deck transformations are locally given by the action of G: whenever f z = f w, some g : G sends z to w and satisfies f (g • y) = f y for y near z. Then the charts that f pushes forward from X make M a (G, X)-manifold.

instance TauCeti.hasGroupoid_smulGroupoid_quotient {X : Type u_2} [TopologicalSpace X] [T2Space X] [LocallyCompactSpace X] (Γ : Type u_4) [Group Γ] [MulAction Γ X] [ContinuousConstSMul Γ X] [ProperlyDiscontinuousSMul Γ X] [IsCancelSMul Γ X] : HasGroupoid (MulAction.orbitRel.Quotient Γ X) (smulGroupoid Γ X)

The orbit space of a free, properly discontinuous action of a group Γ on X, with the charts pushed forward along the orbit projection, is a (Γ, X)-manifold.

instance TauCeti.hasGroupoid_smulGroupoid_quotient_subgroup {G : Type u_1} {X : Type u_2} [Group G] [TopologicalSpace X] [MulAction G X] [ContinuousConstSMul G X] [T2Space X] [LocallyCompactSpace X] (Γ : Subgroup G) [ProperlyDiscontinuousSMul (↥Γ) X] [IsCancelSMul (↥Γ) X] : HasGroupoid (MulAction.orbitRel.Quotient (↥Γ) X) (smulGroupoid G X)

The orbit space X / Γ of a free, properly discontinuous action of a subgroup Γ of G is a (G, X)-manifold.