The induced boundary orientation

The normal coordinate of a half-space transition has strictly positive derivative. Restricting chart signs therefore constructs the actual boundary orientation. The model orientation uses the outward-first convention, so the standard ambient orientation induces the negative standard orientation on the coordinate-zero boundary, including a zero-dimensional boundary.

The outward-first rule can be read in another manifold of the same dimension: if a map φ preserves orientations at a boundary point x, then an oriented boundary basis at x, carried by dφ and preceded by the image of an outward vector, is oriented in the target (TauCeti.boundaryOrientation_spec_of_isOrientationPreservingAt). This applies to the inclusion of a regular domain into an oriented manifold, with the pulled-back orientation.

On the zero-dimensional boundary of a one-manifold, the induced orientation at a point is a sign Orientation.signBasis against a basis indexed by Fin 0. That sign is 1 exactly when an outward tangent vector is positively oriented, and -1 exactly when it is negatively oriented (TauCeti.signBasis_orientationAt_boundaryOrientation_eq_one_iff, TauCeti.signBasis_orientationAt_boundaryOrientation_eq_neg_one_iff).

theorem TauCeti.Manifold.OrientationLift.instIsManifoldRealEuclideanSpaceFinModelWithCornersSelfOfNatWithTopENatElemBoundaryHAddNatEuclideanHalfSpace {n : ℕ} {M : Type u_1} [TopologicalSpace M] [ChartedSpace (EuclideanHalfSpace (n + 1)) M] [IsManifold (modelWithCornersEuclideanHalfSpace (n + 1)) 1 M] : IsManifold (modelWithCornersSelf ℝ (EuclideanSpace ℝ (Fin n))) 1 ↑(ModelWithCorners.boundary M)

noncomputable def TauCeti.Manifold.OrientationLift.boundary {n : ℕ} {M : Type u_1} [TopologicalSpace M] [ChartedSpace (EuclideanHalfSpace (n + 1)) M] [IsManifold (modelWithCornersEuclideanHalfSpace (n + 1)) 1 M] (l : OrientationLift (modelWithCornersEuclideanHalfSpace (n + 1)) M (Fin (n + 1))) : OrientationLift (modelWithCornersSelf ℝ (EuclideanSpace ℝ (Fin n))) (↑(ModelWithCorners.boundary M)) (Fin n)

Restriction of the source signs to boundary charts, with the outward-first model orientation.

@[simp]

theorem TauCeti.Manifold.OrientationLift.boundary_modelOrientation {n : ℕ} {M : Type u_1} [TopologicalSpace M] [ChartedSpace (EuclideanHalfSpace (n + 1)) M] [IsManifold (modelWithCornersEuclideanHalfSpace (n + 1)) 1 M] (l : OrientationLift (modelWithCornersEuclideanHalfSpace (n + 1)) M (Fin (n + 1))) : l.boundary.modelOrientation = l.modelOrientation.halfSpaceBoundaryOrientation

The boundary lift uses the outward-first model orientation.

@[simp]

theorem TauCeti.Manifold.OrientationLift.boundary_sign {n : ℕ} {M : Type u_1} [TopologicalSpace M] [ChartedSpace (EuclideanHalfSpace (n + 1)) M] [IsManifold (modelWithCornersEuclideanHalfSpace (n + 1)) 1 M] (l : OrientationLift (modelWithCornersEuclideanHalfSpace (n + 1)) M (Fin (n + 1))) (α : ↑(ModelWithCorners.boundary M)) (x : ↑(chartAt (EuclideanSpace ℝ (Fin n)) α).source) : l.boundary.sign α x = l.sign ↑α ⟨↑↑x, ⋯⟩

The boundary lift restricts the actual ambient source-indexed signs.

@[simp]

theorem TauCeti.Manifold.OrientationLift.boundary_flip {n : ℕ} {M : Type u_1} [TopologicalSpace M] [ChartedSpace (EuclideanHalfSpace (n + 1)) M] [IsManifold (modelWithCornersEuclideanHalfSpace (n + 1)) 1 M] (l : OrientationLift (modelWithCornersEuclideanHalfSpace (n + 1)) M (Fin (n + 1))) : l.flip.boundary = l.boundary.flip

Diagonal reversal commutes with passage to the boundary lift.

theorem TauCeti.instIsManifoldRealEuclideanSpaceFinModelWithCornersSelfOfNatWithTopENatElemBoundaryHAddNatEuclideanHalfSpace_tauCeti_1 {n : ℕ} {M : Type u_1} [TopologicalSpace M] [ChartedSpace (EuclideanHalfSpace (n + 1)) M] [IsManifold (modelWithCornersEuclideanHalfSpace (n + 1)) 1 M] : IsManifold (modelWithCornersSelf ℝ (EuclideanSpace ℝ (Fin n))) 1 ↑(ModelWithCorners.boundary M)

