Orientation-preserving coordinate changes and oriented atlases

Within-range transition derivatives define the orientation-preserving groupoid and oriented subatlases, including at boundary and corner points. An oriented atlas supplies an orientation; the interval is orientable although its half-line charts have opposite transition signs.

Main declarations

• orientationPreservingGroupoid and IsOrientedAtlas: positive transitions and oriented atlases.
• isOrientedAtlas_atlas: an atlas with orientation-preserving coordinate changes is oriented.
• IsOrientedAtlas.det_fderivWithin_pos and IsOrientedAtlas.prod: determinants and products.
• not_contDiffGroupoid_le_orientationPreservingGroupoid: smooth changes can reverse orientation.

References

• J. M. Lee, Introduction to Smooth Manifolds, 2nd edition, Chapter 15.

def TauCeti.OrientationPreservingOn {E : Type u_1} {H : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] (I : ModelWithCorners ℝ E H) [FiniteDimensional ℝ E] (f : H → H) (s : Set H) : Prop

A map f : H → H preserves orientation on s, read in the model through I: at the image I x of each point x ∈ s, the coordinate expression I ∘ f ∘ I.symm is differentiable within range I, with derivative of positive determinant. The model vector space E is finite-dimensional, as determinants are only meaningful there; the determinant is that of the matrix of the derivative in the basis Module.finBasis ℝ E, which is LinearMap.det of the derivative (TauCeti.orientationPreservingOn_iff).

theorem TauCeti.orientationPreservingOn_iff {E : Type u_1} {H : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] {I : ModelWithCorners ℝ E H} [FiniteDimensional ℝ E] {f : H → H} {s : Set H} : OrientationPreservingOn I f s ↔ ∀ x ∈ s, DifferentiableWithinAt ℝ (↑I ∘ f ∘ ↑I.symm) (Set.range ↑I) (↑I x) ∧ 0 < LinearMap.det ↑(fderivWithin ℝ (↑I ∘ f ∘ ↑I.symm) (Set.range ↑I) (↑I x))

Unfold TauCeti.OrientationPreservingOn, with the determinant of the derivative stated basis-free as LinearMap.det.

theorem TauCeti.OrientationPreservingOn.mono {E : Type u_1} {H : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] {I : ModelWithCorners ℝ E H} [FiniteDimensional ℝ E] {f : H → H} {s t : Set H} (h : OrientationPreservingOn I f t) (hst : s ⊆ t) : OrientationPreservingOn I f s

Orientation preservation on a set is inherited by its subsets.

theorem TauCeti.orientationPreservingOn_id {E : Type u_1} {H : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] {I : ModelWithCorners ℝ E H} [FiniteDimensional ℝ E] (s : Set H) : OrientationPreservingOn I id s

The identity preserves orientation on every set.

theorem TauCeti.OrientationPreservingOn.comp {E : Type u_1} {H : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] {I : ModelWithCorners ℝ E H} [FiniteDimensional ℝ E] {f g : H → H} {s t : Set H} (hg : OrientationPreservingOn I g t) (hf : OrientationPreservingOn I f s) (hst : Set.MapsTo f s t) : OrientationPreservingOn I (g ∘ f) s

A composite of orientation-preserving maps preserves orientation.

theorem TauCeti.OrientationPreservingOn.congr {E : Type u_1} {H : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] {I : ModelWithCorners ℝ E H} [FiniteDimensional ℝ E] {f g : H → H} {s : Set H} (hs : IsOpen s) (h : OrientationPreservingOn I f s) (hfg : Set.EqOn g f s) : OrientationPreservingOn I g s

On an open set, orientation preservation only depends on the values of the map there.

def TauCeti.orientationPreservingPregroupoid {E : Type u_1} {H : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] (I : ModelWithCorners ℝ E H) [FiniteDimensional ℝ E] : Pregroupoid H

Given a model with corners (E, H), the pregroupoid of orientation-preserving maps of H: those whose coordinate expression in E has derivative of positive determinant.

