Interior and boundary of a manifold #
Define the interior and boundary of a manifold.
Main definitions #
- IsInteriorPoint x:
p ∈ Mis an interior point if, forφbeing the preferred chart atx,φ xis an interior point ofφ.target. - IsBoundaryPoint x:
p ∈ Mis a boundary point if,(extChartAt I x) x ∈ frontier (range I). - interior I M is the interior of
M, the set of its interior points. - boundary I M is the boundary of
M, the set of its boundary points.
Main results #
univ_eq_interior_union_boundary:Mis the union of its interior and boundaryinterior_boundary_disjoint: interior and boundary ofMare disjoint- if
Mis boundaryless, every point is an interior point
Tags #
manifold, interior, boundary
TODO #
xis an interior point iff any chart aroundxmaps it tointerior (range I); similarly for the boundary.- the interior of
Mis open, hence the boundary is closed (and nowhere dense) In finite dimensions, this requires e.g. the homology of spheres. - the interior of
Mis a smooth manifold without boundary boundary Mis a smooth submanifold (possibly with boundary and corners): follows from the corresponding statement for the model with cornersI; this requires a definition of submanifolds- if
Mis finite-dimensional, its boundary has measure zero
def
ModelWithCorners.IsInteriorPoint
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_3}
[TopologicalSpace H]
(I : ModelWithCorners 𝕜 E H)
{M : Type u_4}
[TopologicalSpace M]
[ChartedSpace H M]
(x : M)
:
p ∈ M is an interior point of a manifold M iff its image in the extended chart
lies in the interior of the model space.
Equations
- ModelWithCorners.IsInteriorPoint I x = (↑(extChartAt I x) x ∈ interior (Set.range ↑I))
Instances For
def
ModelWithCorners.IsBoundaryPoint
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_3}
[TopologicalSpace H]
(I : ModelWithCorners 𝕜 E H)
{M : Type u_4}
[TopologicalSpace M]
[ChartedSpace H M]
(x : M)
:
p ∈ M is a boundary point of a manifold M iff its image in the extended chart
lies on the boundary of the model space.
Equations
- ModelWithCorners.IsBoundaryPoint I x = (↑(extChartAt I x) x ∈ frontier (Set.range ↑I))
Instances For
def
ModelWithCorners.interior
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_3}
[TopologicalSpace H]
(I : ModelWithCorners 𝕜 E H)
(M : Type u_4)
[TopologicalSpace M]
[ChartedSpace H M]
:
Set M
The interior of a manifold M is the set of its interior points.
Equations
- ModelWithCorners.interior I M = {x : M | ModelWithCorners.IsInteriorPoint I x}
Instances For
theorem
ModelWithCorners.isInteriorPoint_iff
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_3}
[TopologicalSpace H]
(I : ModelWithCorners 𝕜 E H)
{M : Type u_4}
[TopologicalSpace M]
[ChartedSpace H M]
{x : M}
:
ModelWithCorners.IsInteriorPoint I x ↔ ↑(extChartAt I x) x ∈ interior (extChartAt I x).target
def
ModelWithCorners.boundary
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_3}
[TopologicalSpace H]
(I : ModelWithCorners 𝕜 E H)
(M : Type u_4)
[TopologicalSpace M]
[ChartedSpace H M]
:
Set M
The boundary of a manifold M is the set of its boundary points.
Equations
- ModelWithCorners.boundary I M = {x : M | ModelWithCorners.IsBoundaryPoint I x}
Instances For
theorem
ModelWithCorners.isBoundaryPoint_iff
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_3}
[TopologicalSpace H]
(I : ModelWithCorners 𝕜 E H)
{M : Type u_4}
[TopologicalSpace M]
[ChartedSpace H M]
{x : M}
:
ModelWithCorners.IsBoundaryPoint I x ↔ ↑(extChartAt I x) x ∈ frontier (Set.range ↑I)
theorem
ModelWithCorners.isInteriorPoint_or_isBoundaryPoint
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_3}
[TopologicalSpace H]
(I : ModelWithCorners 𝕜 E H)
{M : Type u_4}
[TopologicalSpace M]
[ChartedSpace H M]
(x : M)
:
Every point is either an interior or a boundary point.
theorem
ModelWithCorners.interior_union_boundary_eq_univ
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_3}
[TopologicalSpace H]
(I : ModelWithCorners 𝕜 E H)
{M : Type u_4}
[TopologicalSpace M]
[ChartedSpace H M]
:
ModelWithCorners.interior I M ∪ ModelWithCorners.boundary I M = Set.univ
A manifold decomposes into interior and boundary.
theorem
ModelWithCorners.disjoint_interior_boundary
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_3}
[TopologicalSpace H]
(I : ModelWithCorners 𝕜 E H)
{M : Type u_4}
[TopologicalSpace M]
[ChartedSpace H M]
:
The interior and boundary of a manifold M are disjoint.
theorem
ModelWithCorners.boundary_eq_complement_interior
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_3}
[TopologicalSpace H]
(I : ModelWithCorners 𝕜 E H)
{M : Type u_4}
[TopologicalSpace M]
[ChartedSpace H M]
:
The boundary is the complement of the interior.
theorem
range_mem_nhds_isInteriorPoint
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_3}
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
{M : Type u_4}
[TopologicalSpace M]
[ChartedSpace H M]
{x : M}
(h : ModelWithCorners.IsInteriorPoint I x)
:
Set.range ↑I ∈ nhds (↑(extChartAt I x) x)
class
BoundarylessManifold
{𝕜 : Type u_5}
[NontriviallyNormedField 𝕜]
{E : Type u_6}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_7}
[TopologicalSpace H]
(I : ModelWithCorners 𝕜 E H)
(M : Type u_8)
[TopologicalSpace M]
[ChartedSpace H M]
:
Type class for manifold without boundary. This differs from ModelWithCorners.Boundaryless,
which states that the ModelWithCorners maps to the whole model vector space.
- isInteriorPoint' : ∀ (x : M), ModelWithCorners.IsInteriorPoint I x
Instances
instance
ModelWithCorners.instBoundarylessManifold
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_3}
[TopologicalSpace H]
(I : ModelWithCorners 𝕜 E H)
{M : Type u_4}
[TopologicalSpace M]
[ChartedSpace H M]
[ModelWithCorners.Boundaryless I]
:
Boundaryless ModelWithCorners implies boundaryless manifold.
Equations
- (_ : BoundarylessManifold I M) = (_ : BoundarylessManifold I M)
theorem
BoundarylessManifold.isInteriorPoint
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_3}
[TopologicalSpace H]
(I : ModelWithCorners 𝕜 E H)
{M : Type u_4}
[TopologicalSpace M]
[ChartedSpace H M]
[BoundarylessManifold I M]
{x : M}
:
theorem
ModelWithCorners.interior_eq_univ
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_3}
[TopologicalSpace H]
(I : ModelWithCorners 𝕜 E H)
{M : Type u_4}
[TopologicalSpace M]
[ChartedSpace H M]
[BoundarylessManifold I M]
:
ModelWithCorners.interior I M = Set.univ
If I is boundaryless, M has full interior.
theorem
ModelWithCorners.Boundaryless.boundary_eq_empty
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_3}
[TopologicalSpace H]
(I : ModelWithCorners 𝕜 E H)
{M : Type u_4}
[TopologicalSpace M]
[ChartedSpace H M]
[BoundarylessManifold I M]
:
Boundaryless manifolds have empty boundary.