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.Boundaryless.boundary_eq_emptyandof_boundary_eq_empty:Mis boundaryless if and only if its boundary is emptyModelWithCorners.interior_prod: the interior ofM × Nis the product of the interiors ofMandN.ModelWithCorners.boundary_prod: the boundary ofM × Nis∂M × N ∪ (M × ∂N).ModelWithCorners.BoundarylessManifold.prod: ifMandNare boundaryless, so isM × 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
- ModelWithCorners.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
- ModelWithCorners.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]
:
ModelWithCorners.interior M ∪ ModelWithCorners.boundary 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.compl_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
ModelWithCorners.compl_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 is the complement of the boundary.
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}
:
∀ {inst : NontriviallyNormedField 𝕜} {E : Type u_6} {inst_1 : NormedAddCommGroup E} {inst_2 : NormedSpace 𝕜 E}
{H : Type u_7} {inst_3 : TopologicalSpace H} {I : ModelWithCorners 𝕜 E H} {M : Type u_8} {inst_4 : TopologicalSpace M}
{inst_5 : 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]
{x : M}
[BoundarylessManifold I 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]
:
ModelWithCorners.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]
:
Equations
- ⋯ = ⋯
theorem
ModelWithCorners.Boundaryless.iff_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]
:
M is boundaryless iff its boundary is empty.
theorem
ModelWithCorners.Boundaryless.of_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]
(h : ModelWithCorners.boundary M = ∅)
:
Manifolds with empty boundary are boundaryless.
Interior and boundary of the product of two manifolds.
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'}
:
ModelWithCorners.boundary (M × N) = Set.univ.prod (ModelWithCorners.boundary N) ∪ (ModelWithCorners.boundary M).prod Set.univ
The boundary of M × N is ∂M × N ∪ (M × ∂N).
theorem
ModelWithCorners.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'}
[BoundarylessManifold I M]
:
ModelWithCorners.boundary (M × N) = Set.univ.prod (ModelWithCorners.boundary N)
If M is boundaryless, ∂(M×N) = M × ∂N.
theorem
ModelWithCorners.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'}
[BoundarylessManifold J N]
:
ModelWithCorners.boundary (M × N) = (ModelWithCorners.boundary M).prod Set.univ
If N is boundaryless, ∂(M×N) = ∂M × N.
instance
ModelWithCorners.BoundarylessManifold.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'}
[BoundarylessManifold I M]
[BoundarylessManifold J N]
:
BoundarylessManifold (I.prod J) (M × N)
The product of two boundaryless manifolds is boundaryless.
Equations
- ⋯ = ⋯