Determinants at the boundary hyperplane

A linear map preserving the boundary hyperplane has determinant equal to its normal factor times the determinant of its restriction. This is the algebra behind outward-first orientation. The linear model orientation is characterized by prepending an outward vector, including in dimension zero.

theorem ContinuousLinearMap.det_eq_normal_mul_boundary {n : ℕ} (A : EuclideanSpace ℝ (Fin (n + 1)) →L[ℝ] EuclideanSpace ℝ (Fin (n + 1))) {a : ℝ} (hA : ∀ (v : EuclideanSpace ℝ (Fin (n + 1))), (A v).ofLp 0 = a * v.ofLp 0) : A.det = a * (TauCeti.euclideanHalfSpaceBoundaryProj n ∘SL A ∘SL TauCeti.euclideanHalfSpaceBoundaryParam n).det

The determinant splits into the normal factor and the boundary restriction determinant.

theorem EuclideanSpace.det_cons_boundary {n : ℕ} (v : EuclideanSpace ℝ (Fin (n + 1))) (w : Fin n → EuclideanSpace ℝ (Fin n)) : (basisFun (Fin (n + 1)) ℝ).toBasis.det (Fin.cons v fun (i : Fin n) => (TauCeti.euclideanHalfSpaceBoundaryParam n) (w i)) = v.ofLp 0 * (basisFun (Fin n) ℝ).toBasis.det w

The standard-basis determinant of the prepended family equals v 0 times the boundary family's standard-basis determinant.

noncomputable def Orientation.halfSpaceBoundaryOrientation {n : ℕ} (o : Orientation ℝ (EuclideanSpace ℝ (Fin (n + 1))) (Fin (n + 1))) : Orientation ℝ (EuclideanSpace ℝ (Fin n)) (Fin n)

The outward-first orientation on the coordinate-zero boundary of an oriented half-space.

@[simp]

theorem Orientation.halfSpaceBoundaryOrientation_basisFun (n : ℕ) : (EuclideanSpace.basisFun (Fin (n + 1)) ℝ).toBasis.orientation.halfSpaceBoundaryOrientation = -(EuclideanSpace.basisFun (Fin n) ℝ).toBasis.orientation

The standard positive ambient basis induces the negative standard boundary orientation, including in dimension zero.

@[simp]

theorem Orientation.halfSpaceBoundaryOrientation_neg {n : ℕ} (o : Orientation ℝ (EuclideanSpace ℝ (Fin (n + 1))) (Fin (n + 1))) : (-o).halfSpaceBoundaryOrientation = -o.halfSpaceBoundaryOrientation

Reversing the ambient model orientation reverses its boundary orientation.

theorem Orientation.halfSpaceBoundaryOrientation_spec {n : ℕ} (o : Orientation ℝ (EuclideanSpace ℝ (Fin (n + 1))) (Fin (n + 1))) {v : EuclideanSpace ℝ (Fin (n + 1))} (hv : v.ofLp 0 < 0) (b : Module.Basis (Fin n) ℝ (EuclideanSpace ℝ (Fin n))) (b' : Module.Basis (Fin (n + 1)) ℝ (EuclideanSpace ℝ (Fin (n + 1)))) (hb' : ⇑b' = Fin.cons v fun (i : Fin n) => (TauCeti.euclideanHalfSpaceBoundaryParam n) (b i)) : b.orientation = o.halfSpaceBoundaryOrientation ↔ b'.orientation = o

The boundary model orientation is characterized by placing an outward vector first.

theorem Orientation.signBasis_halfSpaceBoundaryOrientation {n : ℕ} (o : Orientation ℝ (EuclideanSpace ℝ (Fin (n + 1))) (Fin (n + 1))) : o.halfSpaceBoundaryOrientation.signBasis (EuclideanSpace.basisFun (Fin n) ℝ).toBasis = -o.signBasis (EuclideanSpace.basisFun (Fin (n + 1)) ℝ).toBasis

The actual half-space boundary orientation changes the relative standard-basis sign by minus one in every dimension, including dimension zero.