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

• ModelWithCorners.univ_eq_interior_union_boundary: M is the union of its interior and boundary
• ModelWithCorners.interior_boundary_disjoint: interior and boundary of M are disjoint
• BoundarylessManifold.isInteriorPoint: if M is boundaryless, every point is an interior point
• ModelWithCorners.Boundaryless.boundary_eq_empty and of_boundary_eq_empty: M is boundaryless if and only if its boundary is empty
• ModelWithCorners.interior_prod: the interior of M × N is the product of the interiors of M and N.
• ModelWithCorners.boundary_prod: the boundary of M × N is ∂M × N ∪ (M × ∂N).
• ModelWithCorners.BoundarylessManifold.prod: if M and N are boundaryless, so is M × N

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

• ⋯ = ⋯

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

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.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] : I.boundary M = ∅ ↔ BoundarylessManifold I 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 : I.boundary M = ∅) : BoundarylessManifold I 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') : (I.prod J).interior (M × N) = I.interior M ×ˢ J.interior N

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') : (I.prod J).boundary (M × N) = Set.univ.prod (J.boundary N) ∪ (I.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] : (I.prod J).boundary (M × N) = Set.univ.prod (J.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] : (I.prod J).boundary (M × N) = (I.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

• ⋯ = ⋯