def TauCeti.orientationPreservingGroupoid {E : Type u_1} {H : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] (I : ModelWithCorners ℝ E H) [FiniteDimensional ℝ E] : StructureGroupoid H

Given a model with corners (E, H), the groupoid of orientation-preserving open partial homeomorphisms of H: both the map and its inverse have derivatives of positive determinant when read in E through I.

theorem TauCeti.mem_orientationPreservingGroupoid_iff {E : Type u_1} {H : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] {I : ModelWithCorners ℝ E H} [FiniteDimensional ℝ E] {e : OpenPartialHomeomorph H H} : e ∈ orientationPreservingGroupoid I ↔ OrientationPreservingOn I (↑e) e.source ∧ OrientationPreservingOn I (↑e.symm) e.target

Membership in TauCeti.orientationPreservingGroupoid, unfolded: the map preserves orientation on its source and its inverse preserves orientation on its target.

theorem TauCeti.ofSet_mem_orientationPreservingGroupoid {E : Type u_1} {H : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] {I : ModelWithCorners ℝ E H} [FiniteDimensional ℝ E] {s : Set H} (hs : IsOpen s) : OpenPartialHomeomorph.ofSet s hs ∈ orientationPreservingGroupoid I

The identity of an open set belongs to the orientation-preserving groupoid.

instance TauCeti.instClosedUnderRestrictionOrientationPreservingGroupoid {E : Type u_1} {H : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] {I : ModelWithCorners ℝ E H} [FiniteDimensional ℝ E] : ClosedUnderRestriction (orientationPreservingGroupoid I)

The orientation-preserving groupoid is closed under restriction to open subsets.

