The groupoid of C^n local diffeomorphisms of a manifold

For a manifold X modelled on I, the open partial homeomorphisms e of X such that e is C^n on its source and e.symm is C^n on its target form a structure groupoid TauCeti.contMDiffGroupoid I n X on X. It plays for a manifold the role that Mathlib's contDiffGroupoid plays for a model space, with smoothness read through the charts of X.

Its use is to build manifolds in two stages. A space M charted over the manifold X, whose transition maps are C^n local diffeomorphisms of X, is a C^n manifold modelled on I for the composite charts ChartedSpace.comp H X M (TauCeti.isManifold_of_hasGroupoid_contMDiffGroupoid). For instance, the total space of a fibre bundle is charted over the product of its base and its fibre by its trivializations, and its smooth atlas is obtained in this way when the fibre is itself a manifold.

Main definitions

• TauCeti.contMDiffPregroupoid I n X: the maps of X that are C^n on a set.
• TauCeti.contMDiffGroupoid I n X: the open partial homeomorphisms of X that are C^n with C^n inverse.

Main results

• TauCeti.mem_contMDiffGroupoid_iff: membership is smoothness of the map on its source and of its inverse on its target.
• TauCeti.isManifold_of_hasGroupoid_contMDiffGroupoid: a space charted over a C^n manifold X with transitions in contMDiffGroupoid I n X is a C^n manifold for the composite charts.

def TauCeti.contMDiffPregroupoid {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] (I : ModelWithCorners 𝕜 E H) (n : WithTop ℕ∞) (X : Type u_4) [TopologicalSpace X] [ChartedSpace H X] : Pregroupoid X

The pregroupoid of maps of a manifold X modelled on I that are C^n on a set.

def TauCeti.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 ℕ∞) (X : Type u_4) [TopologicalSpace X] [ChartedSpace H X] : StructureGroupoid X

The structure groupoid of C^n local diffeomorphisms of a manifold X modelled on I: the open partial homeomorphisms of X that are C^n on their source, with inverse C^n on their target.

@[simp]

theorem TauCeti.contMDiffPregroupoid_property {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {n : WithTop ℕ∞} {X : Type u_4} [TopologicalSpace X] [ChartedSpace H X] {f : X → X} {u : Set X} : (contMDiffPregroupoid I n X).property f u ↔ ContMDiffOn I I n f u

theorem TauCeti.mem_contMDiffGroupoid_iff {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {n : WithTop ℕ∞} {X : Type u_4} [TopologicalSpace X] [ChartedSpace H X] {e : OpenPartialHomeomorph X X} : e ∈ contMDiffGroupoid I n X ↔ ContMDiffOn I I n (↑e) e.source ∧ ContMDiffOn I I n (↑e.symm) e.target

An open partial homeomorphism of X is a C^n local diffeomorphism when it is C^n on its source and its inverse is C^n on its target.

theorem TauCeti.isManifold_of_hasGroupoid_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 ℕ∞) {X : Type u_4} [TopologicalSpace X] [ChartedSpace H X] [IsManifold I n X] (M : Type u_5) [TopologicalSpace M] [ChartedSpace X M] [HasGroupoid M (contMDiffGroupoid I n X)] : IsManifold I n M

A space M charted over a C^n manifold X modelled on I, whose transition maps are C^n local diffeomorphisms of X, is a C^n manifold for the composite charts ChartedSpace.comp H X M.