Diffeotopies preserve orientation #
Every time slice of a diffeotopy preserves every orientation of its ambient manifold. In particular the final diffeomorphism does. This lets a diffeotopy move the centre of an oriented embedded disc while retaining its orientation, before applying the disc theorem at a common centre. The manifold may have boundary or corners and need not be connected.
The result uses local constancy of orientation behavior in a C¹ family with invertible
slice derivatives, and the identity slice at time zero.
References #
- M. W. Hirsch, Differential Topology, Chapter 4, §6 (the disc theorem).
@[simp]
theorem
TauCeti.Diffeotopy.isOrientationPreservingAt_timeSlice
{E : Type u_1}
{H : Type u_2}
{M : Type u_3}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[FiniteDimensional ℝ E]
[TopologicalSpace H]
{I : ModelWithCorners ℝ E H}
[TopologicalSpace M]
[ChartedSpace H M]
{n : WithTop ℕ∞}
[IsManifold I n M]
{ι : Type u_4}
[Fintype ι]
(Φ : Diffeotopy I n M)
(hn : 1 ≤ n)
(o : Manifold.Orientation I M ι)
(t : ↑unitInterval)
(x : M)
:
have this := ⋯;
o.IsOrientationPreservingAt o (⇑(Φ.timeSlice t)) x
Every time slice of a positive-order diffeotopy preserves every ambient orientation, including on a disconnected manifold or a manifold with corners.
@[simp]
theorem
TauCeti.Diffeotopy.isOrientationPreservingAt_final
{E : Type u_1}
{H : Type u_2}
{M : Type u_3}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[FiniteDimensional ℝ E]
[TopologicalSpace H]
{I : ModelWithCorners ℝ E H}
[TopologicalSpace M]
[ChartedSpace H M]
{n : WithTop ℕ∞}
[IsManifold I n M]
{ι : Type u_4}
[Fintype ι]
(Φ : Diffeotopy I n M)
(hn : 1 ≤ n)
(o : Manifold.Orientation I M ι)
(x : M)
:
have this := ⋯;
o.IsOrientationPreservingAt o (⇑Φ.final) x
The final diffeomorphism of a positive-order diffeotopy preserves every ambient orientation.