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].

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

Notations

In the locale 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 can not be implicit, see the discussion in Geometry.Manifold.SmoothManifoldWithCorners).

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.

Equations

• EuclideanHalfSpace n = { x : EuclideanSpace ℝ (Fin n) // 0 ≤ x 0 }

def EuclideanQuadrant (n : ℕ) : Type

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

Equations

• EuclideanQuadrant n = { x : EuclideanSpace ℝ (Fin n) // ∀ (i : Fin n), 0 ≤ x i }

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

Equations

• instTopologicalSpaceEuclideanHalfSpace = instTopologicalSpaceSubtype

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

Equations

• instTopologicalSpaceEuclideanQuadrant = instTopologicalSpaceSubtype

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

Equations

• instInhabitedEuclideanHalfSpace = { default := ⟨0, ⋯⟩ }

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

Equations

• instInhabitedEuclideanQuadrant = { default := ⟨0, ⋯⟩ }

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

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

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

theorem EuclideanQuadrant.convex {n : ℕ} : Convex ℝ {x : EuclideanSpace ℝ (Fin n) | ∀ (i : Fin n), 0 ≤ x 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 fun (x : EuclideanHalfSpace n) => ↑x) = {y : EuclideanSpace ℝ (Fin n) | 0 ≤ y 0}

@[deprecated range_euclideanHalfSpace]

theorem range_half_space (n : ℕ) [NeZero n] : (Set.range fun (x : EuclideanHalfSpace n) => ↑x) = {y : EuclideanSpace ℝ (Fin n) | 0 ≤ y 0}

Alias of range_euclideanHalfSpace.

@[simp]

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

@[deprecated interior_halfSpace]

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

Alias of interior_halfSpace.

@[simp]

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

@[deprecated closure_halfSpace]

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

Alias of closure_halfSpace.

@[simp]

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

@[deprecated closure_open_halfSpace]

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

Alias of closure_open_halfSpace.

@[simp]

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

@[deprecated frontier_halfSpace]

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

Alias of frontier_halfSpace.

theorem range_euclideanQuadrant (n : ℕ) : (Set.range fun (x : EuclideanQuadrant n) => ↑x) = {y : EuclideanSpace ℝ (Fin n) | ∀ (i : Fin n), 0 ≤ y i}

@[deprecated range_euclideanQuadrant]

theorem range_quadrant (n : ℕ) : (Set.range fun (x : EuclideanQuadrant n) => ↑x) = {y : EuclideanSpace ℝ (Fin n) | ∀ (i : Fin n), 0 ≤ y i}

Alias of range_euclideanQuadrant.

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 locale Manifold, use the shortcut 𝓡∂ n.

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• One or more equations did not get rendered due to their size.

def Manifold.term𝓡_ : Lean.ParserDescr

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

Equations

• Manifold.term𝓡_ = Lean.ParserDescr.node `Manifold.term𝓡_ 1022 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "𝓡 ") (Lean.ParserDescr.cat `term 0))

def Manifold.term𝓡_.delab : Lean.PrettyPrinter.Delaborator.Delab

Pretty printer defined by notation3 command.

Equations

• One or more equations did not get rendered due to their size.

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

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

Equations

• Manifold.«term𝓡∂_» = Lean.ParserDescr.node `Manifold.«term𝓡∂_» 1022 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "𝓡∂ ") (Lean.ParserDescr.cat `term 0))

def Manifold.«term𝓡∂_».delab : Lean.PrettyPrinter.Delaborator.Delab

Pretty printer defined by notation3 command.

Equations

• One or more equations did not get rendered due to their size.

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

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

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

def IccLeftChart (x y : ℝ) [h : Fact (x < y)] : PartialHomeomorph (↑(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.

Equations

• One or more equations did not get rendered due to their size.

def IccRightChart (x y : ℝ) [h : Fact (x < y)] : PartialHomeomorph (↑(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.

Equations

• One or more equations did not get rendered due to their size.

instance IccChartedSpace (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.

Equations

• One or more equations did not get rendered due to their size.

instance Icc_smoothManifoldWithCorners (x y : ℝ) [Fact (x < y)] : SmoothManifoldWithCorners (modelWithCornersEuclideanHalfSpace 1) ↑(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 IccChartedSpace and Icc_smoothManifoldWithCorners.

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

Equations

• instChartedSpaceEuclideanHalfSpaceOfNatNatElemRealIcc = inferInstance

instance instSmoothManifoldWithCornersRealEuclideanSpaceFinOfNatNatEuclideanHalfSpaceModelWithCornersEuclideanHalfSpaceElemIcc : SmoothManifoldWithCorners (modelWithCornersEuclideanHalfSpace 1) ↑(Set.Icc 0 1)