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

• ModelWithCorners ℝ (EuclideanSpace ℝ (Fin n)) (EuclideanHalfSpace n) for the model space used to define n-dimensional real manifolds with boundary
• 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 ModelWithCorners ℝ (EuclideanSpace ℝ (Fin n)) (EuclideanHalfSpace 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 smooth_manifold_with_corners.lean).

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 : ℕ) [Zero (Fin 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 : ℕ} [Zero (Fin n)] : TopologicalSpace (EuclideanHalfSpace n)

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

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

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

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

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

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

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

def modelWithCornersEuclideanHalfSpace (n : ℕ) [Zero (Fin 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.

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

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

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

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

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

instance Icc_smooth_manifold (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, and also its zero and one.

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

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