Orientation behavior in smooth families

In a jointly C¹ family of maps between oriented manifolds, if every slice has an invertible derivative at a fixed source point, its orientation behavior there is locally constant in the parameter. On a preconnected parameter manifold it is therefore independent of the parameter. No compactness, global injectivity, or boundarylessness is required.

This is the orientation step in moving embedded discs by a diffeotopy: a motion starting at the identity preserves orientation throughout, so moving the centre does not change the orientation class of the disc.

The coordinate argument follows the relative-determinant method of TauCeti.Manifold.Orientation.eventually_mapOrientation_map_symm_eq in the pullback-orientation construction, applied to the derivatives of the slices of a family.

References

• M. W. Hirsch, Differential Topology, Chapter 4, §6 (the disc theorem).
• J. M. Lee, Introduction to Smooth Manifolds, second edition, Chapter 15 (orientations).

theorem TauCeti.Manifold.Orientation.isLocallyConstant_isOrientationPreservingAt {E : Type u_1} {H : Type u_2} {M : Type u_3} {E' : Type u_4} {H' : Type u_5} {N : Type u_6} {V : Type u_7} {G : Type u_8} {P : Type u_9} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] [NormedAddCommGroup E'] [NormedSpace ℝ E'] [FiniteDimensional ℝ E'] [NormedAddCommGroup V] [NormedSpace ℝ V] [TopologicalSpace H] [TopologicalSpace H'] [TopologicalSpace G] {I : ModelWithCorners ℝ E H} {J : ModelWithCorners ℝ E' H'} {L : ModelWithCorners ℝ V G} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I 1 M] [TopologicalSpace N] [ChartedSpace H' N] [IsManifold J 1 N] [TopologicalSpace P] [ChartedSpace G P] [IsManifold L 1 P] {ι : Type u_10} [Fintype ι] (o : Orientation I M ι) (o' : Orientation J N ι) {F : P × M → N} (hF : ContMDiff (L.prod I) J 1 F) (x : M) (hD : ∀ (p : P), ((mfderiv% fun (y : M) => F (p, y)) x).IsInvertible) : IsLocallyConstant fun (p : P) => o.IsOrientationPreservingAt o' (fun (y : M) => F (p, y)) x

The orientation behavior of a jointly C¹ family is locally constant in the parameter, provided the derivatives of all slices are invertible at the chosen source point.

theorem TauCeti.Manifold.Orientation.isOrientationPreservingAt_family_iff {E : Type u_1} {H : Type u_2} {M : Type u_3} {E' : Type u_4} {H' : Type u_5} {N : Type u_6} {V : Type u_7} {G : Type u_8} {P : Type u_9} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] [NormedAddCommGroup E'] [NormedSpace ℝ E'] [FiniteDimensional ℝ E'] [NormedAddCommGroup V] [NormedSpace ℝ V] [TopologicalSpace H] [TopologicalSpace H'] [TopologicalSpace G] {I : ModelWithCorners ℝ E H} {J : ModelWithCorners ℝ E' H'} {L : ModelWithCorners ℝ V G} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I 1 M] [TopologicalSpace N] [ChartedSpace H' N] [IsManifold J 1 N] [TopologicalSpace P] [ChartedSpace G P] [IsManifold L 1 P] {ι : Type u_10} [Fintype ι] [PreconnectedSpace P] (o : Orientation I M ι) (o' : Orientation J N ι) {F : P × M → N} (hF : ContMDiff (L.prod I) J 1 F) (x : M) (hD : ∀ (p : P), ((mfderiv% fun (y : M) => F (p, y)) x).IsInvertible) (p q : P) : o.IsOrientationPreservingAt o' (fun (y : M) => F (p, y)) x ↔ o.IsOrientationPreservingAt o' (fun (y : M) => F (q, y)) x

In a preconnected smooth family with invertible slice derivatives at x, one slice preserves orientation at x exactly when every other slice does.