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

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
Instances For

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

Equations
Instances For
Equations
• instTopologicalSpaceEuclideanHalfSpace = instTopologicalSpaceSubtype
Equations
• instTopologicalSpaceEuclideanQuadrant = instTopologicalSpaceSubtype
Equations
• instInhabitedEuclideanHalfSpace = { default := β¨0, β―β© }
Equations
• instInhabitedEuclideanQuadrant = { default := β¨0, β―β© }
theorem EuclideanQuadrant.ext {n : β} (x : ) (y : ) (h : βx = βy) :
x = y
theorem EuclideanHalfSpace.ext {n : β} [Zero (Fin n)] (x : ) (y : ) (h : βx = βy) :
x = y
theorem range_euclideanHalfSpace (n : β) [Zero (Fin n)] :
(Set.range fun (x : ) => βx) = {y : | 0 β€ y 0}
@[deprecated range_euclideanHalfSpace]
theorem range_half_space (n : β) [Zero (Fin n)] :
(Set.range fun (x : ) => βx) = {y : | 0 β€ y 0}

Alias of range_euclideanHalfSpace.

theorem range_euclideanQuadrant (n : β) :
(Set.range fun (x : ) => βx) = {y : | β (i : Fin n), 0 β€ y i}
@[deprecated range_euclideanQuadrant]
theorem range_quadrant (n : β) :
(Set.range fun (x : ) => βx) = {y : | β (i : Fin n), 0 β€ y i}

Alias of range_euclideanQuadrant.

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.
Instances For

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.
Instances For

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

Equations
Instances For

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

Equations
Instances For
def IccLeftChart (x : β) (y : β) [h : Fact (x < y)] :
PartialHomeomorph (β(Set.Icc x y))

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.
Instances For
def IccRightChart (x : β) (y : β) [h : Fact (x < y)] :
PartialHomeomorph (β(Set.Icc x y))

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.
Instances For
instance IccManifold (x : β) (y : β) [h : Fact (x < y)] :
ChartedSpace β(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_smooth_manifold (x : β) (y : β) [Fact (x < y)] :

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

Equations
• β― = β―

Register the manifold structure on Icc 0 1, and also its zero and one.