Documentation

TauCeti.Geometry.Manifold.Boundary.Charts

The boundary of a manifold with boundary is a manifold #

Mathlib carries the boundary I.boundary M of a manifold with boundary only as a set: there is no manifold structure on it, so nothing can be glued along it. This file supplies that structure in the basic Euclidean half-space case: M is a C^k manifold, k โ‰  0, modeled on the (n + 1)- dimensional Euclidean half-space ๐“กโˆ‚ (n + 1), and its boundary becomes a boundaryless C^k manifold modeled on EuclideanSpace โ„ (Fin n), one dimension lower, whose inclusion into M is a C^k closed embedding.

The boundary atlas consists of charts induced by the preferred ambient charts. Each preferred ambient chart carries a boundary point to a point of the half-space whose zeroth coordinate vanishes; deleting that coordinate turns it into a preferred chart of the boundary. Two facts make this work, and they are the content of the file.

The charted-space structure depends only on the ambient C^1 structure and is registered as the canonical instance. The manifold and embedding results remain valid for every exponent k โ‰  0. Boundarylessness then follows directly from ModelWithCorners.Boundaryless.boundary_eq_empty.

Corners are deliberately out of scope: gluing along a piece of the boundary produces corners, and the quadrant model modelWithCornersEuclideanQuadrant needs its own boundary analysis. Collar neighbourhoods, which are what make a gluing smooth rather than merely topological, are the next step and are not proved here.

Main definitions #

Main results #

References #

source
theorem TauCeti.ModelWithCorners.isInteriorPoint_euclideanHalfSpace_iff_of_mem_maximalAtlas {d : โ„•} [NeZero d] {k : WithTop โ„•โˆž} {M : Type u_1} [TopologicalSpace M] [ChartedSpace (EuclideanHalfSpace d) M] (hk : k โ‰  0) {e : OpenPartialHomeomorph M (EuclideanHalfSpace d)} (he : e โˆˆ IsManifold.maximalAtlas (modelWithCornersEuclideanHalfSpace d) k M) {x : M} (hx : x โˆˆ e.source) :
(modelWithCornersEuclideanHalfSpace d).IsInteriorPoint x โ†” 0 < (โ†‘(โ†‘e x)).ofLp 0

A point of a charted space modeled on the d-dimensional Euclidean half-space is an interior point exactly when any chart of its C^k maximal atlas, k โ‰  0, around it reads it with positive zeroth coordinate.

source
theorem TauCeti.ModelWithCorners.mem_boundary_euclideanHalfSpace_iff_of_mem_atlas {n : โ„•} {k : WithTop โ„•โˆž} {M : Type u_1} [TopologicalSpace M] [ChartedSpace (EuclideanHalfSpace (n + 1)) M] [IsManifold (modelWithCornersEuclideanHalfSpace (n + 1)) k M] {e : OpenPartialHomeomorph M (EuclideanHalfSpace (n + 1))} {x : M} (hk : k โ‰  0) (he : e โˆˆ atlas (EuclideanHalfSpace (n + 1)) M) (hx : x โˆˆ e.source) :
x โˆˆ ModelWithCorners.boundary M โ†” (โ†‘(โ†‘e x)).ofLp 0 = 0

A point of a C^k manifold with boundary modeled on the (n + 1)-dimensional Euclidean half-space lies on the boundary exactly when any chart around it reads it with vanishing zeroth coordinate.

source
@[irreducible]
noncomputable instance TauCeti.boundaryChartedSpace {n : โ„•} {M : Type u_1} [TopologicalSpace M] [ChartedSpace (EuclideanHalfSpace (n + 1)) M] [IsManifold (modelWithCornersEuclideanHalfSpace (n + 1)) 1 M] :
ChartedSpace (EuclideanSpace โ„ (Fin n)) โ†‘(ModelWithCorners.boundary M)

The canonical charted-space structure on the boundary of a C^1 manifold modeled on a Euclidean half-space. Its atlas consists of the boundary charts induced by the ambient preferred charts. The implementation is intentionally opaque; use the characteristic lemmas below to reason about its atlas and preferred charts.

Equations
  • One or more equations did not get rendered due to their size.
source
theorem TauCeti.boundaryChartedSpace_atlas {n : โ„•} (M : Type u_1) [TopologicalSpace M] [ChartedSpace (EuclideanHalfSpace (n + 1)) M] [IsManifold (modelWithCornersEuclideanHalfSpace (n + 1)) 1 M] :
atlas (EuclideanSpace โ„ (Fin n)) โ†‘(ModelWithCorners.boundary M) = Set.range fun (p : โ†‘(ModelWithCorners.boundary M)) => chartAt (EuclideanSpace โ„ (Fin n)) p

The boundary atlas is the range of its preferred charts.

