Orientation behavior of manifold maps #
This file records the pointwise interface for a map to preserve or reverse manifold orientations.
The differential is required to be represented by a continuous linear equivalence, and its induced
orientation must agree with the target orientation (or its opposite). These predicates are the local
input for pullback orientations and orientation-sensitive integration. A local diffeomorphism at a
point either preserves or reverses orientations there
(IsLocalDiffeomorphAt.isOrientationPreservingAt_or_isOrientationReversingAt).
The inverse of a diffeomorphism preserves orientation wherever the diffeomorphism does
(IsOrientationPreservingAt.diffeomorph_symm), so a diffeomorphism of M preserving an
orientation everywhere has all its integer powers orientation preserving
(isOrientationPreservingAt_zpow).
For orientation lifts whose model orientations correspond under a linear equivalence of the model spaces, the chart signs of the lifts compensate the sign of the coordinate Jacobian of an orientation-preserving map, read in the source model through that equivalence.
For one-dimensional manifolds modelled on ℝ whose orientations are the standard orientation of
ℝ at the relevant points, isOrientationPreservingAt_of_orientationAt_eq and
isOrientationReversingAt_of_orientationAt_eq reduce preservation and reversal to the sign of the
real number by which the derivative multiplies. In particular, translations of ℝ preserve its
standard orientation (isOrientationPreservingAt_add_const).
On the model space E itself, every orientation is constant once the tangent spaces are identified
with E (orientationAt_eq_orientationAt), so a continuous linear automorphism of E preserves
or reverses every orientation of E according to the sign of its determinant
(isOrientationPreservingAt_of_det_pos, isOrientationReversingAt_of_det_neg). In particular
precomposing with an automorphism of negative determinant exchanges preservation and reversal
(isOrientationPreservingAt_comp_of_det_neg, isOrientationReversingAt_comp_of_det_neg).
More generally, a map with negative derivative determinant reverses orientations at that point
(isOrientationReversingAt_of_det_fderiv_neg).
If the derivative carries a tangent basis b onto a basis b', then, whether b is positively
or negatively oriented, preservation (reversal) means that b and b' have equal (opposite)
orientation signs (isOrientationPreservingAt_iff_of_basis,
isOrientationReversingAt_iff_of_basis).
def
TauCeti.Manifold.Orientation.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]
[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']
[FiniteDimensional ℝ E']
{ι : Type u_10}
[Fintype ι]
[IsManifold I 1 M]
[IsManifold I' 1 M']
(o : Orientation I M ι)
(o' : Orientation I' M' ι)
(f : M → M')
(x : M)
:
A map preserves orientations at x when its manifold derivative is an equivalence that maps
o's tangent orientation at x to o''s tangent orientation at f x.
Instances For
theorem
TauCeti.Manifold.Orientation.isOrientationPreservingAt_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]
[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']
[FiniteDimensional ℝ E']
{ι : Type u_10}
[Fintype ι]
[IsManifold I 1 M]
[IsManifold I' 1 M']
(o : Orientation I M ι)
(o' : Orientation I' M' ι)
(f : M → M')
(x : M)
:
o.IsOrientationPreservingAt o' f x ↔ ∃ (e : TangentSpace I x ≃L[ℝ] TangentSpace I' (f x)),
↑e = mfderiv% f x ∧ (Orientation.map ι ↑e) (o.orientationAt x) = o'.orientationAt (f x)
Unfold IsOrientationPreservingAt into its derivative witness and orientation equation.
def
TauCeti.Manifold.Orientation.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]
[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']
[FiniteDimensional ℝ E']
{ι : Type u_10}
[Fintype ι]
[IsManifold I 1 M]
[IsManifold I' 1 M']
(o : Orientation I M ι)
(o' : Orientation I' M' ι)
(f : M → M')
(x : M)
:
A map reverses orientations at x when its manifold derivative is an equivalence that maps
o's tangent orientation at x to the opposite of o''s tangent orientation at f x.
Instances For
theorem
TauCeti.Manifold.Orientation.isOrientationReversingAt_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]
[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']
[FiniteDimensional ℝ E']
{ι : Type u_10}
[Fintype ι]
[IsManifold I 1 M]
[IsManifold I' 1 M']
(o : Orientation I M ι)
(o' : Orientation I' M' ι)
(f : M → M')
(x : M)
:
o.IsOrientationReversingAt o' f x ↔ ∃ (e : TangentSpace I x ≃L[ℝ] TangentSpace I' (f x)),
↑e = mfderiv% f x ∧ (Orientation.map ι ↑e) (o.orientationAt x) = -o'.orientationAt (f x)
Unfold IsOrientationReversingAt into its derivative witness and orientation equation.
theorem
TauCeti.Manifold.Orientation.isOrientationPreservingAt_iff_of_coe_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]
[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']
[FiniteDimensional ℝ E']
{ι : Type u_10}
[Fintype ι]
[IsManifold I 1 M]
[IsManifold I' 1 M']
(o : Orientation I M ι)
(o' : Orientation I' M' ι)
(f : M → M')
(x : M)
(e : TangentSpace I x ≃L[ℝ] TangentSpace I' (f x))
(he : ↑e = mfderiv% f x)
:
o.IsOrientationPreservingAt o' f x ↔ (Orientation.map ι ↑e) (o.orientationAt x) = o'.orientationAt (f x)
Given a continuous linear equivalence representing the derivative, preservation is exactly its orientation equation.
theorem
TauCeti.Manifold.Orientation.isOrientationReversingAt_iff_of_coe_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]
[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']
[FiniteDimensional ℝ E']
{ι : Type u_10}
[Fintype ι]
[IsManifold I 1 M]
[IsManifold I' 1 M']
(o : Orientation I M ι)
(o' : Orientation I' M' ι)
(f : M → M')
(x : M)
(e : TangentSpace I x ≃L[ℝ] TangentSpace I' (f x))
(he : ↑e = mfderiv% f x)
:
o.IsOrientationReversingAt o' f x ↔ (Orientation.map ι ↑e) (o.orientationAt x) = -o'.orientationAt (f x)
Given a continuous linear equivalence representing the derivative, reversal is exactly its orientation equation with the opposite target orientation.
theorem
TauCeti.Manifold.Orientation.isOrientationPreservingAt_iff_map_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]
[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']
[FiniteDimensional ℝ E']
{ι : Type u_10}
[Fintype ι]
[IsManifold I 1 M]
[IsManifold I' 1 M']
(o : Orientation I M ι)
(o' : Orientation I' M' ι)
(g : M → M')
(x : M)
(b : M')
(D : TangentSpace I x ≃L[ℝ] TangentSpace I' (g x))
(hDc : ↑D = mfderiv% g x)
(hx : x ∈ (trivializationAt E (TangentSpace I) x).baseSet)
(hp : g x ∈ (trivializationAt E' (TangentSpace I') b).baseSet)
:
o.IsOrientationPreservingAt o' g x ↔ (Orientation.map ι
↑(((Bundle.Trivialization.continuousLinearEquivAt ℝ (trivializationAt E (TangentSpace I) x) x hx).symm.trans
D).trans
(Bundle.Trivialization.continuousLinearEquivAt ℝ (trivializationAt E' (TangentSpace I') b) (g x) hp)))
((Bundle.Trivialization.mapOrientation ι (trivializationAt E (TangentSpace I) x) hx) (o.orientationAt x)) = (Bundle.Trivialization.mapOrientation ι (trivializationAt E' (TangentSpace I') b) hp) (o'.orientationAt (g x))
Orientation preservation of a map with invertible derivative at x, read in the tangent
trivializations at x and b: the continuous equivalence T induced by the derivative D
carries the orientation of x to that of g x exactly when g preserves orientation at x.
theorem
TauCeti.Manifold.Orientation.isOrientationPreservingAt_iff_of_basis
{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]
[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']
[FiniteDimensional ℝ E']
{ι : Type u_10}
[Fintype ι]
[IsManifold I 1 M]
[IsManifold I' 1 M']
[DecidableEq ι]
{o : Orientation I M ι}
{o' : Orientation I' M' ι}
{f : M → M'}
{x : M}
(b : Module.Basis ι ℝ (TangentSpace I x))
(b' : Module.Basis ι ℝ (TangentSpace I' (f x)))
(hbb' : ∀ (i : ι), (mfderiv% f x) (b i) = b' i)
:
o.IsOrientationPreservingAt o' f x ↔ (b.orientation = o.orientationAt x ↔ b'.orientation = o'.orientationAt (f x))
If the derivative at x carries a basis b of the tangent space at x to the basis b' of
the tangent space at f x, then f preserves orientations at x exactly when b and b' are
both positively or both negatively oriented.
theorem
TauCeti.Manifold.Orientation.isOrientationPreservingAt_or_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]
[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']
[FiniteDimensional ℝ E']
{ι : Type u_10}
[Fintype ι]
[IsManifold I 1 M]
[IsManifold I' 1 M']
(o : Orientation I M ι)
(o' : Orientation I' M' ι)
(f : M → M')
(x : M)
(e : TangentSpace I x ≃L[ℝ] TangentSpace I' (f x))
(he : ↑e = mfderiv% f x)
:
Given a continuous linear equivalence representing the derivative, every map is either orientation-preserving or orientation-reversing at the point.
theorem
IsLocalDiffeomorphAt.isOrientationPreservingAt_or_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]
[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']
[FiniteDimensional ℝ E']
{ι : Type u_10}
[Fintype ι]
[IsManifold I 1 M]
[IsManifold I' 1 M']
{n : WithTop ℕ∞}
{f : M → M'}
{x : M}
(hf : IsLocalDiffeomorphAt I I' n f x)
(hn : n ≠ 0)
(o : TauCeti.Manifold.Orientation I M ι)
(o' : TauCeti.Manifold.Orientation I' M' ι)
:
A C^n local diffeomorphism at x, for n ≠ 0, either preserves or reverses orientations at
x.
theorem
TauCeti.Manifold.Orientation.IsOrientationPreservingAt.isInvertible_mfderiv
{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]
[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']
[FiniteDimensional ℝ E']
{ι : Type u_10}
[Fintype ι]
[IsManifold I 1 M]
[IsManifold I' 1 M']
{o : Orientation I M ι}
{o' : Orientation I' M' ι}
{f : M → M'}
{x : M}
(h : o.IsOrientationPreservingAt o' f x)
:
(mfderiv% f x).IsInvertible
An orientation-preserving map has an invertible manifold derivative.
theorem
TauCeti.Manifold.Orientation.IsOrientationReversingAt.isInvertible_mfderiv
{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]
[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']
[FiniteDimensional ℝ E']
{ι : Type u_10}
[Fintype ι]
[IsManifold I 1 M]
[IsManifold I' 1 M']
{o : Orientation I M ι}
{o' : Orientation I' M' ι}
{f : M → M'}
{x : M}
(h : o.IsOrientationReversingAt o' f x)
:
(mfderiv% f x).IsInvertible
An orientation-reversing map has an invertible manifold derivative.
@[simp]
theorem
TauCeti.Manifold.Orientation.isOrientationPreservingAt_neg_left
{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]
[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']
[FiniteDimensional ℝ E']
{ι : Type u_10}
[Fintype ι]
[IsManifold I 1 M]
[IsManifold I' 1 M']
(o : Orientation I M ι)
(o' : Orientation I' M' ι)
(f : M → M')
(x : M)
:
Negating the source orientation exchanges preservation and reversal.
@[simp]
theorem
TauCeti.Manifold.Orientation.isOrientationPreservingAt_neg_right
{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]
[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']
[FiniteDimensional ℝ E']
{ι : Type u_10}
[Fintype ι]
[IsManifold I 1 M]
[IsManifold I' 1 M']
(o : Orientation I M ι)
(o' : Orientation I' M' ι)
(f : M → M')
(x : M)
:
Negating the target orientation exchanges preservation and reversal.
@[simp]
theorem
TauCeti.Manifold.Orientation.isOrientationReversingAt_neg_left
{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]
[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']
[FiniteDimensional ℝ E']
{ι : Type u_10}
[Fintype ι]
[IsManifold I 1 M]
[IsManifold I' 1 M']
(o : Orientation I M ι)
(o' : Orientation I' M' ι)
(f : M → M')
(x : M)
:
Negating the source orientation exchanges reversal and preservation.
@[simp]
theorem
TauCeti.Manifold.Orientation.isOrientationReversingAt_neg_right
{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]
[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']
[FiniteDimensional ℝ E']
{ι : Type u_10}
[Fintype ι]
[IsManifold I 1 M]
[IsManifold I' 1 M']
(o : Orientation I M ι)
(o' : Orientation I' M' ι)
(f : M → M')
(x : M)
:
Negating the target orientation exchanges reversal and preservation.
theorem
TauCeti.Manifold.Orientation.isOrientationReversingAt_iff_of_basis
{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]
[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']
[FiniteDimensional ℝ E']
{ι : Type u_10}
[Fintype ι]
[IsManifold I 1 M]
[IsManifold I' 1 M']
[DecidableEq ι]
{o : Orientation I M ι}
{o' : Orientation I' M' ι}
{f : M → M'}
{x : M}
(b : Module.Basis ι ℝ (TangentSpace I x))
(b' : Module.Basis ι ℝ (TangentSpace I' (f x)))
(hbb' : ∀ (i : ι), (mfderiv% f x) (b i) = b' i)
:
o.IsOrientationReversingAt o' f x ↔ (b.orientation = o.orientationAt x ↔ b'.orientation = -o'.orientationAt (f x))
If the derivative at x carries a basis b of the tangent space at x to the basis b' of
the tangent space at f x, then f reverses orientations at x exactly when b' is negatively
oriented if b is positively oriented, and positively oriented if b is negatively oriented.
theorem
TauCeti.Manifold.Orientation.not_isOrientationPreservingAt_and_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]
[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']
[FiniteDimensional ℝ E']
{ι : Type u_10}
[Fintype ι]
[IsManifold I 1 M]
[IsManifold I' 1 M']
(o : Orientation I M ι)
(o' : Orientation I' M' ι)
(f : M → M')
(x : M)
:
A map cannot preserve and reverse the same pair of orientations at one point.
theorem
TauCeti.Manifold.Orientation.isOrientationPreservingAt_of_apply_eq_of_mfderiv_eq_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]
[FiniteDimensional ℝ E]
{ι : Type u_10}
[Fintype ι]
[IsManifold I 1 M]
(o : Orientation I M ι)
{f : M → M}
{x : M}
(hx : f x = x)
(hd : mfderiv% f x = ContinuousLinearMap.id ℝ (TangentSpace I x))
:
o.IsOrientationPreservingAt o f x
A self-map fixing x whose derivative at x is the identity preserves every manifold
orientation at x.
@[simp]
theorem
TauCeti.Manifold.Orientation.isOrientationPreservingAt_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]
[FiniteDimensional ℝ E]
{ι : Type u_10}
[Fintype ι]
[IsManifold I 1 M]
(o : Orientation I M ι)
(x : M)
:
o.IsOrientationPreservingAt o id x
The identity map preserves every manifold orientation.
theorem
TauCeti.Manifold.Orientation.isOrientationReversingAt_id_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]
[FiniteDimensional ℝ E]
{ι : Type u_10}
[Fintype ι]
[IsManifold I 1 M]
(o : Orientation I M ι)
(x : M)
:
o.IsOrientationReversingAt (-o) id x
The identity map reverses an orientation when its target is given the opposite orientation.
theorem
TauCeti.Manifold.Orientation.IsOrientationPreservingAt.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]
[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']
[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'']
[FiniteDimensional ℝ E'']
{ι : Type u_10}
[Fintype ι]
[IsManifold I 1 M]
[IsManifold I' 1 M']
[IsManifold I'' 1 M'']
{o : Orientation I M ι}
{o' : Orientation I' M' ι}
{o'' : Orientation I'' M'' ι}
{f : M → M'}
{g : M' → M''}
{x : M}
(hgg : o'.IsOrientationPreservingAt o'' g (f x))
(hgf : o.IsOrientationPreservingAt o' f x)
:
o.IsOrientationPreservingAt o'' (g ∘ f) x
The composition of two orientation-preserving maps preserves orientations at a point.
theorem
TauCeti.Manifold.Orientation.IsOrientationPreservingAt.orientationAt_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]
[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']
[FiniteDimensional ℝ E']
{ι : Type u_10}
[Fintype ι]
[IsManifold I 1 M]
[IsManifold I' 1 M']
{o : Orientation I M ι}
{o' o'' : Orientation I' M' ι}
{f : M → M'}
{x : M}
(h' : o.IsOrientationPreservingAt o' f x)
(h'' : o.IsOrientationPreservingAt o'' f x)
:
Two orientations of M' from which a map preserves orientation at x, from the same
orientation of M, agree at f x.
theorem
TauCeti.Manifold.Orientation.IsOrientationPreservingAt.of_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]
[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']
[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'']
[FiniteDimensional ℝ E'']
{ι : Type u_10}
[Fintype ι]
[IsManifold I 1 M]
[IsManifold I' 1 M']
[IsManifold I'' 1 M'']
{o : Orientation I M ι}
{o' : Orientation I' M' ι}
{o'' : Orientation I'' M'' ι}
{f : M → M'}
{g : M' → M''}
{x : M}
(hgg : o'.IsOrientationPreservingAt o'' g (f x))
(hgf : o.IsOrientationPreservingAt o'' (g ∘ f) x)
(hf : MDiffAt f x)
:
o.IsOrientationPreservingAt o' f x
A differentiable map f preserves orientations at x when g ∘ f does and g preserves
orientations at f x.
theorem
TauCeti.Manifold.Orientation.IsOrientationPreservingAt.diffeomorph_symm
{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]
[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']
[FiniteDimensional ℝ E']
{ι : Type u_10}
[Fintype ι]
[IsManifold I 1 M]
[IsManifold I' 1 M']
{o : Orientation I M ι}
{o' : Orientation I' M' ι}
{n : WithTop ℕ∞}
{e : Diffeomorph I I' M M' n}
{y : M'}
(h : o.IsOrientationPreservingAt o' (⇑e) (e.symm y))
(hn : n ≠ 0)
:
o'.IsOrientationPreservingAt o (⇑e.symm) y
The inverse of a C^n diffeomorphism e, n ≠ 0, preserves orientations at y when e
preserves them at e.symm y.
theorem
TauCeti.Manifold.Orientation.isOrientationPreservingAt_zpow
{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]
[FiniteDimensional ℝ E]
{ι : Type u_10}
[Fintype ι]
[IsManifold I 1 M]
{o : Orientation I M ι}
{n : WithTop ℕ∞}
{φ : Diffeomorph I I M M n}
(h : ∀ (x : M), o.IsOrientationPreservingAt o (⇑φ) x)
(hn : n ≠ 0)
(k : ℤ)
(x : M)
:
o.IsOrientationPreservingAt o (⇑(φ ^ k)) x
If a C^n diffeomorphism φ of M, n ≠ 0, preserves an orientation o at every point,
then so does each of its integer powers φ ^ k.
theorem
TauCeti.Manifold.Orientation.IsOrientationReversingAt.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]
[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']
[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'']
[FiniteDimensional ℝ E'']
{ι : Type u_10}
[Fintype ι]
[IsManifold I 1 M]
[IsManifold I' 1 M']
[IsManifold I'' 1 M'']
{o : Orientation I M ι}
{o' : Orientation I' M' ι}
{o'' : Orientation I'' M'' ι}
{f : M → M'}
{g : M' → M''}
{x : M}
(hgg : o'.IsOrientationReversingAt o'' g (f x))
(hgf : o.IsOrientationReversingAt o' f x)
:
o.IsOrientationPreservingAt o'' (g ∘ f) x
The composition of two orientation-reversing maps preserves orientations at a point.
theorem
TauCeti.Manifold.Orientation.IsOrientationPreservingAt.comp_reversing
{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]
[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']
[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'']
[FiniteDimensional ℝ E'']
{ι : Type u_10}
[Fintype ι]
[IsManifold I 1 M]
[IsManifold I' 1 M']
[IsManifold I'' 1 M'']
{o : Orientation I M ι}
{o' : Orientation I' M' ι}
{o'' : Orientation I'' M'' ι}
{f : M → M'}
{g : M' → M''}
{x : M}
(hgg : o'.IsOrientationPreservingAt o'' g (f x))
(hgf : o.IsOrientationReversingAt o' f x)
:
o.IsOrientationReversingAt o'' (g ∘ f) x
Composing an orientation-preserving map after an orientation-reversing map reverses orientations at a point.
theorem
TauCeti.Manifold.Orientation.IsOrientationReversingAt.comp_preserving
{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]
[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']
[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'']
[FiniteDimensional ℝ E'']
{ι : Type u_10}
[Fintype ι]
[IsManifold I 1 M]
[IsManifold I' 1 M']
[IsManifold I'' 1 M'']
{o : Orientation I M ι}
{o' : Orientation I' M' ι}
{o'' : Orientation I'' M'' ι}
{f : M → M'}
{g : M' → M''}
{x : M}
(hgg : o'.IsOrientationReversingAt o'' g (f x))
(hgf : o.IsOrientationPreservingAt o' f x)
:
o.IsOrientationReversingAt o'' (g ∘ f) x
Composing an orientation-reversing map after an orientation-preserving map reverses orientations at a point.
theorem
TauCeti.Manifold.Orientation.isOrientationPreservingAt_of_orientationAt_eq
{N : Type u_11}
{N' : Type u_12}
[TopologicalSpace N]
[ChartedSpace ℝ N]
[IsManifold (modelWithCornersSelf ℝ ℝ) 1 N]
[TopologicalSpace N']
[ChartedSpace ℝ N']
[IsManifold (modelWithCornersSelf ℝ ℝ) 1 N']
{o : Orientation (modelWithCornersSelf ℝ ℝ) N (Fin 1)}
{o' : Orientation (modelWithCornersSelf ℝ ℝ) N' (Fin 1)}
{f : N → N'}
{x : N}
(ho : o.orientationAt x = (Module.Basis.singleton (Fin 1) ℝ).orientation)
(ho' : o'.orientationAt (f x) = (Module.Basis.singleton (Fin 1) ℝ).orientation)
{c : ℝ}
(hc : 0 < c)
(hf : mfderiv% f x = c • ContinuousLinearMap.id ℝ ℝ)
:
o.IsOrientationPreservingAt o' f x
For orientations of one-dimensional manifolds modelled on ℝ which are the standard
orientation of ℝ at x and at f x, a map whose derivative at x is multiplication by a
positive real number preserves orientation at x.
theorem
TauCeti.Manifold.Orientation.isOrientationReversingAt_of_orientationAt_eq
{N : Type u_11}
{N' : Type u_12}
[TopologicalSpace N]
[ChartedSpace ℝ N]
[IsManifold (modelWithCornersSelf ℝ ℝ) 1 N]
[TopologicalSpace N']
[ChartedSpace ℝ N']
[IsManifold (modelWithCornersSelf ℝ ℝ) 1 N']
{o : Orientation (modelWithCornersSelf ℝ ℝ) N (Fin 1)}
{o' : Orientation (modelWithCornersSelf ℝ ℝ) N' (Fin 1)}
{f : N → N'}
{x : N}
(ho : o.orientationAt x = (Module.Basis.singleton (Fin 1) ℝ).orientation)
(ho' : o'.orientationAt (f x) = (Module.Basis.singleton (Fin 1) ℝ).orientation)
{c : ℝ}
(hc : c < 0)
(hf : mfderiv% f x = c • ContinuousLinearMap.id ℝ ℝ)
:
o.IsOrientationReversingAt o' f x
For orientations of one-dimensional manifolds modelled on ℝ which are the standard
orientation of ℝ at x and at f x, a map whose derivative at x is multiplication by a
negative real number reverses orientation at x.
theorem
TauCeti.Manifold.Orientation.isOrientationPreservingAt_add_const
(a t : ℝ)
:
real.IsOrientationPreservingAt real (fun (x : ℝ) => x + a) t
Translations of ℝ preserve its standard orientation.
theorem
TauCeti.Manifold.Orientation.orientationAt_eq_orientationAt
{E : Type u_1}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[FiniteDimensional ℝ E]
{ι : Type u_10}
[Fintype ι]
(o : Orientation (modelWithCornersSelf ℝ E) E ι)
(x y : E)
:
An orientation of the model space is constant. An orientation of the connected model space
E has the same tangent orientation at any two points, the tangent spaces of E all being E.
theorem
TauCeti.Manifold.Orientation.isOrientationPreservingAt_of_det_pos
{E : Type u_1}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[FiniteDimensional ℝ E]
{ι : Type u_10}
[Fintype ι]
(o : Orientation (modelWithCornersSelf ℝ E) E ι)
(L : E ≃L[ℝ] E)
(hL : 0 < LinearMap.det ↑↑L)
(x : E)
:
o.IsOrientationPreservingAt o (⇑L) x
A continuous linear automorphism of E with positive determinant preserves every orientation
of E, at every point.
theorem
TauCeti.Manifold.Orientation.isOrientationReversingAt_of_det_neg
{E : Type u_1}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[FiniteDimensional ℝ E]
{ι : Type u_10}
[Fintype ι]
(o : Orientation (modelWithCornersSelf ℝ E) E ι)
(L : E ≃L[ℝ] E)
(hL : LinearMap.det ↑↑L < 0)
(x : E)
:
o.IsOrientationReversingAt o (⇑L) x
A continuous linear automorphism of E with negative determinant reverses every orientation
of E, at every point.
theorem
TauCeti.Manifold.Orientation.isOrientationReversingAt_of_det_fderiv_neg
{E : Type u_1}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[FiniteDimensional ℝ E]
{ι : Type u_10}
[Fintype ι]
(o : Orientation (modelWithCornersSelf ℝ E) E ι)
{f : E → E}
{v : E}
(hdet : (fderiv ℝ f v).det < 0)
:
o.IsOrientationReversingAt o f v
A negative Jacobian determinant reverses orientation. A map of a finite-dimensional
real normed space with negative derivative determinant at v reverses every orientation there.
theorem
TauCeti.Manifold.Orientation.isOrientationPreservingAt_comp_of_det_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]
[FiniteDimensional ℝ E]
{ι : Type u_10}
[Fintype ι]
[IsManifold I 1 M]
{oE : Orientation (modelWithCornersSelf ℝ E) E ι}
{oM : Orientation I M ι}
{e : E → M}
{L : E ≃L[ℝ] E}
{x : E}
(he : oE.IsOrientationReversingAt oM e (L x))
(hL : LinearMap.det ↑↑L < 0)
:
oE.IsOrientationPreservingAt oM (e ∘ ⇑L) x
Precomposing a map which reverses orientations at L x with a continuous linear automorphism
L of E of negative determinant gives a map which preserves them at x.
theorem
TauCeti.Manifold.Orientation.isOrientationReversingAt_comp_of_det_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]
[FiniteDimensional ℝ E]
{ι : Type u_10}
[Fintype ι]
[IsManifold I 1 M]
{oE : Orientation (modelWithCornersSelf ℝ E) E ι}
{oM : Orientation I M ι}
{e : E → M}
{L : E ≃L[ℝ] E}
{x : E}
(he : oE.IsOrientationPreservingAt oM e (L x))
(hL : LinearMap.det ↑↑L < 0)
:
oE.IsOrientationReversingAt oM (e ∘ ⇑L) x
Precomposing a map which preserves orientations at L x with a continuous linear automorphism
L of E of negative determinant gives a map which reverses them at x.
@[simp]
theorem
TauCeti.Manifold.Orientation.isOrientationPreservingAt_congrModel_left
{E : Type u_1}
{H : Type u_2}
{M : Type u_3}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[TopologicalSpace H]
[TopologicalSpace M]
[ChartedSpace H 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']
[FiniteDimensional ℝ E']
{ι : Type u_10}
[Fintype ι]
{I J : ModelWithCorners ℝ E H}
(h : I = J)
[IsManifold I 1 M]
[IsManifold J 1 M]
[IsManifold I' 1 M']
(o : Orientation I M ι)
(o' : Orientation I' M' ι)
(f : M → M')
(x : M)
:
@[simp]
theorem
TauCeti.Manifold.Orientation.isOrientationPreservingAt_congrModel_right
{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]
[FiniteDimensional ℝ E]
{E' : Type u_4}
{H' : Type u_5}
{M' : Type u_6}
[NormedAddCommGroup E']
[NormedSpace ℝ E']
[TopologicalSpace H']
[TopologicalSpace M']
[ChartedSpace H' M']
[FiniteDimensional ℝ E']
{ι : Type u_10}
[Fintype ι]
{I' J' : ModelWithCorners ℝ E' H'}
(h : I' = J')
[IsManifold I 1 M]
[IsManifold I' 1 M']
[IsManifold J' 1 M']
(o : Orientation I M ι)
(o' : Orientation I' M' ι)
(f : M → M')
(x : M)
:
@[simp]
theorem
TauCeti.Manifold.Orientation.isOrientationReversingAt_congrModel_left
{E : Type u_1}
{H : Type u_2}
{M : Type u_3}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[TopologicalSpace H]
[TopologicalSpace M]
[ChartedSpace H 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']
[FiniteDimensional ℝ E']
{ι : Type u_10}
[Fintype ι]
{I J : ModelWithCorners ℝ E H}
(h : I = J)
[IsManifold I 1 M]
[IsManifold J 1 M]
[IsManifold I' 1 M']
(o : Orientation I M ι)
(o' : Orientation I' M' ι)
(f : M → M')
(x : M)
:
@[simp]
theorem
TauCeti.Manifold.Orientation.isOrientationReversingAt_congrModel_right
{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]
[FiniteDimensional ℝ E]
{E' : Type u_4}
{H' : Type u_5}
{M' : Type u_6}
[NormedAddCommGroup E']
[NormedSpace ℝ E']
[TopologicalSpace H']
[TopologicalSpace M']
[ChartedSpace H' M']
[FiniteDimensional ℝ E']
{ι : Type u_10}
[Fintype ι]
{I' J' : ModelWithCorners ℝ E' H'}
(h : I' = J')
[IsManifold I 1 M]
[IsManifold I' 1 M']
[IsManifold J' 1 M']
(o : Orientation I M ι)
(o' : Orientation I' M' ι)
(f : M → M')
(x : M)
:
theorem
TauCeti.Manifold.Orientation.isOrientationPreservingAt_id_congrModel
{E : Type u_1}
{H : Type u_2}
{M : Type u_3}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[TopologicalSpace H]
[TopologicalSpace M]
[ChartedSpace H M]
[FiniteDimensional ℝ E]
{ι : Type u_10}
[Fintype ι]
{I J : ModelWithCorners ℝ E H}
(h : I = J)
[IsManifold I 1 M]
[IsManifold J 1 M]
(o : Orientation I M ι)
(x : M)
:
o.IsOrientationPreservingAt (congrModel h o) id x
Casting an orientation along an equality of models gives an orientation preserved by id.
theorem
TauCeti.Manifold.OrientationLift.signAt_mul_signAt_mul_det_pos
{E : Type u_1}
{E' : Type u_2}
{H : Type u_3}
{H' : Type u_4}
{M : Type u_5}
{N : Type u_6}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[FiniteDimensional ℝ E]
[TopologicalSpace H]
{I : ModelWithCorners ℝ E H}
[TopologicalSpace M]
[ChartedSpace H M]
[IsManifold I 1 M]
[NormedAddCommGroup E']
[NormedSpace ℝ E']
[FiniteDimensional ℝ E']
[TopologicalSpace H']
{J : ModelWithCorners ℝ E' H'}
[TopologicalSpace N]
[ChartedSpace H' N]
[IsManifold J 1 N]
{k : ℕ}
(l : OrientationLift I M (Fin k))
(l' : OrientationLift J N (Fin k))
(C : E ≃L[ℝ] E')
(hl : l'.modelOrientation = (Orientation.map (Fin k) ↑C) l.modelOrientation)
{f : M → N}
{x : M}
(hf : MDiffAt f x)
(ho : (Orientation.mk l).IsOrientationPreservingAt (Orientation.mk l') f x)
{β : M}
{α : N}
(hx : x ∈ (chartAt H β).source)
(hfx : f x ∈ (chartAt H' α).source)
:
0 < ↑↑(l.signAt β x) * ↑↑(l'.signAt α (f x)) * (↑C.symm ∘SL fderivWithin ℝ (↑(extChartAt J α) ∘ f ∘ ↑(extChartAt I β).symm) (Set.range ↑I) (↑(extChartAt I β) x)).det
If f preserves the orientations of two lifts whose model orientations correspond under a
continuous linear equivalence C : E ≃ E' of the model spaces, then the chart signs of the lifts
compensate the sign of the coordinate Jacobian of f between any two preferred charts, read in
E through C.