Constructing examples of manifolds over ℝ

We introduce the necessary bits to be able to define manifolds modelled over ℝ^n, boundaryless or with boundary or with corners. As a concrete example, we construct explicitly the manifold with boundary structure on the real interval [x, y], and prove that its boundary is indeed {x, y} whenever x < y. As a corollary, a product M × [x, y] with a manifold M without boundary has boundary M × {x, y}.

More specifically, we introduce

• modelWithCornersEuclideanHalfSpace n : ModelWithCorners ℝ (EuclideanSpace ℝ (Fin n)) (EuclideanHalfSpace n) for the model space used to define n-dimensional real manifolds with boundary
• modelWithCornersEuclideanQuadrant n : ModelWithCorners ℝ (EuclideanSpace ℝ (Fin n)) (EuclideanQuadrant n) for the model space used to define n-dimensional real manifolds with corners

Notation

In the scope Manifold, we introduce the notations

• 𝓡 n for the identity model with corners on EuclideanSpace ℝ (Fin n)
• 𝓡∂ n for modelWithCornersEuclideanHalfSpace n.

For instance, if a manifold M is boundaryless, smooth and modelled on EuclideanSpace ℝ (Fin m), and N is smooth with boundary modelled on EuclideanHalfSpace n, and f : M → N is a smooth map, then the derivative of f can be written simply as mfderiv (𝓡 m) (𝓡∂ n) f (as to why the model with corners cannot be implicit, see the discussion in Geometry.Manifold.IsManifold).

Implementation notes

The manifold structure on the interval [x, y] = Icc x y requires the assumption x < y as a typeclass. We provide it as [Fact (x < y)].

def EuclideanHalfSpace (n : ℕ) [NeZero n] : Type

The half-space in ℝ^n, used to model manifolds with boundary. We only define it when 1 ≤ n, as the definition only makes sense in this case.

def EuclideanQuadrant (n : ℕ) : Type

The quadrant in ℝ^n, used to model manifolds with corners, made of all vectors with nonnegative coordinates.

instance instTopologicalSpaceEuclideanHalfSpace {n : ℕ} [NeZero n] : TopologicalSpace (EuclideanHalfSpace n)

instance instTopologicalSpaceEuclideanQuadrant {n : ℕ} : TopologicalSpace (EuclideanQuadrant n)

instance instZeroEuclideanHalfSpace {n : ℕ} [NeZero n] : Zero (EuclideanHalfSpace n)

instance instZeroEuclideanQuadrant {n : ℕ} : Zero (EuclideanQuadrant n)

instance instInhabitedEuclideanHalfSpace {n : ℕ} [NeZero n] : Inhabited (EuclideanHalfSpace n)

instance instInhabitedEuclideanQuadrant {n : ℕ} : Inhabited (EuclideanQuadrant n)

theorem EuclideanQuadrant.ext {n : ℕ} (x y : EuclideanQuadrant n) (h : ↑x = ↑y) : x = y

theorem EuclideanQuadrant.ext_iff {n : ℕ} {x y : EuclideanQuadrant n} : x = y ↔ ↑x = ↑y

theorem EuclideanHalfSpace.ext {n : ℕ} [NeZero n] (x y : EuclideanHalfSpace n) (h : ↑x = ↑y) : x = y

theorem EuclideanHalfSpace.ext_iff {n : ℕ} [NeZero n] {x y : EuclideanHalfSpace n} : x = y ↔ ↑x = ↑y

theorem EuclideanHalfSpace.convex {n : ℕ} [NeZero n] : Convex ℝ {x : EuclideanSpace ℝ (Fin n) | 0 ≤ x.ofLp 0}

theorem EuclideanQuadrant.convex {n : ℕ} : Convex ℝ {x : EuclideanSpace ℝ (Fin n) | ∀ (i : Fin n), 0 ≤ x.ofLp i}

instance EuclideanHalfSpace.pathConnectedSpace {n : ℕ} [NeZero n] : PathConnectedSpace (EuclideanHalfSpace n)

instance EuclideanQuadrant.pathConnectedSpace {n : ℕ} : PathConnectedSpace (EuclideanQuadrant n)

instance instLocPathConnectedSpaceEuclideanHalfSpace {n : ℕ} [NeZero n] : LocPathConnectedSpace (EuclideanHalfSpace n)

instance instLocPathConnectedSpaceEuclideanQuadrant {n : ℕ} : LocPathConnectedSpace (EuclideanQuadrant n)

theorem range_euclideanHalfSpace (n : ℕ) [NeZero n] : Set.range Subtype.val = {y : EuclideanSpace ℝ (Fin n) | 0 ≤ y.ofLp 0}

@[simp]

