Source-indexed orientation lifts

An orientation lift consists of an orientation of the model vector space and locally constant signs defined only on the source of each preferred chart. The signs compensate for the sign of the transition derivative within the model range, including boundary and corner points. Simultaneously reversing the model orientation and every chart sign leaves the induced tangent orientations unchanged, and TauCeti.Manifold.OrientationLift.congrModel casts lifts along an equality of models on the same model vector space and chart carrier.

References

• Michael Lee's Mathlib PR #35376: the chart-sign lift and diagonal-quotient design, adapted here to source-indexed signs and actual tangent-bundle trivializations.
• J. M. Lee, Introduction to Smooth Manifolds, second edition, Chapter 15.
• TauCeti PR #15107: the earlier formalization of the chart-sign lift and diagonal-flip quotient.

structure TauCeti.Manifold.OrientationLift {E : Type u_1} {H : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] (I : ModelWithCorners ℝ E H) (M : Type u_5) [TopologicalSpace M] [ChartedSpace H M] (ι : Type u_6) [Fintype ι] [FiniteDimensional ℝ E] : Type (max (max u_1 u_5) u_6)

A model orientation with source-indexed chart signs. Compatibility is expressed through actual transition Jacobians within range I, including boundary and corner points.

• modelOrientation : Orientation ℝ E ι

  Orientation of the model vector space.

• card_eq : Fintype.card ι = Module.finrank ℝ E

  The index type has the dimension of the model space.

• sign (α : M) : ↑(chartAt H α).source → ℤˣ

  A sign only at points lying in the chosen preferred chart's source.

• locallyConstant_sign (α : M) : IsLocallyConstant (self.sign α)

  Chart signs are locally constant on their actual domains.

• compatible (α β x : M) (hα : x ∈ (chartAt H α).source) (hβ : x ∈ (chartAt H β).source) : 0 < ↑↑(self.sign α ⟨x, hα⟩) * ↑↑(self.sign β ⟨x, hβ⟩) * (fderivWithin ℝ (↑(extChartAt I β) ∘ ↑(extChartAt I α).symm) (Set.range ↑I) (↑(extChartAt I α) x)).det

  The two chart signs compensate for the sign of the within-range transition Jacobian.

theorem TauCeti.Manifold.OrientationLift.ext_iff {E : Type u_1} {H : Type u_2} {inst✝ : NormedAddCommGroup E} {inst✝¹ : NormedSpace ℝ E} {inst✝² : TopologicalSpace H} {I : ModelWithCorners ℝ E H} {M : Type u_5} {inst✝³ : TopologicalSpace M} {inst✝⁴ : ChartedSpace H M} {ι : Type u_6} {inst✝⁵ : Fintype ι} {inst✝⁶ : FiniteDimensional ℝ E} {x y : OrientationLift I M ι} : x = y ↔ x.modelOrientation = y.modelOrientation ∧ x.sign = y.sign

theorem TauCeti.Manifold.OrientationLift.ext {E : Type u_1} {H : Type u_2} {inst✝ : NormedAddCommGroup E} {inst✝¹ : NormedSpace ℝ E} {inst✝² : TopologicalSpace H} {I : ModelWithCorners ℝ E H} {M : Type u_5} {inst✝³ : TopologicalSpace M} {inst✝⁴ : ChartedSpace H M} {ι : Type u_6} {inst✝⁵ : Fintype ι} {inst✝⁶ : FiniteDimensional ℝ E} {x y : OrientationLift I M ι} (modelOrientation : x.modelOrientation = y.modelOrientation) (sign : x.sign = y.sign) : x = y

