Continuity of composition of diffeomorphisms

For compact source manifolds with locally compact models, composition of C^n diffeomorphisms is jointly continuous for the weak Whitney topology, since the forgetful map to C^n maps is an embedding and composition of C^n maps is continuous (ContMDiffMap.continuous_comp_manifoldWeakWhitney). In particular the self-diffeomorphisms of a compact manifold form a topological monoid. Continuity of inversion is a separate matter, as it needs an inverse-function estimate.

Main results

• Diffeomorph.continuous_trans: composition of diffeomorphisms is jointly continuous.
• Diffeomorph.continuousMul: the self-diffeomorphisms of a compact manifold have jointly continuous multiplication; it is a scoped instance in TauCeti.DiffeomorphWeakWhitney.

@[simp]

theorem Diffeomorph.toContMDiffMap_trans {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] {F : Type u_5} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {G : Type u_6} [TopologicalSpace G] {J : ModelWithCorners 𝕜 F G} {N : Type u_7} [TopologicalSpace N] [ChartedSpace G N] {E' : Type u_8} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {H' : Type u_9} [TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'} {P : Type u_10} [TopologicalSpace P] [ChartedSpace H' P] {n : WithTop ℕ∞} (f : Diffeomorph I J M N n) (g : Diffeomorph J I' N P n) : ↑(f.trans g) = (↑g).comp ↑f

The underlying C^n map of a composite of diffeomorphisms is the composite of the underlying C^n maps.

theorem Diffeomorph.continuous_trans {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] {F : Type u_5} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {G : Type u_6} [TopologicalSpace G] {J : ModelWithCorners 𝕜 F G} {N : Type u_7} [TopologicalSpace N] [ChartedSpace G N] {E' : Type u_8} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {H' : Type u_9} [TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'} {P : Type u_10} [TopologicalSpace P] [ChartedSpace H' P] {n : WithTop ℕ∞} [CompactSpace M] [CompactSpace N] [LocallyCompactSpace E] [LocallyCompactSpace F] [IsManifold I n M] [IsManifold J n N] [IsManifold I' n P] : Continuous fun (p : Diffeomorph I J M N n × Diffeomorph J I' N P n) => p.1.trans p.2

Composition of diffeomorphisms is jointly continuous for the weak Whitney topology.

theorem Diffeomorph.continuousMul {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] {n : WithTop ℕ∞} [CompactSpace M] [LocallyCompactSpace E] [IsManifold I n M] : ContinuousMul (Diffeomorph I I M M n)

Multiplication of self-diffeomorphisms of a compact manifold is jointly continuous for the weak Whitney topology.