theorem interior_halfSpace {n : ℕ} (p : ENNReal) (a : ℝ) (i : Fin n) : interior {y : PiLp p fun (x : Fin n) => ℝ | a ≤ y.ofLp i} = {y : PiLp p fun (x : Fin n) => ℝ | a < y.ofLp i}

@[simp]

theorem closure_halfSpace {n : ℕ} (p : ENNReal) (a : ℝ) (i : Fin n) : closure {y : PiLp p fun (x : Fin n) => ℝ | a ≤ y.ofLp i} = {y : PiLp p fun (x : Fin n) => ℝ | a ≤ y.ofLp i}

@[simp]

theorem closure_open_halfSpace {n : ℕ} (p : ENNReal) (a : ℝ) (i : Fin n) : closure {y : PiLp p fun (x : Fin n) => ℝ | a < y.ofLp i} = {y : PiLp p fun (x : Fin n) => ℝ | a ≤ y.ofLp i}

@[simp]

theorem frontier_halfSpace {n : ℕ} (p : ENNReal) (a : ℝ) (i : Fin n) : frontier {y : PiLp p fun (x : Fin n) => ℝ | a ≤ y.ofLp i} = {y : PiLp p fun (x : Fin n) => ℝ | a = y.ofLp i}

theorem range_euclideanQuadrant (n : ℕ) : Set.range Subtype.val = {y : EuclideanSpace ℝ (Fin n) | ∀ (i : Fin n), 0 ≤ y.ofLp i}

theorem interior_euclideanQuadrant (n : ℕ) (p : ENNReal) (a : ℝ) : interior {y : PiLp p fun (x : Fin n) => ℝ | ∀ (i : Fin n), a ≤ y.ofLp i} = {y : PiLp p fun (x : Fin n) => ℝ | ∀ (i : Fin n), a < y.ofLp i}

def modelWithCornersEuclideanHalfSpace (n : ℕ) [NeZero n] : ModelWithCorners ℝ (EuclideanSpace ℝ (Fin n)) (EuclideanHalfSpace n)

Definition of the model with corners (EuclideanSpace ℝ (Fin n), EuclideanHalfSpace n), used as a model for manifolds with boundary. In the scope Manifold, use the shortcut 𝓡∂ n.

def modelWithCornersEuclideanQuadrant (n : ℕ) : ModelWithCorners ℝ (EuclideanSpace ℝ (Fin n)) (EuclideanQuadrant n)

Definition of the model with corners (EuclideanSpace ℝ (Fin n), EuclideanQuadrant n), used as a model for manifolds with corners

def Manifold.term𝓡_ : Lean.ParserDescr

The model space used to define n-dimensional real manifolds without boundary.

def Manifold.«term𝓡∂_» : Lean.ParserDescr

The model space used to define n-dimensional real manifolds with boundary.

theorem modelWithCornersEuclideanHalfSpace_zero {n : ℕ} [NeZero n] : ↑(modelWithCornersEuclideanHalfSpace n) 0 = 0

theorem range_modelWithCornersEuclideanHalfSpace (n : ℕ) [NeZero n] : Set.range ↑(modelWithCornersEuclideanHalfSpace n) = {y : EuclideanSpace ℝ (Fin n) | 0 ≤ y.ofLp 0}

theorem interior_range_modelWithCornersEuclideanHalfSpace (n : ℕ) [NeZero n] : interior (Set.range ↑(modelWithCornersEuclideanHalfSpace n)) = {y : EuclideanSpace ℝ (Fin n) | 0 < y.ofLp 0}

theorem frontier_range_modelWithCornersEuclideanHalfSpace (n : ℕ) [NeZero n] : frontier (Set.range ↑(modelWithCornersEuclideanHalfSpace n)) = {y : EuclideanSpace ℝ (Fin n) | 0 = y.ofLp 0}

def IccLeftChart (x y : ℝ) [h : Fact (x < y)] : OpenPartialHomeomorph (↑(Set.Icc x y)) (EuclideanHalfSpace 1)

The left chart for the topological space [x, y], defined on [x,y) and sending x to 0 in EuclideanHalfSpace 1.

theorem Fact.Manifold.instLeReal {x y : ℝ} [hxy : Fact (x < y)] : Fact (x ≤ y)

theorem IccLeftChart_extend_bot {x y : ℝ} [hxy : Fact (x < y)] : ↑((IccLeftChart x y).extend (modelWithCornersEuclideanHalfSpace 1)) ⊥ = 0

theorem iccLeftChart_extend_zero {x y : ℝ} [hxy : Fact (x < y)] {p : ↑(Set.Icc x y)} : (↑((IccLeftChart x y).extend (modelWithCornersEuclideanHalfSpace 1)) p).ofLp 0 = ↑p - x