noncomputable def TauCeti.boundaryOrientation {n : ℕ} {M : Type u_1} [TopologicalSpace M] [ChartedSpace (EuclideanHalfSpace (n + 1)) M] [IsManifold (modelWithCornersEuclideanHalfSpace (n + 1)) 1 M] (o : Manifold.Orientation (modelWithCornersEuclideanHalfSpace (n + 1)) M (Fin (n + 1))) : Manifold.Orientation (modelWithCornersSelf ℝ (EuclideanSpace ℝ (Fin n))) (↑(ModelWithCorners.boundary M)) (Fin n)

The canonical boundary orientation, with the outward vector first.

@[simp]

theorem TauCeti.boundaryOrientation_mk {n : ℕ} {M : Type u_1} [TopologicalSpace M] [ChartedSpace (EuclideanHalfSpace (n + 1)) M] [IsManifold (modelWithCornersEuclideanHalfSpace (n + 1)) 1 M] (l : Manifold.OrientationLift (modelWithCornersEuclideanHalfSpace (n + 1)) M (Fin (n + 1))) : boundaryOrientation (Manifold.Orientation.mk l) = Manifold.Orientation.mk l.boundary

Passage to the boundary orientation is independent of the chosen representative lift.

theorem TauCeti.boundaryOrientation_spec {n : ℕ} {M : Type u_1} [TopologicalSpace M] [ChartedSpace (EuclideanHalfSpace (n + 1)) M] [IsManifold (modelWithCornersEuclideanHalfSpace (n + 1)) 1 M] (o : Manifold.Orientation (modelWithCornersEuclideanHalfSpace (n + 1)) M (Fin (n + 1))) (x : ↑(ModelWithCorners.boundary M)) {v : TangentSpace (modelWithCornersEuclideanHalfSpace (n + 1)) ↑x} (hv : IsOutwardPointing (↑x) v) (b : Module.Basis (Fin n) ℝ (TangentSpace (modelWithCornersSelf ℝ (EuclideanSpace ℝ (Fin n))) x)) (b' : Module.Basis (Fin (n + 1)) ℝ (TangentSpace (modelWithCornersEuclideanHalfSpace (n + 1)) ↑x)) (hb' : ⇑b' = Fin.cons v fun (i : Fin n) => (mfderiv% Subtype.val x) (b i)) : b.orientation = (boundaryOrientation o).orientationAt x ↔ b'.orientation = o.orientationAt ↑x

Outward-first: an oriented boundary basis preceded by any outward vector is oriented for the ambient manifold. This characterization includes zero-dimensional boundaries.

theorem TauCeti.orientationAt_boundaryOrientation {n : ℕ} {M : Type u_1} [TopologicalSpace M] [ChartedSpace (EuclideanHalfSpace (n + 1)) M] [IsManifold (modelWithCornersEuclideanHalfSpace (n + 1)) 1 M] (o : Manifold.Orientation (modelWithCornersEuclideanHalfSpace (n + 1)) M (Fin (n + 1))) (x : ↑(ModelWithCorners.boundary M)) : (boundaryOrientation o).orientationAt x = (o.orientationAt ↑x).halfSpaceBoundaryOrientation

The induced boundary orientation at each point is the outward-first half-space orientation.

@[simp]

theorem TauCeti.boundaryOrientation_neg {n : ℕ} {M : Type u_1} [TopologicalSpace M] [ChartedSpace (EuclideanHalfSpace (n + 1)) M] [IsManifold (modelWithCornersEuclideanHalfSpace (n + 1)) 1 M] (o : Manifold.Orientation (modelWithCornersEuclideanHalfSpace (n + 1)) M (Fin (n + 1))) : boundaryOrientation (-o) = -boundaryOrientation o

Reversing the ambient orientation reverses the induced boundary orientation.

theorem TauCeti.orientationAt_boundaryOrientation_model (n : ℕ) (x : ↑(ModelWithCorners.boundary (EuclideanHalfSpace (n + 1)))) : (boundaryOrientation (Manifold.Orientation.model (EuclideanSpace.basisFun (Fin (n + 1)) ℝ).toBasis.orientation ⋯)).orientationAt x = -(EuclideanSpace.basisFun (Fin n) ℝ).toBasis.orientation

The standard half-space orientation induces the negative standard orientation on its coordinate-zero boundary. The formula also applies to the zero-dimensional boundary of a ray.

theorem TauCeti.boundaryOrientation_spec_of_isOrientationPreservingAt {n : ℕ} {M : Type u_1} [TopologicalSpace M] [ChartedSpace (EuclideanHalfSpace (n + 1)) M] [IsManifold (modelWithCornersEuclideanHalfSpace (n + 1)) 1 M] {E : Type u_2} {H : Type u_3} {M' : Type u_4} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] {I : ModelWithCorners ℝ E H} [FiniteDimensional ℝ E] [TopologicalSpace M'] [ChartedSpace H M'] [IsManifold I 1 M'] {o : Manifold.Orientation (modelWithCornersEuclideanHalfSpace (n + 1)) M (Fin (n + 1))} {o' : Manifold.Orientation I M' (Fin (n + 1))} {φ : M → M'} (x : ↑(ModelWithCorners.boundary M)) (hφ : o.IsOrientationPreservingAt o' φ ↑x) {v : TangentSpace (modelWithCornersEuclideanHalfSpace (n + 1)) ↑x} (hv : IsOutwardPointing (↑x) v) (b : Module.Basis (Fin n) ℝ (TangentSpace (modelWithCornersSelf ℝ (EuclideanSpace ℝ (Fin n))) x)) (b' : Module.Basis (Fin (n + 1)) ℝ (TangentSpace I (φ ↑x))) (hb' : ⇑b' = Fin.cons ((mfderiv% φ ↑x) v) fun (i : Fin n) => ((mfderiv% fun (y : ↑(ModelWithCorners.boundary M)) => φ ↑y) x) (b i)) : b.orientation = (boundaryOrientation o).orientationAt x ↔ b'.orientation = o'.orientationAt (φ ↑x)

Outward-first in an ambient manifold. Let φ map a manifold with boundary M to a manifold M' of the same dimension, preserving orientations at a boundary point x, for instance the inclusion of a regular domain with the pulled-back orientation. Then an oriented basis of the boundary at x, carried into M' and preceded by the image under dφ of an outward vector, is oriented for M'.

theorem TauCeti.instIsManifoldRealEuclideanSpaceFinOfNatNatModelWithCornersSelfWithTopENatElemBoundaryHAddEuclideanHalfSpace_tauCeti {M : Type u_1} [TopologicalSpace M] [ChartedSpace (EuclideanHalfSpace (0 + 1)) M] [IsManifold (modelWithCornersEuclideanHalfSpace (0 + 1)) 1 M] : IsManifold (modelWithCornersSelf ℝ (EuclideanSpace ℝ (Fin 0))) 1 ↑(ModelWithCorners.boundary M)

theorem TauCeti.signBasis_orientationAt_boundaryOrientation_eq_one_iff {M : Type u_1} [TopologicalSpace M] [ChartedSpace (EuclideanHalfSpace (0 + 1)) M] [IsManifold (modelWithCornersEuclideanHalfSpace (0 + 1)) 1 M] (o : Manifold.Orientation (modelWithCornersEuclideanHalfSpace (0 + 1)) M (Fin 1)) (x : ↑(ModelWithCorners.boundary M)) {v : TangentSpace (modelWithCornersEuclideanHalfSpace (0 + 1)) ↑x} (hv : IsOutwardPointing (↑x) v) (b : Module.Basis (Fin 1) ℝ (TangentSpace (modelWithCornersEuclideanHalfSpace (0 + 1)) ↑x)) (hb : b 0 = v) (e : Module.Basis (Fin 0) ℝ (TangentSpace (modelWithCornersSelf ℝ (EuclideanSpace ℝ (Fin 0))) x)) : ((boundaryOrientation o).orientationAt x).signBasis e = 1 ↔ b.orientation = o.orientationAt ↑x

The boundary sign at x, read against any basis e of the zero-dimensional tangent space, is 1 exactly when an outward tangent vector at x, taken as a basis of the tangent line, is positively oriented.

theorem TauCeti.signBasis_orientationAt_boundaryOrientation_eq_neg_one_iff {M : Type u_1} [TopologicalSpace M] [ChartedSpace (EuclideanHalfSpace (0 + 1)) M] [IsManifold (modelWithCornersEuclideanHalfSpace (0 + 1)) 1 M] (o : Manifold.Orientation (modelWithCornersEuclideanHalfSpace (0 + 1)) M (Fin 1)) (x : ↑(ModelWithCorners.boundary M)) {v : TangentSpace (modelWithCornersEuclideanHalfSpace (0 + 1)) ↑x} (hv : IsOutwardPointing (↑x) v) (b : Module.Basis (Fin 1) ℝ (TangentSpace (modelWithCornersEuclideanHalfSpace (0 + 1)) ↑x)) (hb : b 0 = v) (e : Module.Basis (Fin 0) ℝ (TangentSpace (modelWithCornersSelf ℝ (EuclideanSpace ℝ (Fin 0))) x)) : ((boundaryOrientation o).orientationAt x).signBasis e = -1 ↔ b.orientation = -o.orientationAt ↑x

The boundary sign at x, read against any basis e of the zero-dimensional tangent space, is -1 exactly when an outward tangent vector at x, taken as a basis of the tangent line, is negatively oriented.