Pulling back orientations

Let f : M → M' be a C¹ map between manifolds with corners whose manifold derivative is invertible at every point. An orientation o' of M' pulls back to an orientation of M: the tangent orientation at x is the one carried to o''s tangent orientation at f x by the derivative of f at x. It is the unique orientation of M for which f preserves orientation at every point [Lee, Prop. 15.15].

Local diffeomorphisms of class C^n, n ≠ 0, are the main examples, through IsLocalDiffeomorph.isInvertible_mfderiv. The weaker hypothesis also covers maps that are not local diffeomorphisms at boundary points, such as the inclusion of a closed ball into its ambient space, whose image is not open.

The local constancy of the pulled-back tangent orientations holds for any family of orientations of the tangent spaces of M' along f that is locally constant in trivializations (TauCeti.Manifold.Orientation.eventually_mapOrientation_map_symm_eq), not only for those of an orientation of M'; this is the form needed for orientations defined fibrewise, such as the canonical orientation of an orientation double cover.

Conversely, orientations descend along local diffeomorphisms: a family of orientations of the tangent spaces of M' which is carried, near a, from an orientation of M by the derivative of a local diffeomorphism f at a is locally constant near f a (IsLocalDiffeomorphAt.eventually_mapOrientation_eq). This is the form needed for orientations of spaces glued from oriented pieces, such as the connected sum.

Main definitions

• TauCeti.Manifold.Orientation.pullback: the pullback of an orientation along a C¹ map with everywhere invertible derivative.

Main results

• TauCeti.Manifold.Orientation.isOrientationPreservingAt_pullback: f preserves orientation from the pullback orientation.
• TauCeti.Manifold.Orientation.eq_pullback_iff: the pullback is the only orientation from which f preserves orientation everywhere.
• TauCeti.Manifold.Orientation.eq_neg_pullback_iff: its opposite is the only orientation from which f reverses orientation everywhere.
• TauCeti.Manifold.Orientation.pullback_id, TauCeti.Manifold.Orientation.pullback_comp: functoriality.
• IsLocalDiffeomorphAt.eventually_mapOrientation_eq: tangent orientations carried from an orientation by a local diffeomorphism are locally constant.
• TauCeti.Manifold.Orientation.eventually_isOrientationPreservingAt, TauCeti.Manifold.Orientation.eventually_isOrientationReversingAt: a C¹ map that preserves (reverses) orientation at a point does so at every nearby point.

References

• John M. Lee, Introduction to Smooth Manifolds, second edition, Graduate Texts in Mathematics 218, Springer, 2013, Proposition 15.15.

theorem TauCeti.Manifold.Orientation.eventually_mapOrientation_map_symm_eq {E : Type u_1} {H : Type u_2} {M : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] {I : ModelWithCorners ℝ E H} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I 1 M] {E' : Type u_4} {H' : Type u_5} {M' : Type u_6} [NormedAddCommGroup E'] [NormedSpace ℝ E'] [TopologicalSpace H'] {I' : ModelWithCorners ℝ E' H'} [TopologicalSpace M'] [ChartedSpace H' M'] [IsManifold I' 1 M'] {ι : Type u_10} [Fintype ι] {f : M → M'} {a : M} (hf : ContMDiffAt I I' 1 f a) (D : (x : M) → TangentSpace I x ≃L[ℝ] TangentSpace I' (f x)) (hD : ∀ᶠ (x : M) in nhds a, ↑(D x) = mfderiv% f x) (hι : Fintype.card ι = Module.finrank ℝ E) (ω : (x : M) → _root_.Orientation ℝ (TangentSpace I' (f x)) ι) (hω : ∀ᶠ (x : M) in nhds a, ∀ (hx : f x ∈ (trivializationAt E' (TangentSpace I') (f a)).baseSet), (Bundle.Trivialization.mapOrientation ι (trivializationAt E' (TangentSpace I') (f a)) hx) (ω x) = (Bundle.Trivialization.mapOrientation ι (trivializationAt E' (TangentSpace I') (f a)) ⋯) (ω a)) : ∀ᶠ (x : M) in nhds a, ∀ (hx : x ∈ (trivializationAt E (TangentSpace I) a).baseSet), (Bundle.Trivialization.mapOrientation ι (trivializationAt E (TangentSpace I) a) hx) ((Orientation.map ι ↑(D x).symm) (ω x)) = (Bundle.Trivialization.mapOrientation ι (trivializationAt E (TangentSpace I) a) ⋯) ((Orientation.map ι ↑(D a).symm) (ω a))