theorem IccLeftChart_extend_interior_pos {x y : ℝ} [hxy : Fact (x < y)] {p : ↑(Set.Icc x y)} (hp : x < ↑p ∧ ↑p < y) : 0 < (↑((IccLeftChart x y).extend (modelWithCornersEuclideanHalfSpace 1)) p).ofLp 0

theorem IccLeftChart_extend_bot_mem_frontier {x y : ℝ} [hxy : Fact (x < y)] : ↑((IccLeftChart x y).extend (modelWithCornersEuclideanHalfSpace 1)) ⊥ ∈ frontier (Set.range ↑(modelWithCornersEuclideanHalfSpace 1))

def IccRightChart (x y : ℝ) [h : Fact (x < y)] : OpenPartialHomeomorph (↑(Set.Icc x y)) (EuclideanHalfSpace 1)

The right chart for the topological space [x, y], defined on (x,y] and sending y to 0 in EuclideanHalfSpace 1.

theorem IccRightChart_extend_top {x y : ℝ} [hxy : Fact (x < y)] : ↑((IccRightChart x y).extend (modelWithCornersEuclideanHalfSpace 1)) ⊤ = 0

theorem IccRightChart_extend_top_mem_frontier {x y : ℝ} [hxy : Fact (x < y)] : ↑((IccRightChart x y).extend (modelWithCornersEuclideanHalfSpace 1)) ⊤ ∈ frontier (Set.range ↑(modelWithCornersEuclideanHalfSpace 1))

instance instIccChartedSpace (x y : ℝ) [h : Fact (x < y)] : ChartedSpace (EuclideanHalfSpace 1) ↑(Set.Icc x y)

Charted space structure on [x, y], using only two charts taking values in EuclideanHalfSpace 1.

@[simp]

theorem Icc_chartedSpaceChartAt {x y : ℝ} [hxy : Fact (x < y)] {z : ↑(Set.Icc x y)} : chartAt (EuclideanHalfSpace 1) z = if ↑z < y then IccLeftChart x y else IccRightChart x y

theorem Icc_chartedSpaceChartAt_of_le_top {x y : ℝ} [hxy : Fact (x < y)] {z : ↑(Set.Icc x y)} (h : ↑z < y) : chartAt (EuclideanHalfSpace 1) z = IccLeftChart x y

theorem Icc_chartedSpaceChartAt_of_top_le {x y : ℝ} [hxy : Fact (x < y)] {z : ↑(Set.Icc x y)} (h : y ≤ ↑z) : chartAt (EuclideanHalfSpace 1) z = IccRightChart x y

theorem Icc_isBoundaryPoint_bot {x y : ℝ} [hxy : Fact (x < y)] : (modelWithCornersEuclideanHalfSpace 1).IsBoundaryPoint ⊥

theorem Icc_isBoundaryPoint_top {x y : ℝ} [hxy : Fact (x < y)] : (modelWithCornersEuclideanHalfSpace 1).IsBoundaryPoint ⊤

theorem Icc_isInteriorPoint_interior {x y : ℝ} [hxy : Fact (x < y)] {p : ↑(Set.Icc x y)} (hp : x < ↑p ∧ ↑p < y) : (modelWithCornersEuclideanHalfSpace 1).IsInteriorPoint p

theorem boundary_Icc {x y : ℝ} [hxy : Fact (x < y)] : ModelWithCorners.boundary ↑(Set.Icc x y) = {⊥, ⊤}

theorem boundary_product {x y : ℝ} [hxy : Fact (x < y)] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_2} [TopologicalSpace H] (I : ModelWithCorners ℝ E H) {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] [I.Boundaryless] : ModelWithCorners.boundary (M × ↑(Set.Icc x y)) = Set.univ.prod {⊥, ⊤}

A product M × [x,y] for M boundaryless has boundary M × {x, y}.

instance instIsManifoldIcc (x y : ℝ) [Fact (x < y)] {n : WithTop ℕ∞} : IsManifold (modelWithCornersEuclideanHalfSpace 1) n ↑(Set.Icc x y)

The manifold structure on [x, y] is smooth.

Register the manifold structure on Icc 0 1. These are merely special cases of instIccChartedSpace and instIsManifoldIcc.

instance instChartedSpaceEuclideanHalfSpaceOfNatNatElemRealIcc : ChartedSpace (EuclideanHalfSpace 1) ↑(Set.Icc 0 1)

instance instIsManifoldRealEuclideanSpaceFinOfNatNatEuclideanHalfSpaceModelWithCornersEuclideanHalfSpaceElemIcc {n : WithTop ℕ∞} : IsManifold (modelWithCornersEuclideanHalfSpace 1) n ↑(Set.Icc 0 1)