Interior and boundary of a manifold

Define the interior and boundary of a manifold.

Main definitions

• IsInteriorPoint x: p ∈ M is an interior point if, for φ being the preferred chart at x, φ x is an interior point of φ.target.
• IsBoundaryPoint x: p ∈ M is 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: M is the union of its interior and boundary
• interior_boundary_disjoint: interior and boundary of M are disjoint
• if M is boundaryless, every point is an interior point

Tags

manifold, interior, boundary

TODO

• x is an interior point iff any chart around x maps it to interior (range I); similarly for the boundary.
• the interior of M is open, hence the boundary is closed (and nowhere dense) In finite dimensions, this requires e.g. the homology of spheres.
• the interior of M is a smooth manifold without boundary
• boundary M is a smooth submanifold (possibly with boundary and corners): follows from the corresponding statement for the model with corners I; this requires a definition of submanifolds
• if M is 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) : Prop

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))

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) : Prop

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))

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}

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}

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] : I.interior M ∪ I.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] : 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] : I.boundary M = (I.interior 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] : Prop

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

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] : BoundarylessManifold I M

Boundaryless ModelWithCorners implies boundaryless manifold.

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] : I.boundary M = ∅

Boundaryless manifolds have empty boundary.