Let f be a map that is C¹ at a and whose derivative at each x near a is the equivalence D x, and let ω x be an orientation of the tangent space of M' at f x, locally constant near a when read in the preferred trivialization at f a. Then the orientations of the tangent spaces of M obtained by transporting ω x back along D x are locally constant near a when read in the preferred trivialization at a.

noncomputable def TauCeti.Manifold.Orientation.pullback {E : Type u_1} {H : Type u_2} {M : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] {I : ModelWithCorners ℝ E H} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I 1 M] [FiniteDimensional ℝ E] {E' : Type u_4} {H' : Type u_5} {M' : Type u_6} [NormedAddCommGroup E'] [NormedSpace ℝ E'] [TopologicalSpace H'] {I' : ModelWithCorners ℝ E' H'} [TopologicalSpace M'] [ChartedSpace H' M'] [IsManifold I' 1 M'] [FiniteDimensional ℝ E'] {ι : Type u_10} [Fintype ι] (o' : Orientation I' M' ι) {f : M → M'} (hf : ContMDiff I I' 1 f) (hdf : ∀ (x : M), (mfderiv% f x).IsInvertible) (hι : Fintype.card ι = Module.finrank ℝ E) : Orientation I M ι

The pullback of an orientation o' of M' along a C¹ map f : M → M' whose manifold derivative is invertible at every point: the tangent orientation at x is carried to that of o' at f x by the derivative of f (map_orientationAt_pullback). It is the unique orientation from which f preserves orientation everywhere (eq_pullback_iff). For a C^n local diffeomorphism, n ≠ 0, invertibility of the derivative is IsLocalDiffeomorph.isInvertible_mfderiv.

The hypothesis hι says that ι indexes orientations of the model of M; it follows from the invertibility of the derivative unless M is empty.

theorem TauCeti.Manifold.Orientation.map_orientationAt_pullback {E : Type u_1} {H : Type u_2} {M : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] {I : ModelWithCorners ℝ E H} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I 1 M] [FiniteDimensional ℝ E] {E' : Type u_4} {H' : Type u_5} {M' : Type u_6} [NormedAddCommGroup E'] [NormedSpace ℝ E'] [TopologicalSpace H'] {I' : ModelWithCorners ℝ E' H'} [TopologicalSpace M'] [ChartedSpace H' M'] [IsManifold I' 1 M'] [FiniteDimensional ℝ E'] {ι : Type u_10} [Fintype ι] (o' : Orientation I' M' ι) {f : M → M'} (hf : ContMDiff I I' 1 f) (hdf : ∀ (x : M), (mfderiv% f x).IsInvertible) (hι : Fintype.card ι = Module.finrank ℝ E) (x : M) (D : TangentSpace I x ≃L[ℝ] TangentSpace I' (f x)) (hD : ↑D = mfderiv% f x) : (Orientation.map ι ↑D) ((o'.pullback hf hdf hι).orientationAt x) = o'.orientationAt (f x)

The derivative of f carries the tangent orientations of the pullback orientation to those of the original orientation.

@[simp]

theorem TauCeti.Manifold.Orientation.isOrientationPreservingAt_pullback {E : Type u_1} {H : Type u_2} {M : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] {I : ModelWithCorners ℝ E H} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I 1 M] [FiniteDimensional ℝ E] {E' : Type u_4} {H' : Type u_5} {M' : Type u_6} [NormedAddCommGroup E'] [NormedSpace ℝ E'] [TopologicalSpace H'] {I' : ModelWithCorners ℝ E' H'} [TopologicalSpace M'] [ChartedSpace H' M'] [IsManifold I' 1 M'] [FiniteDimensional ℝ E'] {ι : Type u_10} [Fintype ι] (o' : Orientation I' M' ι) {f : M → M'} (hf : ContMDiff I I' 1 f) (hdf : ∀ (x : M), (mfderiv% f x).IsInvertible) (hι : Fintype.card ι = Module.finrank ℝ E) (x : M) : (o'.pullback hf hdf hι).IsOrientationPreservingAt o' f x

A map preserves orientation at every point from the pullback orientation.

theorem TauCeti.Manifold.Orientation.eq_pullback_iff {E : Type u_1} {H : Type u_2} {M : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] {I : ModelWithCorners ℝ E H} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I 1 M] [FiniteDimensional ℝ E] {E' : Type u_4} {H' : Type u_5} {M' : Type u_6} [NormedAddCommGroup E'] [NormedSpace ℝ E'] [TopologicalSpace H'] {I' : ModelWithCorners ℝ E' H'} [TopologicalSpace M'] [ChartedSpace H' M'] [IsManifold I' 1 M'] [FiniteDimensional ℝ E'] {ι : Type u_10} [Fintype ι] (o' : Orientation I' M' ι) {f : M → M'} (hf : ContMDiff I I' 1 f) (hdf : ∀ (x : M), (mfderiv% f x).IsInvertible) (hι : Fintype.card ι = Module.finrank ℝ E) {o : Orientation I M ι} : o = o'.pullback hf hdf hι ↔ ∀ (x : M), o.IsOrientationPreservingAt o' f x

