The path traced by a diffeotopy

A diffeotopy of M is a C^n motion through self-diffeomorphisms, so its time slices are a jointly C^n family of diffeomorphisms; Diffeomorph.ofSmoothFamily therefore makes them a continuous curve in TauCeti.Diff for the weak Whitney topology. Since a diffeotopy starts at the identity, that curve is a path from 1 to the final diffeomorphism: a self-diffeomorphism diffeotopic to the identity lies in the path component of 1.

This application is kept apart from TauCeti.Geometry.Diffeomorphism.Topology so that the topology itself does not drag in diffeotopy theory and the real-manifold structure of the unit interval.

Main definitions

• TauCeti.Diffeotopy.toPath: the path traced in TauCeti.Diff by a diffeotopy.

Main results

• TauCeti.Diffeotopy.continuous_timeSlice: the time slices of a diffeotopy move continuously.
• TauCeti.Diffeotopy.joined_one_final: the identity is joined to the final diffeomorphism.

References

• M. Hirsch, Differential Topology, Springer GTM 33 (1976), Chapter 8, §8.1, for smooth isotopies and diffeotopies.

theorem TauCeti.Diffeotopy.continuous_timeSlice {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_2} [TopologicalSpace H] {J : ModelWithCorners ℝ E H} {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] {n : WithTop ℕ∞} (Φ : Diffeotopy J n M) [CompactSpace M] [IsManifold J n M] : Continuous Φ.timeSlice

The time slices of a diffeotopy move continuously in the weak Whitney topology.

noncomputable def TauCeti.Diffeotopy.toPath {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_2} [TopologicalSpace H] {J : ModelWithCorners ℝ E H} {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] {n : WithTop ℕ∞} (Φ : Diffeotopy J n M) [CompactSpace M] [IsManifold J n M] : Path 1 Φ.final

A diffeotopy is a path in TauCeti.Diff from the identity to its final diffeomorphism; in particular a self-diffeomorphism diffeotopic to the identity lies in the path component of 1.

Equations

• Φ.toPath = { toFun := Φ.timeSlice, continuous_toFun := ⋯, source' := ⋯, target' := ⋯ }

@[simp]

theorem TauCeti.Diffeotopy.toPath_apply {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_2} [TopologicalSpace H] {J : ModelWithCorners ℝ E H} {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] {n : WithTop ℕ∞} (Φ : Diffeotopy J n M) [CompactSpace M] [IsManifold J n M] (t : ↑unitInterval) : Φ.toPath t = Φ.timeSlice t

The path traced by a diffeotopy is its family of time slices.

theorem TauCeti.Diffeotopy.joined_one_final {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_2} [TopologicalSpace H] {J : ModelWithCorners ℝ E H} {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] {n : WithTop ℕ∞} (Φ : Diffeotopy J n M) [CompactSpace M] [IsManifold J n M] : Joined 1 Φ.final

The identity diffeomorphism is joined to the final diffeomorphism of a diffeotopy.