theorem TauCeti.OrientationPreservingOn.prodMap {E : Type u_1} {H : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] {I : ModelWithCorners ℝ E H} [FiniteDimensional ℝ E] {E' : Type u_3} {H' : Type u_4} [NormedAddCommGroup E'] [NormedSpace ℝ E'] [TopologicalSpace H'] [FiniteDimensional ℝ E'] {I' : ModelWithCorners ℝ E' H'} {f : H → H} {f' : H' → H'} {s : Set H} {s' : Set H'} (hf : OrientationPreservingOn I f s) (hf' : OrientationPreservingOn I' f' s') : OrientationPreservingOn (I.prod I') (Prod.map f f') (s ×ˢ s')

A product of orientation-preserving maps preserves orientation in the product model: the derivative of the product is block diagonal, so its determinant is the product of the two.

theorem TauCeti.orientationPreservingGroupoid_prod {E : Type u_1} {H : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] {I : ModelWithCorners ℝ E H} [FiniteDimensional ℝ E] {E' : Type u_3} {H' : Type u_4} [NormedAddCommGroup E'] [NormedSpace ℝ E'] [TopologicalSpace H'] [FiniteDimensional ℝ E'] {I' : ModelWithCorners ℝ E' H'} {e : OpenPartialHomeomorph H H} {e' : OpenPartialHomeomorph H' H'} (he : e ∈ orientationPreservingGroupoid I) (he' : e' ∈ orientationPreservingGroupoid I') : e.prod e' ∈ orientationPreservingGroupoid (I.prod I')

The product of two orientation-preserving open partial homeomorphisms preserves orientation in the product model.

Linear coordinate changes

On the model vector space itself, a linear automorphism preserves orientation exactly when its determinant is positive. In particular the reflection of ℝ is a smooth coordinate change that reverses orientation, so some smooth coordinate changes are excluded from the orientation-preserving groupoid and an oriented atlas is a genuine constraint.

theorem ContinuousLinearMap.orientationPreservingOn_iff {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] (A : E →L[ℝ] E) {s : Set E} : TauCeti.OrientationPreservingOn (modelWithCornersSelf ℝ E) (⇑A) s ↔ s = ∅ ∨ 0 < LinearMap.det ↑A

A continuous linear map of the model vector space preserves orientation on a set exactly when the set is empty or the determinant of the map is positive.

theorem ContinuousLinearEquiv.toHomeomorph_toOpenPartialHomeomorph_mem_orientationPreservingGroupoid_iff {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] (A : E ≃L[ℝ] E) : A.toHomeomorph.toOpenPartialHomeomorph ∈ TauCeti.orientationPreservingGroupoid (modelWithCornersSelf ℝ E) ↔ 0 < LinearMap.det ↑↑A

A linear automorphism of the model vector space, viewed as a coordinate change, belongs to the orientation-preserving groupoid exactly when its determinant is positive.

theorem TauCeti.not_contDiffGroupoid_le_orientationPreservingGroupoid (n : WithTop ℕ∞) : ¬contDiffGroupoid n (modelWithCornersSelf ℝ ℝ) ≤ orientationPreservingGroupoid (modelWithCornersSelf ℝ ℝ)

The reflection x ↦ -x of ℝ is a smooth coordinate change that reverses orientation: the C^n groupoid of ℝ is not contained in the orientation-preserving groupoid.

Oriented atlases

structure TauCeti.IsOrientedAtlas {E : Type u_1} {H : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] [TopologicalSpace H] (I : ModelWithCorners ℝ E H) (n : WithTop ℕ∞) {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] [NeZero n] (A : Set (OpenPartialHomeomorph M H)) : Prop

An oriented atlas of the C^n manifold M, for n ≠ 0: a family of charts from its maximal C^n atlas which covers M and whose coordinate changes all preserve orientation.

• subset_maximalAtlas : A ⊆ IsManifold.maximalAtlas I n M

  Every chart of an oriented atlas is compatible with the C^n structure of M.

• exists_mem_source (x : M) : ∃ e ∈ A, x ∈ e.source

  The charts of an oriented atlas cover M.

• symm_trans_mem {e e' : OpenPartialHomeomorph M H} : e ∈ A → e' ∈ A → e.symm.trans e' ∈ orientationPreservingGroupoid I

  The coordinate changes of an oriented atlas preserve orientation.

theorem TauCeti.isOrientedAtlas_atlas {E : Type u_1} {H : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] [TopologicalSpace H] (I : ModelWithCorners ℝ E H) (n : WithTop ℕ∞) [NeZero n] (M : Type u_3) [TopologicalSpace M] [ChartedSpace H M] [IsManifold I n M] [HasGroupoid M (orientationPreservingGroupoid I)] : IsOrientedAtlas I n (atlas H M)

The atlas of a manifold whose coordinate changes all preserve orientation is an oriented atlas.

theorem TauCeti.IsOrientedAtlas.det_fderivWithin_pos {E : Type u_1} {H : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {n : WithTop ℕ∞} [NeZero n] {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] {A : Set (OpenPartialHomeomorph M H)} (hA : IsOrientedAtlas I n A) {e e' : OpenPartialHomeomorph M H} (he : e ∈ A) (he' : e' ∈ A) {x : M} (hx : x ∈ e.source) (hx' : x ∈ e'.source) : 0 < LinearMap.det ↑(fderivWithin ℝ (↑(e'.extend I) ∘ ↑(e.extend I).symm) (Set.range ↑I) (↑(e.extend I) x))

Two charts of an oriented atlas change coordinates with derivative of positive determinant at every point of their common domain.

theorem TauCeti.IsOrientedAtlas.prod {E : Type u_1} {H : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {n : WithTop ℕ∞} [NeZero n] {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] {E' : Type u_4} {H' : Type u_5} [NormedAddCommGroup E'] [NormedSpace ℝ E'] [TopologicalSpace H'] [FiniteDimensional ℝ E'] {I' : ModelWithCorners ℝ E' H'} {M' : Type u_6} [TopologicalSpace M'] [ChartedSpace H' M'] [IsManifold I n M] [IsManifold I' n M'] {A : Set (OpenPartialHomeomorph M H)} {A' : Set (OpenPartialHomeomorph M' H')} (hA : IsOrientedAtlas I n A) (hA' : IsOrientedAtlas I' n A') : IsOrientedAtlas (I.prod I') n (Set.image2 OpenPartialHomeomorph.prod A A')

The products of the charts of two oriented atlases form an oriented atlas of the product.