def TauCeti.Manifold.OrientationLift.congrChartAt {E : Type u_1} {H : Type u_2} {M : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] {I : ModelWithCorners ℝ E H} [TopologicalSpace M] {ι : Type u_4} [Fintype ι] [FiniteDimensional ℝ E] {c c' : ChartedSpace H M} (h : ChartedSpace.chartAt = ChartedSpace.chartAt) (o : OrientationLift I M ι) : OrientationLift I M ι

Changing the atlas without changing its preferred charts leaves the lift data unchanged.

@[simp]

theorem TauCeti.Manifold.OrientationLift.congrChartAt_modelOrientation {E : Type u_1} {H : Type u_2} {M : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] {I : ModelWithCorners ℝ E H} [TopologicalSpace M] {ι : Type u_4} [Fintype ι] [FiniteDimensional ℝ E] {c c' : ChartedSpace H M} (h : ChartedSpace.chartAt = ChartedSpace.chartAt) (o : OrientationLift I M ι) : (congrChartAt h o).modelOrientation = o.modelOrientation

Changing only the atlas preserves the model orientation.

@[simp]

theorem TauCeti.Manifold.OrientationLift.congrChartAt_sign {E : Type u_1} {H : Type u_2} {M : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] {I : ModelWithCorners ℝ E H} [TopologicalSpace M] {ι : Type u_4} [Fintype ι] [FiniteDimensional ℝ E] {c c' : ChartedSpace H M} (h : ChartedSpace.chartAt = ChartedSpace.chartAt) (o : OrientationLift I M ι) (α : M) (x : ↑(ChartedSpace.chartAt α).source) : (congrChartAt h o).sign α x = o.sign α ⟨↑x, ⋯⟩

Changing only the atlas transports each source sign along equality of preferred charts.

theorem TauCeti.Manifold.OrientationLift.sign_mul_sign {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] {ι : Type u_4} [Fintype ι] [FiniteDimensional ℝ E] (o : OrientationLift I M ι) (α β x : M) (hα : x ∈ (chartAt H α).source) (hβ : x ∈ (chartAt H β).source) : ↑(o.sign α ⟨x, hα⟩ * o.sign β ⟨x, hβ⟩) = ↑(SignType.sign (fderivWithin ℝ (↑(extChartAt I β) ∘ ↑(extChartAt I α).symm) (Set.range ↑I) (↑(extChartAt I α) x)).det)

The product of the source signs is exactly the sign of the within-range transition Jacobian.

theorem TauCeti.Manifold.OrientationLift.sign_mul_det {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] {ι : Type u_4} [Fintype ι] [FiniteDimensional ℝ E] (o : OrientationLift I M ι) (α β x : M) (hα : x ∈ (chartAt H α).source) (hβ : x ∈ (chartAt H β).source) : ↑↑(o.sign α ⟨x, hα⟩) * (fderivWithin ℝ (↑(extChartAt I β) ∘ ↑(extChartAt I α).symm) (Set.range ↑I) (↑(extChartAt I α) x)).det = |(fderivWithin ℝ (↑(extChartAt I β) ∘ ↑(extChartAt I α).symm) (Set.range ↑I) (↑(extChartAt I α) x)).det| * ↑↑(o.sign β ⟨x, hβ⟩)

Signed transition determinants agree with the absolute Jacobian factor appearing in the change-of-variables theorem for top forms.

def TauCeti.Manifold.OrientationLift.flip {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] {ι : Type u_4} [Fintype ι] [FiniteDimensional ℝ E] (o : OrientationLift I M ι) : OrientationLift I M ι

Simultaneously reverse the model orientation and all source signs. This changes only the representative lift, not any induced tangent orientation.

@[simp]

theorem TauCeti.Manifold.OrientationLift.flip_modelOrientation {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] {ι : Type u_4} [Fintype ι] [FiniteDimensional ℝ E] (o : OrientationLift I M ι) : o.flip.modelOrientation = -o.modelOrientation

@[simp]

theorem TauCeti.Manifold.OrientationLift.flip_sign {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] {ι : Type u_4} [Fintype ι] [FiniteDimensional ℝ E] (o : OrientationLift I M ι) (α : M) (x : ↑(chartAt H α).source) : o.flip.sign α x = -o.sign α x

@[simp]

theorem TauCeti.Manifold.OrientationLift.flip_flip {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] {ι : Type u_4} [Fintype ι] [FiniteDimensional ℝ E] (o : OrientationLift I M ι) : o.flip.flip = o

@[instance_reducible]

instance TauCeti.Manifold.OrientationLift.instNeg {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] {ι : Type u_4} [Fintype ι] [FiniteDimensional ℝ E] : Neg (OrientationLift I M ι)

Reverse the induced orientation while holding the chart signs fixed.

@[simp]

theorem TauCeti.Manifold.OrientationLift.neg_modelOrientation {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] {ι : Type u_4} [Fintype ι] [FiniteDimensional ℝ E] (o : OrientationLift I M ι) : (-o).modelOrientation = -o.modelOrientation

@[simp]

theorem TauCeti.Manifold.OrientationLift.neg_sign {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] {ι : Type u_4} [Fintype ι] [FiniteDimensional ℝ E] (o : OrientationLift I M ι) (α : M) (x : ↑(chartAt H α).source) : (-o).sign α x = o.sign α x

def TauCeti.Manifold.OrientationLift.reindex {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] {ι : Type u_4} [Fintype ι] [FiniteDimensional ℝ E] {ι' : Type u_5} [Fintype ι'] (e : ι ≃ ι') (o : OrientationLift I M ι) : OrientationLift I M ι'

Reindex the model orientation of a lift along an equivalence of index types, keeping its chart signs.

@[simp]

theorem TauCeti.Manifold.OrientationLift.reindex_modelOrientation {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] {ι : Type u_4} [Fintype ι] [FiniteDimensional ℝ E] {ι' : Type u_5} [Fintype ι'] (e : ι ≃ ι') (o : OrientationLift I M ι) : (reindex e o).modelOrientation = (Orientation.reindex ℝ E e) o.modelOrientation

@[simp]

theorem TauCeti.Manifold.OrientationLift.reindex_sign {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] {ι : Type u_4} [Fintype ι] [FiniteDimensional ℝ E] {ι' : Type u_5} [Fintype ι'] (e : ι ≃ ι') (o : OrientationLift I M ι) (α : M) (x : ↑(chartAt H α).source) : (reindex e o).sign α x = o.sign α x

@[simp]

theorem TauCeti.Manifold.OrientationLift.reindex_flip {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] {ι : Type u_4} [Fintype ι] [FiniteDimensional ℝ E] {ι' : Type u_5} [Fintype ι'] (e : ι ≃ ι') (o : OrientationLift I M ι) : reindex e o.flip = (reindex e o).flip

Reindexing commutes with the diagonal flip.

noncomputable def TauCeti.Manifold.OrientationLift.signAt {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] {ι : Type u_4} [Fintype ι] [FiniteDimensional ℝ E] (o : OrientationLift I M ι) (α x : M) : ℤˣ

A total chart sign with the fixed value 1 off the chart source. Only the source-indexed signs are part of the lift.

@[simp]

theorem TauCeti.Manifold.OrientationLift.signAt_of_mem {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] {ι : Type u_4} [Fintype ι] [FiniteDimensional ℝ E] (o : OrientationLift I M ι) {α x : M} (hx : x ∈ (chartAt H α).source) : o.signAt α x = o.sign α ⟨x, hx⟩

@[simp]

theorem TauCeti.Manifold.OrientationLift.signAt_of_notMem {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] {ι : Type u_4} [Fintype ι] [FiniteDimensional ℝ E] (o : OrientationLift I M ι) {α x : M} (hx : x ∉ (chartAt H α).source) : o.signAt α x = 1

theorem TauCeti.Manifold.OrientationLift.continuousOn_signAt {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] {ι : Type u_4} [Fintype ι] [FiniteDimensional ℝ E] (o : OrientationLift I M ι) (α : M) : ContinuousOn (o.signAt α) (chartAt H α).source

The total sign is continuous when restricted to the actual preferred chart source.

@[simp]

theorem TauCeti.Manifold.OrientationLift.neg_signAt {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] {ι : Type u_4} [Fintype ι] [FiniteDimensional ℝ E] (o : OrientationLift I M ι) (α x : M) : (-o).signAt α x = o.signAt α x

theorem TauCeti.Manifold.OrientationLift.flip_signAt_of_mem {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] {ι : Type u_4} [Fintype ι] [FiniteDimensional ℝ E] (o : OrientationLift I M ι) {α x : M} (hx : x ∈ (chartAt H α).source) : o.flip.signAt α x = -o.signAt α x

Diagonal reversal negates the total sign on the chart source.

def TauCeti.Manifold.OrientationLift.chartOrientation {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] {ι : Type u_4} [Fintype ι] [FiniteDimensional ℝ E] (o : OrientationLift I M ι) (α : M) (x : ↑(chartAt H α).source) : Orientation ℝ E ι

The signed model orientation read in a preferred chart at a point of its source.

theorem TauCeti.Manifold.OrientationLift.chartOrientation_eq_ite {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] {ι : Type u_4} [Fintype ι] [FiniteDimensional ℝ E] (o : OrientationLift I M ι) (α : M) (x : ↑(chartAt H α).source) : o.chartOrientation α x = if o.sign α x = 1 then o.modelOrientation else -o.modelOrientation

The chart orientation is the model orientation or its negative according to the chart sign.

noncomputable def TauCeti.Manifold.OrientationLift.orientationAt {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] {ι : Type u_4} [Fintype ι] [FiniteDimensional ℝ E] [IsManifold I 1 M] (o : OrientationLift I M ι) (x : M) : Orientation ℝ (TangentSpace I x) ι

The tangent orientation induced by a lift, using the actual inverse tangent trivialization of the preferred chart at the point.

@[simp]

theorem TauCeti.Manifold.OrientationLift.mapOrientation_orientationAt {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] {ι : Type u_4} [Fintype ι] [FiniteDimensional ℝ E] [IsManifold I 1 M] (o : OrientationLift I M ι) {α x : M} (hα : x ∈ (chartAt H α).source) : (Bundle.Trivialization.mapOrientation ι (trivializationAt E (TangentSpace I) α) ⋯) (o.orientationAt x) = o.chartOrientation α ⟨x, hα⟩

Reading the tangent orientation in any preferred chart gives precisely its signed model orientation. Thus the construction is independent of the chosen chart.

@[simp]

theorem TauCeti.Manifold.OrientationLift.orientationAt_flip {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] {ι : Type u_4} [Fintype ι] [FiniteDimensional ℝ E] [IsManifold I 1 M] (o : OrientationLift I M ι) (x : M) : o.flip.orientationAt x = o.orientationAt x

Diagonally flipping a lift preserves every actual tangent orientation.

theorem TauCeti.Manifold.OrientationLift.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] {ι : Type u_4} [Fintype ι] [FiniteDimensional ℝ E] [IsManifold I 1 M] (o : OrientationLift I M ι) (x : M) : o.orientationAt x = o.chartOrientation x ⟨x, ⋯⟩

The tangent orientation at a point is its signed model orientation in that point's preferred chart.

theorem TauCeti.Manifold.OrientationLift.signBasis_orientationAt {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] {ι : Type u_4} [Fintype ι] [FiniteDimensional ℝ E] [IsManifold I 1 M] [DecidableEq ι] (o : OrientationLift I M ι) (b : Module.Basis ι ℝ E) (x : M) : (o.orientationAt x).signBasis b = o.modelOrientation.signBasis b * o.signAt x x

The tangent basis sign is the model basis sign multiplied by the preferred chart sign.

theorem TauCeti.Manifold.OrientationLift.signBasis_mul_signAt_mul_abs_det_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] {ι : Type u_4} [Fintype ι] [FiniteDimensional ℝ E] [DecidableEq ι] (l : OrientationLift I M ι) (b : Module.Basis ι ℝ E) (α : M) {x : M} (hx : x ∈ (chartAt H α).source) (L : E ≃ₗ[ℝ] E) (hB : (b.map L).orientation = l.chartOrientation α ⟨x, hx⟩) : ↑↑(l.modelOrientation.signBasis b) * ↑↑(l.signAt α x) * |LinearMap.det ↑L| = LinearMap.det ↑L

The chart sign and the absolute determinant of a linear equivalence carrying a basis b to a basis of the chart orientation combine to the determinant itself.

noncomputable def TauCeti.Manifold.OrientationLift.toVectorBundleOrientation {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] {ι : Type u_4} [Fintype ι] [FiniteDimensional ℝ E] [IsManifold I 1 M] (o : OrientationLift I M ι) : VectorBundleOrientation E (TangentSpace I) ι

The tangent orientations of a lift vary locally constantly in bundle trivializations.

@[simp]

theorem TauCeti.Manifold.OrientationLift.toVectorBundleOrientation_apply {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] {ι : Type u_4} [Fintype ι] [FiniteDimensional ℝ E] [IsManifold I 1 M] (o : OrientationLift I M ι) (x : M) : o.toVectorBundleOrientation x = o.orientationAt x

@[simp]

theorem TauCeti.Manifold.OrientationLift.orientationAt_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] {ι : Type u_4} [Fintype ι] [FiniteDimensional ℝ E] [IsManifold I 1 M] (o : OrientationLift I M ι) (x : M) : (-o).orientationAt x = -o.orientationAt x

Negating the model orientation reverses every induced tangent orientation.

@[simp]

theorem TauCeti.Manifold.OrientationLift.orientationAt_reindex {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] {ι : Type u_4} [Fintype ι] [FiniteDimensional ℝ E] [IsManifold I 1 M] {ι' : Type u_5} [Fintype ι'] (e : ι ≃ ι') (o : OrientationLift I M ι) (x : M) : (reindex e o).orientationAt x = (Orientation.reindex ℝ (TangentSpace I x) e) (o.orientationAt x)

Reindexing a lift reindexes every induced tangent orientation.

noncomputable def TauCeti.Manifold.OrientationLift.ofVectorBundleOrientation {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] {ι : Type u_4} [Fintype ι] [FiniteDimensional ℝ E] [IsManifold I 1 M] (model : Orientation ℝ E ι) (hι : Fintype.card ι = Module.finrank ℝ E) (o : VectorBundleOrientation E (TangentSpace I) ι) : OrientationLift I M ι

Every orientation of the tangent bundle gives a source-indexed lift, after choosing a model orientation. The model choice disappears in the diagonal quotient.

@[simp]

theorem TauCeti.Manifold.OrientationLift.orientationAt_ofVectorBundleOrientation {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] {ι : Type u_4} [Fintype ι] [FiniteDimensional ℝ E] [IsManifold I 1 M] (model : Orientation ℝ E ι) (hι : Fintype.card ι = Module.finrank ℝ E) (o : VectorBundleOrientation E (TangentSpace I) ι) (x : M) : (ofVectorBundleOrientation model hι o).orientationAt x = o x

The lift reconstructed from a tangent bundle orientation recovers that orientation pointwise.

def TauCeti.Manifold.OrientationLift.ofHasGroupoid {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] {ι : Type u_4} [Fintype ι] [FiniteDimensional ℝ E] [IsManifold I 1 M] [HasGroupoid M (orientationPreservingGroupoid I)] (model : Orientation ℝ E ι) (hι : Fintype.card ι = Module.finrank ℝ E) : OrientationLift I M ι

When the given atlas has positive transition derivatives, every model orientation is the model orientation of the orientation lift all of whose chart signs are 1. On a model with corners, whose preferred charts are all the identity, this is the constant model orientation.

@[simp]

theorem TauCeti.Manifold.OrientationLift.ofHasGroupoid_modelOrientation {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] {ι : Type u_4} [Fintype ι] [FiniteDimensional ℝ E] [IsManifold I 1 M] [HasGroupoid M (orientationPreservingGroupoid I)] (model : Orientation ℝ E ι) (hι : Fintype.card ι = Module.finrank ℝ E) : (ofHasGroupoid model hι).modelOrientation = model

@[simp]

theorem TauCeti.Manifold.OrientationLift.ofHasGroupoid_sign {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] {ι : Type u_4} [Fintype ι] [FiniteDimensional ℝ E] [IsManifold I 1 M] [HasGroupoid M (orientationPreservingGroupoid I)] (model : Orientation ℝ E ι) (hι : Fintype.card ι = Module.finrank ℝ E) (α : M) (x : ↑(chartAt H α).source) : (ofHasGroupoid model hι).sign α x = 1

@[simp]

theorem TauCeti.Manifold.OrientationLift.orientationAt_ofHasGroupoid {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] {ι : Type u_4} [Fintype ι] [FiniteDimensional ℝ E] [IsManifold I 1 M] [HasGroupoid M (orientationPreservingGroupoid I)] (model : Orientation ℝ E ι) (hι : Fintype.card ι = Module.finrank ℝ E) (x : M) : (ofHasGroupoid model hι).orientationAt x = model

At every point, the tangent orientation of ofHasGroupoid model hι, read in the preferred chart at that point, is the model orientation.

theorem TauCeti.Manifold.OrientationLift.ext_of_orientationAt {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] {ι : Type u_4} [Fintype ι] [FiniteDimensional ℝ E] [IsManifold I 1 M] {o o' : OrientationLift I M ι} (hm : o.modelOrientation = o'.modelOrientation) (h : ∀ (x : M), o.orientationAt x = o'.orientationAt x) : o = o'

Two lifts with the same model orientation and tangent orientations have the same signs.

theorem TauCeti.Manifold.OrientationLift.eq_or_eq_flip_of_orientationAt {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] {ι : Type u_4} [Fintype ι] [FiniteDimensional ℝ E] [IsManifold I 1 M] {o o' : OrientationLift I M ι} (h : ∀ (x : M), o.orientationAt x = o'.orientationAt x) : o = o' ∨ o = o'.flip

Equality of the induced tangent orientations identifies precisely the diagonal flip.

@[simp]

theorem TauCeti.Manifold.OrientationLift.neg_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] {ι : Type u_4} [Fintype ι] [FiniteDimensional ℝ E] (o : OrientationLift I M ι) : - -o = o

@[simp]

theorem TauCeti.Manifold.OrientationLift.flip_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] {ι : Type u_4} [Fintype ι] [FiniteDimensional ℝ E] (o : OrientationLift I M ι) : (-o).flip = -o.flip

def TauCeti.Manifold.OrientationLift.setoid {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] {ι : Type u_4} [Fintype ι] [FiniteDimensional ℝ E] : Setoid (OrientationLift I M ι)

The equivalence relation that forgets the simultaneous reversal of the model orientation and all chart signs.

theorem TauCeti.Manifold.OrientationLift.setoid_rel {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] {ι : Type u_4} [Fintype ι] [FiniteDimensional ℝ E] (o o' : OrientationLift I M ι) : setoid o o' ↔ o' = o ∨ o' = o.flip

The diagonal equivalence relation is equality or simultaneous sign reversal.

def TauCeti.Manifold.OrientationLift.congrModel {E : Type u_1} {H : Type u_2} {M : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] [TopologicalSpace M] [ChartedSpace H M] {ι : Type u_4} [Fintype ι] [FiniteDimensional ℝ E] {I J : ModelWithCorners ℝ E H} (h : I = J) (o : OrientationLift I M ι) : OrientationLift J M ι

Cast an orientation lift along an equality of models on the same model vector space and chart carrier.

@[simp]

theorem TauCeti.Manifold.OrientationLift.congrModel_modelOrientation {E : Type u_1} {H : Type u_2} {M : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] [TopologicalSpace M] [ChartedSpace H M] {ι : Type u_4} [Fintype ι] [FiniteDimensional ℝ E] {I J : ModelWithCorners ℝ E H} (h : I = J) (o : OrientationLift I M ι) : (congrModel h o).modelOrientation = o.modelOrientation

@[simp]

theorem TauCeti.Manifold.OrientationLift.congrModel_sign {E : Type u_1} {H : Type u_2} {M : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] [TopologicalSpace M] [ChartedSpace H M] {ι : Type u_4} [Fintype ι] [FiniteDimensional ℝ E] {I J : ModelWithCorners ℝ E H} (h : I = J) (o : OrientationLift I M ι) (α : M) (x : ↑(chartAt H α).source) : (congrModel h o).sign α x = o.sign α x

@[simp]

theorem TauCeti.Manifold.OrientationLift.congrModel_signAt {E : Type u_1} {H : Type u_2} {M : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] [TopologicalSpace M] [ChartedSpace H M] {ι : Type u_4} [Fintype ι] [FiniteDimensional ℝ E] {I J : ModelWithCorners ℝ E H} (h : I = J) (o : OrientationLift I M ι) (α x : M) : (congrModel h o).signAt α x = o.signAt α x

@[simp]

theorem TauCeti.Manifold.OrientationLift.congrModel_refl {E : Type u_1} {H : Type u_2} {M : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] [TopologicalSpace M] [ChartedSpace H M] {ι : Type u_4} [Fintype ι] [FiniteDimensional ℝ E] {I : ModelWithCorners ℝ E H} (o : OrientationLift I M ι) : congrModel ⋯ o = o

@[simp]

theorem TauCeti.Manifold.OrientationLift.congrModel_congrModel {E : Type u_1} {H : Type u_2} {M : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] [TopologicalSpace M] [ChartedSpace H M] {ι : Type u_4} [Fintype ι] [FiniteDimensional ℝ E] {I J K : ModelWithCorners ℝ E H} (h₁ : I = J) (h₂ : J = K) (o : OrientationLift I M ι) : congrModel h₂ (congrModel h₁ o) = congrModel ⋯ o

@[simp]

theorem TauCeti.Manifold.OrientationLift.flip_congrModel {E : Type u_1} {H : Type u_2} {M : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] [TopologicalSpace M] [ChartedSpace H M] {ι : Type u_4} [Fintype ι] [FiniteDimensional ℝ E] {I J : ModelWithCorners ℝ E H} (h : I = J) (o : OrientationLift I M ι) : (congrModel h o).flip = congrModel h o.flip

@[simp]

theorem TauCeti.Manifold.OrientationLift.neg_congrModel {E : Type u_1} {H : Type u_2} {M : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] [TopologicalSpace M] [ChartedSpace H M] {ι : Type u_4} [Fintype ι] [FiniteDimensional ℝ E] {I J : ModelWithCorners ℝ E H} (h : I = J) (o : OrientationLift I M ι) : congrModel h (-o) = -congrModel h o

@[simp]

theorem TauCeti.Manifold.OrientationLift.orientationAt_congrModel {E : Type u_1} {H : Type u_2} {M : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] [TopologicalSpace M] [ChartedSpace H M] {ι : Type u_4} [Fintype ι] [FiniteDimensional ℝ E] {I J : ModelWithCorners ℝ E H} (h : I = J) [IsManifold I 1 M] [IsManifold J 1 M] (o : OrientationLift I M ι) (x : M) : (congrModel h o).orientationAt x = o.orientationAt x