The pullback orientation is the only orientation from which f preserves orientation at every point.

theorem TauCeti.Manifold.Orientation.eq_neg_pullback_iff {E : Type u_1} {H : Type u_2} {M : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] {I : ModelWithCorners ℝ E H} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I 1 M] [FiniteDimensional ℝ E] {E' : Type u_4} {H' : Type u_5} {M' : Type u_6} [NormedAddCommGroup E'] [NormedSpace ℝ E'] [TopologicalSpace H'] {I' : ModelWithCorners ℝ E' H'} [TopologicalSpace M'] [ChartedSpace H' M'] [IsManifold I' 1 M'] [FiniteDimensional ℝ E'] {ι : Type u_10} [Fintype ι] (o' : Orientation I' M' ι) {f : M → M'} (hf : ContMDiff I I' 1 f) (hdf : ∀ (x : M), (mfderiv% f x).IsInvertible) (hι : Fintype.card ι = Module.finrank ℝ E) {o : Orientation I M ι} : o = -o'.pullback hf hdf hι ↔ ∀ (x : M), o.IsOrientationReversingAt o' f x

The opposite of the pullback orientation is the only orientation from which f reverses orientation at every point.

@[simp]

theorem TauCeti.Manifold.Orientation.pullback_neg {E : Type u_1} {H : Type u_2} {M : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] {I : ModelWithCorners ℝ E H} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I 1 M] [FiniteDimensional ℝ E] {E' : Type u_4} {H' : Type u_5} {M' : Type u_6} [NormedAddCommGroup E'] [NormedSpace ℝ E'] [TopologicalSpace H'] {I' : ModelWithCorners ℝ E' H'} [TopologicalSpace M'] [ChartedSpace H' M'] [IsManifold I' 1 M'] [FiniteDimensional ℝ E'] {ι : Type u_10} [Fintype ι] (o' : Orientation I' M' ι) {f : M → M'} (hf : ContMDiff I I' 1 f) (hdf : ∀ (x : M), (mfderiv% f x).IsInvertible) (hι : Fintype.card ι = Module.finrank ℝ E) : (-o').pullback hf hdf hι = -o'.pullback hf hdf hι

Pulling back the opposite orientation gives the opposite of the pullback orientation.

@[simp]

theorem TauCeti.Manifold.Orientation.pullback_id {E : Type u_1} {H : Type u_2} {M : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] {I : ModelWithCorners ℝ E H} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I 1 M] [FiniteDimensional ℝ E] {ι : Type u_10} [Fintype ι] (o : Orientation I M ι) (hf : ContMDiff I I 1 id) (hdf : ∀ (x : M), (mfderiv% id x).IsInvertible) (hι : Fintype.card ι = Module.finrank ℝ E) : o.pullback hf hdf hι = o

Pulling back along the identity does nothing.