source
theorem TauCeti.boundaryChartedSpace_chartAt_source {n : โ„•} (M : Type u_1) [TopologicalSpace M] [ChartedSpace (EuclideanHalfSpace (n + 1)) M] [IsManifold (modelWithCornersEuclideanHalfSpace (n + 1)) 1 M] (p : โ†‘(ModelWithCorners.boundary M)) :
(chartAt (EuclideanSpace โ„ (Fin n)) p).source = Subtype.val โปยน' (chartAt (EuclideanHalfSpace (n + 1)) โ†‘p).source

The source of the preferred boundary chart at p is the part of the boundary the ambient preferred chart at p sees.

source
theorem TauCeti.boundaryChartedSpace_chartAt_target {n : โ„•} (M : Type u_1) [TopologicalSpace M] [ChartedSpace (EuclideanHalfSpace (n + 1)) M] [IsManifold (modelWithCornersEuclideanHalfSpace (n + 1)) 1 M] (p : โ†‘(ModelWithCorners.boundary M)) :
(chartAt (EuclideanSpace โ„ (Fin n)) p).target = EuclideanHalfSpace.boundaryParam n โปยน' (chartAt (EuclideanHalfSpace (n + 1)) โ†‘p).target

The target of the preferred boundary chart at p is the ambient target, pulled back to the coordinate hyperplane.

source
theorem TauCeti.boundaryChartedSpace_chartAt_apply {n : โ„•} (M : Type u_1) [TopologicalSpace M] [ChartedSpace (EuclideanHalfSpace (n + 1)) M] [IsManifold (modelWithCornersEuclideanHalfSpace (n + 1)) 1 M] (p q : โ†‘(ModelWithCorners.boundary M)) :
โ†‘(chartAt (EuclideanSpace โ„ (Fin n)) p) q = EuclideanHalfSpace.boundaryProj n (โ†‘(chartAt (EuclideanHalfSpace (n + 1)) โ†‘p) โ†‘q)

The preferred boundary chart at p reads a point through the ambient preferred chart at p and deletes the zeroth coordinate.

source
theorem TauCeti.boundaryChartedSpace_chartAt_symm_apply {n : โ„•} (M : Type u_1) [TopologicalSpace M] [ChartedSpace (EuclideanHalfSpace (n + 1)) M] [IsManifold (modelWithCornersEuclideanHalfSpace (n + 1)) 1 M] (p : โ†‘(ModelWithCorners.boundary M)) {z : EuclideanSpace โ„ (Fin n)} (hz : EuclideanHalfSpace.boundaryParam n z โˆˆ (chartAt (EuclideanHalfSpace (n + 1)) โ†‘p).target) :
โ†‘(โ†‘(chartAt (EuclideanSpace โ„ (Fin n)) p).symm z) = โ†‘(chartAt (EuclideanHalfSpace (n + 1)) โ†‘p).symm (EuclideanHalfSpace.boundaryParam n z)

On its target, the inverse of the preferred boundary chart at p is the inverse of the ambient preferred chart at p, applied to the parametrized point.

source
theorem TauCeti.isManifold_boundary {n : โ„•} {k : WithTop โ„•โˆž} (M : Type u_1) [TopologicalSpace M] [ChartedSpace (EuclideanHalfSpace (n + 1)) M] [IsManifold (modelWithCornersEuclideanHalfSpace (n + 1)) k M] (hk : k โ‰  0) :
have x := โ‹ฏ; IsManifold (modelWithCornersSelf โ„ (EuclideanSpace โ„ (Fin n))) k โ†‘(ModelWithCorners.boundary M)

The boundary of a C^k manifold with boundary is a C^k manifold of dimension one less: the transition maps between the boundary charts are C^k.

source
theorem TauCeti.isImmersion_subtypeVal_boundary {n : โ„•} {k : WithTop โ„•โˆž} (M : Type u_1) [TopologicalSpace M] [ChartedSpace (EuclideanHalfSpace (n + 1)) M] [IsManifold (modelWithCornersEuclideanHalfSpace (n + 1)) k M] (hk : k โ‰  0) :
have x := โ‹ฏ; Manifold.IsImmersion (modelWithCornersSelf โ„ (EuclideanSpace โ„ (Fin n))) (modelWithCornersEuclideanHalfSpace (n + 1)) k Subtype.val

The inclusion of the boundary into the manifold is a C^k immersion. In the preferred boundary and ambient charts it is the coordinate inclusion with one-dimensional complement.

source
theorem TauCeti.isSmoothEmbedding_subtypeVal_boundary {n : โ„•} {k : WithTop โ„•โˆž} (M : Type u_1) [TopologicalSpace M] [ChartedSpace (EuclideanHalfSpace (n + 1)) M] [IsManifold (modelWithCornersEuclideanHalfSpace (n + 1)) k M] (hk : k โ‰  0) :
have x := โ‹ฏ; Manifold.IsSmoothEmbedding (modelWithCornersSelf โ„ (EuclideanSpace โ„ (Fin n))) (modelWithCornersEuclideanHalfSpace (n + 1)) k Subtype.val

The inclusion of the boundary into the manifold is a C^k smooth embedding.