Restricting an orientation to an open subset

An open subset U of a manifold M, charted by the restrictions of the charts of M, includes into M by a local diffeomorphism (TauCeti.isLocalDiffeomorph_subtype_val). So every orientation of M pulls back to an orientation of U (TauCeti.Manifold.Orientation.restrict), the unique one for which the inclusion preserves orientation.

Main definitions

• TauCeti.Manifold.Orientation.restrict: the restriction of an orientation to an open subset.

Main results

• TauCeti.Manifold.Orientation.isOrientationPreservingAt_restrict: the inclusion of the open subset preserves orientation from the restriction.
• TauCeti.Manifold.Orientation.isOrientationPreservingAt_restrict_inclusion: for open subsets U ≤ W, the inclusion of U into W preserves the restricted orientations.
• TauCeti.Manifold.Orientation.eq_restrict_iff: this property characterizes the restriction.
• TauCeti.Manifold.Orientation.restrict_neg: restriction commutes with taking the opposite orientation.

noncomputable def TauCeti.Manifold.Orientation.restrict {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] [IsManifold I 1 M] {ι : Type u_4} [Fintype ι] (o : Orientation I M ι) (U : TopologicalSpace.Opens M) : Orientation I (↥U) ι

The restriction of an orientation of M to the open subset U: its pullback along the inclusion U → M.

@[simp]

theorem TauCeti.Manifold.Orientation.isOrientationPreservingAt_restrict {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] [IsManifold I 1 M] {ι : Type u_4} [Fintype ι] (o : Orientation I M ι) (U : TopologicalSpace.Opens M) (x : ↥U) : (o.restrict U).IsOrientationPreservingAt o Subtype.val x

The inclusion of an open subset preserves orientation from the restricted orientation.

@[simp]

theorem TauCeti.Manifold.Orientation.isOrientationPreservingAt_restrict_inclusion {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] [IsManifold I 1 M] {ι : Type u_4} [Fintype ι] (o : Orientation I M ι) {U W : TopologicalSpace.Opens M} (h : U ≤ W) (x : ↥U) : (o.restrict U).IsOrientationPreservingAt (o.restrict W) (TopologicalSpace.Opens.inclusion h) x

For open subsets U ≤ W, the inclusion of U into W preserves the orientations restricted from M.

@[simp]

theorem TauCeti.Manifold.Orientation.restrict_neg {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] [IsManifold I 1 M] {ι : Type u_4} [Fintype ι] (o : Orientation I M ι) (U : TopologicalSpace.Opens M) : (-o).restrict U = -o.restrict U

Restricting the opposite orientation gives the opposite of the restriction.

theorem TauCeti.Manifold.Orientation.eq_restrict_iff {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] [IsManifold I 1 M] {ι : Type u_4} [Fintype ι] {o : Orientation I M ι} {U : TopologicalSpace.Opens M} {o' : Orientation I (↥U) ι} : o' = o.restrict U ↔ ∀ (x : ↥U), o'.IsOrientationPreservingAt o Subtype.val x

The restriction is the only orientation of U from which the inclusion into M preserves orientation at every point.