theorem TauCeti.Manifold.Orientation.pullback_comp {E : Type u_1} {H : Type u_2} {M : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] {I : ModelWithCorners ℝ E H} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I 1 M] [FiniteDimensional ℝ E] {E' : Type u_4} {H' : Type u_5} {M' : Type u_6} [NormedAddCommGroup E'] [NormedSpace ℝ E'] [TopologicalSpace H'] {I' : ModelWithCorners ℝ E' H'} [TopologicalSpace M'] [ChartedSpace H' M'] [IsManifold I' 1 M'] [FiniteDimensional ℝ E'] {E'' : Type u_7} {H'' : Type u_8} {M'' : Type u_9} [NormedAddCommGroup E''] [NormedSpace ℝ E''] [TopologicalSpace H''] {I'' : ModelWithCorners ℝ E'' H''} [TopologicalSpace M''] [ChartedSpace H'' M''] [IsManifold I'' 1 M''] [FiniteDimensional ℝ E''] {ι : Type u_10} [Fintype ι] {f : M → M'} (hf : ContMDiff I I' 1 f) (hdf : ∀ (x : M), (mfderiv% f x).IsInvertible) (hι : Fintype.card ι = Module.finrank ℝ E) (o'' : Orientation I'' M'' ι) {g : M' → M''} (hg : ContMDiff I' I'' 1 g) (hdg : ∀ (y : M'), (mfderiv% g y).IsInvertible) (hι' : Fintype.card ι = Module.finrank ℝ E') : (o''.pullback hg hdg hι').pullback hf hdf hι = o''.pullback ⋯ ⋯ hι

Pulling back along a composite is pulling back successively.

theorem IsLocalDiffeomorphAt.eventually_mapOrientation_eq {E : Type u_1} {H : Type u_2} {M : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] {I : ModelWithCorners ℝ E H} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I 1 M] [FiniteDimensional ℝ E] {E' : Type u_4} {H' : Type u_5} {M' : Type u_6} [NormedAddCommGroup E'] [NormedSpace ℝ E'] [TopologicalSpace H'] {I' : ModelWithCorners ℝ E' H'} [TopologicalSpace M'] [ChartedSpace H' M'] [IsManifold I' 1 M'] {ι : Type u_10} [Fintype ι] {n : WithTop ℕ∞} [NeZero n] {f : M → M'} {a : M} (hf : IsLocalDiffeomorphAt I I' n f a) (o : TauCeti.Manifold.Orientation I M ι) (ω : (y : M') → Orientation ℝ (TangentSpace I' y) ι) (hω : ∀ᶠ (x : M) in nhds a, ∃ (D : TangentSpace I x ≃L[ℝ] TangentSpace I' (f x)), ↑D = mfderiv% f x ∧ (Orientation.map ι ↑D) (o.orientationAt x) = ω (f x)) : ∀ᶠ (y : M') in nhds (f a), ∀ (hy : y ∈ (trivializationAt E' (TangentSpace I') (f a)).baseSet), (Bundle.Trivialization.mapOrientation ι (trivializationAt E' (TangentSpace I') (f a)) hy) (ω y) = (Bundle.Trivialization.mapOrientation ι (trivializationAt E' (TangentSpace I') (f a)) ⋯) (ω (f a))

Orientations descend along local diffeomorphisms. Let f : M → M' be a C^n local diffeomorphism at a, n ≠ 0, and let ω y be an orientation of the tangent space of M' at each y. If near a the derivative of f carries the tangent orientations of an orientation o of M to ω, then ω is locally constant near f a when read in the preferred trivialization at f a.

theorem TauCeti.Manifold.Orientation.eventually_isOrientationPreservingAt {E : Type u_1} {H : Type u_2} {M : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] {I : ModelWithCorners ℝ E H} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I 1 M] [FiniteDimensional ℝ E] {E' : Type u_4} {H' : Type u_5} {M' : Type u_6} [NormedAddCommGroup E'] [NormedSpace ℝ E'] [TopologicalSpace H'] {I' : ModelWithCorners ℝ E' H'} [TopologicalSpace M'] [ChartedSpace H' M'] [IsManifold I' 1 M'] [FiniteDimensional ℝ E'] {ι : Type u_10} [Fintype ι] {f : M → M'} {a : M} (hf : ContMDiffAt I I' 1 f a) {o : Orientation I M ι} {o' : Orientation I' M' ι} (ho : o.IsOrientationPreservingAt o' f a) : ∀ᶠ (x : M) in nhds a, o.IsOrientationPreservingAt o' f x

Orientation preservation is an open condition. If a map f that is C¹ at a preserves the orientations o and o' at a, then it preserves them at every point near a.

theorem TauCeti.Manifold.Orientation.eventually_isOrientationReversingAt {E : Type u_1} {H : Type u_2} {M : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] {I : ModelWithCorners ℝ E H} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I 1 M] [FiniteDimensional ℝ E] {E' : Type u_4} {H' : Type u_5} {M' : Type u_6} [NormedAddCommGroup E'] [NormedSpace ℝ E'] [TopologicalSpace H'] {I' : ModelWithCorners ℝ E' H'} [TopologicalSpace M'] [ChartedSpace H' M'] [IsManifold I' 1 M'] [FiniteDimensional ℝ E'] {ι : Type u_10} [Fintype ι] {f : M → M'} {a : M} (hf : ContMDiffAt I I' 1 f a) {o : Orientation I M ι} {o' : Orientation I' M' ι} (ho : o.IsOrientationReversingAt o' f a) : ∀ᶠ (x : M) in nhds a, o.IsOrientationReversingAt o' f x

Orientation reversal is an open condition. If a map f that is C¹ at a reverses the orientations o and o' at a, then it reverses them at every point near a.