Tangent maps of boundary charts #
The boundary inclusion is the coordinate hyperplane parametrization in the preferred charts. Its manifold derivative is therefore the actual zero-insertion linear map.
theorem
TauCeti.instIsManifoldRealEuclideanSpaceFinModelWithCornersSelfOfNatWithTopENatElemBoundaryHAddNatEuclideanHalfSpace_tauCeti
{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)
theorem
TauCeti.boundaryParam_mem_extChartAt_target_iff
{n : ℕ}
{M : Type u_1}
[TopologicalSpace M]
[ChartedSpace (EuclideanHalfSpace (n + 1)) M]
[IsManifold (modelWithCornersEuclideanHalfSpace (n + 1)) 1 M]
(α : ↑(ModelWithCorners.boundary M))
(y : EuclideanSpace ℝ (Fin n))
:
(euclideanHalfSpaceBoundaryParam n) y ∈ (extChartAt (modelWithCornersEuclideanHalfSpace (n + 1)) ↑α).target ↔ y ∈ (extChartAt (modelWithCornersSelf ℝ (EuclideanSpace ℝ (Fin n))) α).target
The boundary chart target is exactly the zero-coordinate slice of the ambient target.
theorem
TauCeti.boundaryParam_extChartAt
{n : ℕ}
{M : Type u_1}
[TopologicalSpace M]
[ChartedSpace (EuclideanHalfSpace (n + 1)) M]
[IsManifold (modelWithCornersEuclideanHalfSpace (n + 1)) 1 M]
{α x : ↑(ModelWithCorners.boundary M)}
(hα : x ∈ (extChartAt (modelWithCornersSelf ℝ (EuclideanSpace ℝ (Fin n))) α).source)
:
(euclideanHalfSpaceBoundaryParam n) (↑(extChartAt (modelWithCornersSelf ℝ (EuclideanSpace ℝ (Fin n))) α) x) = ↑(extChartAt (modelWithCornersEuclideanHalfSpace (n + 1)) ↑α) ↑x
Inserting the missing zero coordinate of a boundary chart recovers its ambient chart.
theorem
TauCeti.mfderiv_subtypeVal_boundary
{n : ℕ}
{M : Type u_1}
[TopologicalSpace M]
[ChartedSpace (EuclideanHalfSpace (n + 1)) M]
[IsManifold (modelWithCornersEuclideanHalfSpace (n + 1)) 1 M]
(x : ↑(ModelWithCorners.boundary M))
:
The inclusion of the boundary has the coordinate zero-insertion map as its manifold derivative in the canonical preferred charts.
theorem
TauCeti.tangentCoordChange_boundary
{n : ℕ}
{M : Type u_1}
[TopologicalSpace M]
[ChartedSpace (EuclideanHalfSpace (n + 1)) M]
[IsManifold (modelWithCornersEuclideanHalfSpace (n + 1)) 1 M]
{α β x : ↑(ModelWithCorners.boundary M)}
(hα : x ∈ (extChartAt (modelWithCornersSelf ℝ (EuclideanSpace ℝ (Fin n))) α).source)
(hβ : x ∈ (extChartAt (modelWithCornersSelf ℝ (EuclideanSpace ℝ (Fin n))) β).source)
:
tangentCoordChange (modelWithCornersSelf ℝ (EuclideanSpace ℝ (Fin n))) α β x = euclideanHalfSpaceBoundaryProj n ∘SL tangentCoordChange (modelWithCornersEuclideanHalfSpace (n + 1)) ↑α ↑β ↑x ∘SL euclideanHalfSpaceBoundaryParam n
Boundary transition derivatives are the ambient transition derivatives restricted to the coordinate hyperplane and then projected back to boundary coordinates.
theorem
TauCeti.tangentCoordChange_boundaryParam
{n : ℕ}
{M : Type u_1}
[TopologicalSpace M]
[ChartedSpace (EuclideanHalfSpace (n + 1)) M]
[IsManifold (modelWithCornersEuclideanHalfSpace (n + 1)) 1 M]
{α β x : ↑(ModelWithCorners.boundary M)}
(hα : x ∈ (extChartAt (modelWithCornersSelf ℝ (EuclideanSpace ℝ (Fin n))) α).source)
(hβ : x ∈ (extChartAt (modelWithCornersSelf ℝ (EuclideanSpace ℝ (Fin n))) β).source)
:
tangentCoordChange (modelWithCornersEuclideanHalfSpace (n + 1)) ↑α ↑β ↑x ∘SL euclideanHalfSpaceBoundaryParam n = euclideanHalfSpaceBoundaryParam n ∘SL tangentCoordChange (modelWithCornersSelf ℝ (EuclideanSpace ℝ (Fin n))) α β x
Boundary transition maps intertwine zero insertion with the ambient transition maps.
theorem
TauCeti.exists_pos_det_tangentCoordChange_boundary
{n : ℕ}
{M : Type u_1}
[TopologicalSpace M]
[ChartedSpace (EuclideanHalfSpace (n + 1)) M]
[IsManifold (modelWithCornersEuclideanHalfSpace (n + 1)) 1 M]
{α β x : ↑(ModelWithCorners.boundary M)}
(hα : x ∈ (extChartAt (modelWithCornersSelf ℝ (EuclideanSpace ℝ (Fin n))) α).source)
(hβ : x ∈ (extChartAt (modelWithCornersSelf ℝ (EuclideanSpace ℝ (Fin n))) β).source)
:
∃ a > 0,
(tangentCoordChange (modelWithCornersEuclideanHalfSpace (n + 1)) ↑α ↑β ↑x).det = a * (tangentCoordChange (modelWithCornersSelf ℝ (EuclideanSpace ℝ (Fin n))) α β x).det
Ambient and boundary transition determinants differ by a strictly positive normal factor.