The increasing orientation of a closed interval #

The preferred left half-line chart has positive sign and the preferred right half-line chart has negative sign. These source signs define the increasing orientation despite the reversing transition between the two half-line charts.

source

noncomputable def TauCeti.Manifold.OrientationLift.interval (a b : ℝ) [Fact (a < b)] :

OrientationLift (modelWithCornersEuclideanHalfSpace 1) (↑(Set.Icc a b)) (Fin 1)

The increasing interval orientation is represented by positive signs in left half-line charts and negative signs in right half-line charts.

Instances For

source

@[simp]

theorem TauCeti.Manifold.OrientationLift.interval_modelOrientation (a b : ℝ) [Fact (a < b)] :

(interval a b).modelOrientation = (EuclideanSpace.basisFun (Fin 1) ℝ).toBasis.orientation

The interval lift uses the standard positive model orientation.

source

@[simp]

theorem TauCeti.Manifold.OrientationLift.interval_sign (a b : ℝ) [Fact (a < b)] (α : ↑(Set.Icc a b)) (x : ↑(chartAt (EuclideanHalfSpace 1) α).source) :

(interval a b).sign α x = if ↑α < b then 1 else -1

The interval lift's chart sign is determined by the actual preferred chart.

source

noncomputable def TauCeti.Manifold.Orientation.interval (a b : ℝ) [Fact (a < b)] :

Orientation (modelWithCornersEuclideanHalfSpace 1) (↑(Set.Icc a b)) (Fin 1)

The canonical increasing orientation of a nondegenerate closed interval.

Instances For

source

@[simp]

theorem TauCeti.Manifold.Orientation.interval_eq_mk (a b : ℝ) [Fact (a < b)] :

interval a b = mk (OrientationLift.interval a b)

The canonical interval orientation is represented by its explicit left/right chart lift.

source

theorem TauCeti.Manifold.Orientation.orientationAt_interval (a b : ℝ) [Fact (a < b)] (x : ↑(Set.Icc a b)) :

(interval a b).orientationAt x = if ↑x < b then (EuclideanSpace.basisFun (Fin 1) ℝ).toBasis.orientation else -(EuclideanSpace.basisFun (Fin 1) ℝ).toBasis.orientation

The increasing interval orientation has positive own-chart coordinates except at the right endpoint, whose preferred half-line chart points towards decreasing real coordinates.

source

theorem TauCeti.Manifold.Orientation.map_orientationAt_interval {a b : ℝ} [hab : Fact (a < b)] (x : ↑(Set.Icc a b)) :

(Orientation.map (Fin 1) ↑(subtypeValIccTangentEquiv x)) ((interval a b).orientationAt x) = (Module.Basis.singleton (Fin 1) ℝ).orientation

Interval inclusion carries its increasing tangent orientation to the positive real orientation at every point, including both endpoints.

source

theorem TauCeti.exists_interval_tangent_bases {a b : ℝ} [Fact (a < b)] (x : ↑(Set.Icc a b)) :

∃ (B : Module.Basis (Fin 1) ℝ (EuclideanSpace ℝ (Fin 1))) (C : Module.Basis (Fin 1) ℝ (EuclideanSpace ℝ (Fin 1))), B.orientation = (Manifold.Orientation.interval a b).orientationAt x ∧ C.orientation = (-Manifold.Orientation.interval a b).orientationAt x ∧ (subtypeValIccTangentEquiv x) (B 0) = 1 ∧ (subtypeValIccTangentEquiv x) (C 0) = -1

The increasing and decreasing interval orientations admit tangent bases whose actual inclusion velocities are respectively one and minus one, including at the endpoints.

source

@[reducible]

noncomputable def TauCeti.intervalSuccessorChartedSpace {a b : ℝ} [hab : Fact (a < b)] :

ChartedSpace (EuclideanHalfSpace (0 + 1)) ↑(Set.Icc a b)

The interval charted structure, with its model dimension written as a successor so that zero-dimensional boundary constructions infer the canonical interval charts.

Instances For

source