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 #
ModelWithCorners.univ_eq_interior_union_boundary:Mis the union of its interior and boundaryModelWithCorners.interior_boundary_disjoint: interior and boundary ofMare disjointBoundarylessManifold.isInteriorPoint: ifMis boundaryless, every point is an interior pointModelWithCorners.interior_prod: the interior ofM × Nis the product of the interiors ofMandN.ModelWithCorners.boundary_prod: the boundary ofM × Nis∂M × N ∪ (M × ∂N).
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
- I.IsInteriorPoint 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
- I.IsBoundaryPoint 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
- I.interior M = {x : M | I.IsInteriorPoint 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}
:
I.IsInteriorPoint 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
- I.boundary M = {x : M | I.IsBoundaryPoint 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}
:
I.IsBoundaryPoint 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)
:
I.IsInteriorPoint x ∨ I.IsBoundaryPoint x
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]
:
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]
:
Disjoint (I.interior M) (I.boundary 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 : I.IsInteriorPoint 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), I.IsInteriorPoint x
Instances
theorem
BoundarylessManifold.isInteriorPoint'
{𝕜 : 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]
[self : BoundarylessManifold I M]
(x : M)
:
I.IsInteriorPoint x
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]
[I.Boundaryless]
:
Boundaryless ModelWithCorners implies boundaryless manifold.
Equations
- ⋯ = ⋯
instance
ModelWithCorners.BoundarylessManifold.of_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]
[IsEmpty M]
:
The empty manifold is boundaryless.
Equations
- ⋯ = ⋯
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}
:
I.IsInteriorPoint x
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]
:
I.interior 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.
instance
ModelWithCorners.instIsEmptyElemBoundaryOfBoundarylessManifold
{𝕜 : 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]
:
IsEmpty ↑(I.boundary M)
Equations
- ⋯ = ⋯
theorem
ModelWithCorners.interior_prod
{𝕜 : 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]
{E' : Type u_5}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{H' : Type u_6}
[TopologicalSpace H']
{N : Type u_7}
[TopologicalSpace N]
[ChartedSpace H' N]
(J : ModelWithCorners 𝕜 E' H')
:
The interior of M × N is the product of the interiors of M and N.
theorem
ModelWithCorners.boundary_prod
{𝕜 : 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]
{E' : Type u_5}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{H' : Type u_6}
[TopologicalSpace H']
{N : Type u_7}
[TopologicalSpace N]
[ChartedSpace H' N]
(J : ModelWithCorners 𝕜 E' H')
:
The boundary of M × N is ∂M × N ∪ (M × ∂N).
theorem
boundary_of_boundaryless_left
{𝕜 : 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]
{E' : Type u_5}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{H' : Type u_6}
[TopologicalSpace H']
{N : Type u_7}
[TopologicalSpace N]
[ChartedSpace H' N]
(J : ModelWithCorners 𝕜 E' H')
[I.Boundaryless]
:
If M is boundaryless, ∂(M×N) = M × ∂N.
theorem
boundary_of_boundaryless_right
{𝕜 : 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]
{E' : Type u_5}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{H' : Type u_6}
[TopologicalSpace H']
{N : Type u_7}
[TopologicalSpace N]
[ChartedSpace H' N]
(J : ModelWithCorners 𝕜 E' H')
[J.Boundaryless]
:
If N is boundaryless, ∂(M×N) = ∂M × N.